Do Students Need More Formal Education?

A few weeks ago, some of the top researchers and practitioners in the area of formal methods converged on Portland, Oregon. The event was the annual Formal Methods in Computer-Aided Design (FMCAD) conference and Semiconductor Engineering attended the panel titled “Teaching Formal Methods: Needs, Challenges, Experiences, and Opportunities.” Panelists included: Jason Baumgartner, formal verification development lead at IBM; Mike Durling, manager of supervisory controls and systems integration at GE; Pete Manolios, professor in the College of Computer and Information Science at Northeastern University; Vigyan Singhal, CEO of Oski; Moshe Vardi, Karen Ostrum George distinguished service professor in Computational Engineering at Rice University and Director of the Ken Kennedy Institute for Information Technology; and Helmut Veith, Professor at the faculty of informatics at the Vienna University of Technology.

“Formal methods have had a transformative impact on hardware verification” said panel moderator, Panagiotis Manolios, professor in the College of Computer and Information Science at Northeastern University. “But formal methods are poised to have a big impact and to do the same things for safety critical systems.”

A recent study, which looked primarily at the aerospace industry, showed that adoption of formal methods is increasing, but the biggest barrier to adoption is education. Thus the motivation for the panel.

Mike Durling talked about the amount of distributed software being used in safety critical applications such as jet engines, healthcare imaging equipment, and nuclear reactors. “Once something has become certified nobody wants to change it,” Durling said. “The bureaucratic barriers become too high. While these things could be made more efficient, nobody wants to change them. This creates an opportunity for more formal verification of software running on hardware that composes systems.” Durling went on to talk about the role of research within GE, how it relates to product development, and the lack of formal knowledge amongst them. “We need tools, education and a community.”

Vigyan Singhal and his company, Oski, are users of formal tools rather than developers of them. They currently have about 20 people that were hired as new college grads. Some don’t have an EE or CS background; instead they have a chemical or mechanical engineering background. “We stretch the technology to the limit so that we rarely get full proofs,” he said “and we rarely compete against other formal plans, we are compared against simulation. We must be able to justify the bugs that are missed as well as the ones that are found.” Vigyan said that when it comes to formal, he would prefer to train one person full time rather than a greater number of people part time. “Metrics enable us to show progress, but at the end of the day there is no substitute for thinking.”

Manolios started by saying, “We should teach formal methods at the undergraduate level.” His justification is that he believes that most students don’t even think about the ability to reason about software with any mathematical precision, using formal methods. “In many cases the thing that is taught last is the very thing that could have helped them with all of their previous studies. It changes the way you think. If we taught formal semantics early on, it could be used for compiler classes, to verify that transformations are correct and many other ways.” Northeastern has been teaching this since 2008 but there are still challenges about how to integrate it with the curriculum.

Helmut Veith said that the education system in Europe is a little different compared to the education system in the United States. “We have a lot of people teaching logic and there are a number of areas that are compulsory in Bachelors courses and lots more in Masters.” In Europe, most of the industrial companies leading the adoption of formal methods are in the automotive industry.

Moshe Vardi simply stated that, “If the case [for formal methods] were compelling enough, the industry would overcome barriers. I don’t think this is the case and there are not many companies rushing to the door.” Vardi questioned the use of formal at Intel. “I would guess it has actually gone done in recent years. Is it because there are not enough educated people? I think it is the other way around—the lack of industry adoption is not creating the downward pressure.” He talked about the competition in education and noted you cannot compete with the buzzwords of today, such as big data and cloud programming. “Perhaps change the focus to reliability, or security of software. Changes must be made by the industry, not by the people in this room. “

Jason Baumgartner said that within IBM there are about 10 people developing tools and hundreds using the tools. “Most of the users of formal methods do not come with a formal methods background. Synthesis and design backgrounds are more important. We only need a few experts in formal technology.” Baumgartner complained that most EDA vendors think of formal as mystery black boxes that cannot be divulged. He believes they need to educate project leads about how best to use all of the forms of verification. “It all comes down to return on investment. Perhaps we need another major problem in the industry to raise awareness.”

Speaking from the audience, Sandip Ray of Intel stated, “We are here to talk about formal methods but we need a system-level solution and we don’t really talk about how formal understands simulation and the other way around. There are many separations that need to be bridged.”

Another person from the audience asked about the cost benefit tradeoff. Singhal answered that not all problems are worth using formal on. Durling claimed that if you can identify the 15% of problems that formal would do well on, it would be much easier. “When it pays benefits, people will pay attention.”

Vardi stated that there is no semiconductor company that does not use synthesis.” This is not a question about the amount of teaching about synthesis. The resultant discussion attempted to claim this is because you just have to use synthesis; you don’t need any special training, but perhaps formal tools should be the same.

Darryl Stewart of ARM added that his company does a lot of model checking. “People come into the company not even having done verification. It is not just formal.”

Offline, Dave Kelf, OneSpin Solutions’ marketing director, agreed with the tone of the panel saying “Formal Verification has proven to be one of the most complex and painful [EDA technologies] to adopt. The serious vendors have created pre-packaged solutions, which target specific verification problems. That helps both with the practical issue of targeting the verification problem in hand, as well as eliminating the need to write properties, in the form of assertions, to get the job done.

Sudhir Kadkade of Mentor noted, “It would help if formal techniques were introduced when other subjects are taught, such as algorithms, operating systems, communication networks, etc. Learning about how to apply FM in specific areas is more important than learning the theory.”

See also:
Cracking the Tough Nut using Formal Methods
Coming up with the Wrong Formal Answer

Formal Verification Tool Providers:

Combinatorial Equivalence Checking
Modified definition from EDAC – A formal verification technique which verifies the integrity of each design step by proving the functional equivalence between the combinatorial portions of two implementations.

Cadence (Conformal), Mentor Graphics (FormalPro), Synopsys (Formality, Quartz), OneSpin (360 EC)

Sequential Equivalence Checking
Modified definition from EDAC – A formal verification technique which verifies the integrity of the design step from an untimed or partially timed model to a fully timed RTL model by proving the functional equivalence between the two implementations.

Jasper Design Automation (Jasper Gold), Calypto (SLEC)

Property (Model) Checking
Definition from EDAC – A formal verification technique which compares the functionality of a design to a set of user-specified properties or characteristics. Determines whether a set of conditions or properties hold true or are contained within a given implementation of a design. Also referred to as property checking.

Mentor Graphics (Questa Formal), Cadence (Incisive Formal)

Clock Domain Crossing
Real Intent (Meridian CDC), Mentor Graphics (Questa CDC), Atrenta (SpyGlass CDC), Jasper (Jasper Gold)

X-Propagation
Real Intent (Ascent XV), Jasper (Jasper Gold)

Smart Lint
Real Intent (Ascent), Atrenta (SpyGlass)

Other
Synopsys (ESP-CV for memory verification), Jasper (Jasper Gold – security paths)