Global Sources
EE Times-Asia
Stay in touch with EE Times Asia
EE Times-Asia > EDA/IP

Formal tools won't replace simulation

Posted: 10 Jun 2003 ?? ?Print Version ?Bookmark and Share

Keywords:design automation conference? formal verification? simulation? simulator?

Formal verification is a valuable adjunct to simulation, but not a replacement for it, according to panelists at the Design Automation Conference. User panelists from IBM and Intel voiced the strongest reservations about formal techniques, while those from EDA companies seemed more favorable.

Moderator Rajesh Gupta, professor at the University of California at San Diego, asked panelists whether formal verification will reduce the need for simulation, how formal tools fit into verification strategies and what is the return on investment. He noted that the simulation market, at $90 million per quarter, is far larger than the $13.1 million formal verification market.

John O'Leary, senior staff engineer at Intel, said formal verification has two possible applications - finding bugs in RTL code, and gaining assurance of zero bugs prior to tapeout. "What we've found at Intel, although we do find bugs, is that the real value of formal verification is the assurance," he said.

"I'm sure not going to give up on simulation because I don't know a better way to find early bugs in RTL," he said. "Formal verification has capacity limits and won't find all the interesting properties."

O'Leary noted, however, that formal tools can find tough bugs that simulators miss. To successfully use formal tools, he said, designers need to choose the right problem, have a clear specification, and know which formal tool fits best - equivalence checking, model checking, symbolic simulation, or theorem proving.

"Simulation has always been, and always will be, the single most important verification tool we have," said Daniel Beece, senior staff member at IBM's T.J. Watson research division. He said equivalence checking is the second most important and that semi-formal methods for test coverage come in third.

What makes formal verification difficult for ASICs, Beece said, are capacity limits, complex latching structures and the lack of specialists on ASIC design teams. Beece said he'd rather have a smart verification engineer write a testbench program than spend time creating formal properties - "even though," he said, "it's much more interesting to write temporal logic in some kind of screwy design language."

"Declaring that formal methods haven't worked is wrong," said Fabio Somenzi, professor at the University of Colorado. "If you look at how long it took logic simulation and HDLs to come of age, 15 to 20 years is a typical incubation period for technologies like this." What's needed now, he said, are language standards, design flow integration and solutions to capacity and performance issues.

"There is no contradiction between simulation, emulation and formal verification," said Carl Pixley, senior director of Synopsys' advanced technology group. "The challenge is to find the right combination to make them all cost effective." He described a methodology used while working at Motorola in which designers first write constraints, then develop assertions and finally "flip" the constraints to become monitors.

Brian Bailey, chief technologist for Mentor Graphics' design verification and test division, said formal technology is here and the business model is ready - and what's missing is the "packaging" that will insert it into the design flow. He said formal methods have been held back by a lack of standards, but that Accellera's SystemVerilog and Property Specification Language will help.

"I think we are very close now to a time when formal is a technology everyone will be using, but they might not be aware they're using it," Bailey said.

Harry Foster, chief methodologist at formal verification startup Jasper Design Automation, was the strongest defender of a pure formal approach. "Dynamic verification will not solve the verification challenge," he said. "Pure formal verification can go a lot further, without relying on simulation. The effort to create a quality formal testbench is no worse than the effort to create a quality simulation testbench, and the quality of results is better."

What's needed now, said Foster, is design for verification, such that engineers develop code with both synthesis and verification in mind. He called for greater use of block-level verification and for proving "end-to-end behavior" as well as isolated assertions.

Kathryn Kranen, Jasper president and CEO, argued with IBM's Beece about simulation versus formal verification. She said building a simulation model is difficult, and asked if it wouldn't be better to "just do the [formal] checks." Beece responded that it's difficult to write checks without understanding the design.

"Formal verification is not exhaustive," Bailey warned. "Completion is just as much of an issue with formal as it is with dynamic. Until we can guarantee we can write every property we need to test a design, we're going to need an amalgam of the two technologies."

- Richard Goering

EE Times

Article Comments - Formal tools won't replace simulatio...
*? You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.

Back to Top