San Francisco Privately held EDA vendor Averant Inc.'s booth at the Design Automation Conference (DAC) here last week featured a graphic showing a toothbrush and dental floss, with the caption "For best results, use both." The analogy was meant to highlight the relationship between simulation and formal verification, according to Averant executives, who said designers need to employ both techniques to achieve adequate design closure.
"If you think about brushing your teeth, it's like random simulation," said Larry Lapides, Averant's vice president of sales. And just as dentists joke that you should floss only those teeth you wish to keep, Lapides said you should use static verification only on designs you want to succeed.
Averant took advantage of DAC to roll out the next generation of its Solidify tool, offering designers fine control over the thoroughness of formal verification.
Lapides and Ramin Hojati, Averant's president, said Solidify 4.0 offers an industry-first guided-proof system that enables designers to conduct both rapid "bug hunting" exercises early on in the design cycle and then, later on, more exhaustive proofs of assertions.
"There are cases where you are generating tens of thousands of properties, and you really need to have them run overnight on a single computer," Hojati said. "And there are also cases where someone really wants to know if one property is going to pass, and has to spend a lot of time with it. This tool gives designers great flexibility to decide how much time they want to spend."
According to Hojati, early in the design cycle users may want to process 100 properties in seconds on a single computer in the bug-hunting phase. Later, when the focus shifts to exhaustive proofs, the user may have days and several machines to process these properties, Hojati said. By trading off completeness and accuracy against CPU time, Solidify can provide early feedback while achieving maximum use of available computing power, he said.
Solidify 4.0 also includes other enhancements, such as support for the entire SystemVerilog Assertion (SVA) language. Also supported is the use of in-line SVA, verification intellectual property (IP) attached through the bind command and the Open Verilog Library (OVL) implemented in SVA, according to Averant.
Hojati and Lapides said that Solidify 4.0 also offers another industry first: the ability to translate among several property languages including SVA, PSL, OVA, OVL and HPL. This, the executives said, gives design teams the freedom to choose the property language that best serves their needs, enabling preservation and reuse of verification IP.
"The tool reads four languages and writes out four languages," Hojati said. "There is value in that. Customers can feel much more confident their IP is secure."
Other enhancements include extended debugging capabilities and clock-crossing checks, as well as support for PSL version 1.1, according to Averant. Hojati said the extended debugging capabilities are similar to existing commercial debuggers, but that Solidify allows people to stay within their own design environment.
Solidify now also handles any mix of Verilog descriptions in the same design. According to the company, the new Solidify also supports Liberty's cell format.
Solidify 4.0 will be available next month on Linux, Windows and Solaris platforms. Hojati declined to reveal the price, but did say that Averant has "reconfigured the product a little bit," adding property code coverage, which he de-
scribed as being analogous to code coverage in simulation and unique in the static verification world.
According to Lapides, formal verification continues to be held back by a misconception about where it fits into the overall verification methodology.
"Verification methodology is really driving toward coverage verification, with an overall objective of 100 percent functional coverage," Lapides said. "People understand that bug hunting is good early on, but there is actually a second value for standalone tools."
See related chart