Carl-Johan Seger
​Chalmers has recruited Carl-Johan Seger as Professor in Computer Science, working on verification tools in the Wallenberg Autonomous Systems and Software Program (WASP). Photo: Anneli Andersson

He offers methods for securing autonomous systems

Verification is a time consuming and crucial factor in both hardware and software development. The one who finds the smartest method to quickly verify a system becomes highly sought after. Carl-Johan Seger is one of those people.


In 1995, Carl-Johan Seger received a phone call with an offer that would change the direction of his research career at the University of British Columbia. He had only a few days earlier taken up a professor's appointment with so-called tenure, a meriting position.
"I started my new position in June 1995 and in September I resigned," says Carl-Johan Seger, laughing at the memory.

The phone call came from the American semiconductor company Intel, who was in great need of his skills.
"There was a crisis at Intel. They had just rolled out a new generation of Pentium processors when a serious error in the construction was discovered. The error had escaped Intel's very extensive verification procedures. The final bill landed somewhere in the neighbourhood of 475 million dollar", he says.

The problem was that the traditional verification method did not allow testing of all conceivable values, it could simply not be done within the time frame, even though very extensive verification was carried out.

Mathematical tools for verification
Carl-Johan Seger's research is on formal methods, i.e., mathematical tools for analysis and verification of systems. Very useful for verifying hardware – in this case silicon circuits. The tools that Carl-Johan Seger worked with in his research could offer the solution to the precise problems that Intel suffered.

"With formal methods, we developed a verification tool that was not only more reliable, we could also perform the verification faster."

As a result, Carl-Johan Seger introduced early formal verification in the development process at Intel.
"Early formal verification is extremely important for achieving good results. It is only after we verify that we can know for sure, and can draw conclusions from the work. It is usually said that we learn by our mistakes, and I couldn’t agree more."

At Intel, he created the Forte Formal Verification System, based on his previous research, and the same verification system is still used today, over 20 years later.
"If you buy a computer today with an Intel processor, large parts of the processor are verified by this method."

Return to academia
He stayed at Intel for 22 years, and during that time he has published his research with great impact.
"It has been fun working in industry, but there is not much long-term research done. In 2006-2007, I was given the opportunity to be a visiting researcher at Oxford", he says.

Perhaps that is where the thoughts of returning to academia took shape? So, when Intel last year announced staff cuts, and launched a retirement package, he took the offer.
"Intel's offer turned to those who with x number of years in the company, added with one's own age, summed to the number 75 or higher. And it included me with a 3-month margin."

Carl-Johan Seger is pleased with his choice to return to academia and Chalmers, and the mood is on top during the interview. We wonder, of course, how he experiences the transition.
"It's a big change, I cannot say it's neither better nor worse, but on the other hand – it takes a lot of effort and renewal and it makes me feel younger."

Important part of autonomous systems
Carl-Johan Seger is recruited as part of Chalmers activities in the Wallenberg project WASP – Wallenberg Autonomous Systems and Software Program. An important trend along with the development of autonomous systems is the decreasing gaps between hardware and software, we are seeing much more of programmable hardware. There are two very big benefits to doing so – increased performance and reduced energy consumption.

"When a large number of sensors are introduced to enable an autonomous system, and all sensors are sending their data to a central processor, it becomes inefficient and slow. Through programmable hardware, or FPGA, Field-Programmable Gate Array, we can introduce more intelligence closer to the sensors", says Carl-Johan Seger.

FPGA are circuits in which the function of the circuit is determined by software. It provides flexibility, you do not necessarily need to re-design your hardware to introduce new functionality – just rolling out new instructions is enough. But there's a big challenge, it gets a lot more difficult to design and verify.
"Look at cars for example, they contain many computer-powered features, and it's crucial that the systems respond quickly, never fail and are secured. This is what we are testing using formal methods", says Carl-Johan Seger.

So, what does Carl-Johan Seger think about the future of self-driving vehicles out of a safety perspective? He says that there are several layers of technology in the vehicles – all are not critical systems.
"There is a core in the systems that we need to find solutions for, in order for the self-driving vehicles to succeed. The future is about robust technology, but it's also about working out the regulations and what the consequences are if anything goes wrong. The market will determine how big risks that are reasonable to take. If the cost of errors becomes too large then we will not see any self-driving vehicles on the roads."

Carl-Johan Seger points out that autonomous systems are not just about vehicles. We will see all sorts of new services, inspections, deliveries, window cleaning, and a host of applications in industry.
"The development of autonomous systems leads to an increasing need to do right from the start – and thus it gets more and more important with verification. It is simply faster and less of a business risk to do it right the first time."

Back at Chalmers
Carl-Johan Seger is now recruited to Chalmers as Professor of Computer Science. Which means he is back at Chalmers where he started his studies in 1981, after nearly 34 years in Canada, the United States and Britain.
"I don’t say I'm moving back to Sweden. I've been away for so long, so I say I'm moving to Sweden. It actually makes it a little easier for me."

The first task at Chalmers is to build a verification system. Intel has proprietary ownership of the Forte system, so Carl-Johan Seger could not bring it to Chalmers for further research.
"My wife usually says Forte is my fourth child, and maybe there is something to it. I have spent at least as many hours with Forte as with my three children."

However, he has the old system to build on, the one he developed during his time as a researcher before leaving for Intel.
"Now we are rebuilding, and this time, of course, it will go much faster because we already know the target."


Contact details: Carl-Johan Seger, secarl@chalmers.se

Text: Malin Ulfvarson
Photo: Anneli Andersson

Published: Tue 17 Oct 2017. Modified: Mon 23 Oct 2017