Semiformal tools to speed tests

Semiformal tools to speed tests
By Michael Santarini, EE Times
December 27, 2001 (12:03 p.m. EST)
URL: http://www.eetimes.com/story/OEG20011221S0032

Semiformal analysis tools promise to speed up the process of functionally verifying integrated-circuit designs. But Dataquest's chief EDA analyst, Gary Smith, said he doesn't expect semiformal or any other verification method to close the verification gap anytime soon. With design-start medians cruising into the million-gate range, the effort and time it takes to verify that a design is working as planned is only likely to grow.

By most user and analyst estimates, verification today consumes 70 percent of overall chip-development time, and the ratio of verification engineers to designers on a given design team is 3 to 1. That ratio by most estimates will likely mushroom over the next couple of years if vendors of electronic design automation products don't build tools soon to make verification engineers more productive and speed their work.

To that end, the last couple of years have seen the emergence of a batch of startups aiming to create a bridge between formal and functional verification, offering a more thorough dynamic simulation by incorporating formal techniques. Dataquest's Smith calls this relatively new product class "semiformal analysis tools."

Such products are fast gaining user kudos, Smith said, because semiformal analysis enhances the existing simulation flow with formal techniques, allowing users to better find corner-case bugs within dynamic simulation.

Some engineers refer to it as "dumbed-down model checking," because the tools analyze hardware-description language (HDL) code and prompt users to enter "build." Alternatively, the tool will automatically generate "assertion checkers" or "monitors" that can be run with simulation. Users create these assertion checkers to put up red flags when certain violations occur in simulation.

"The key to this approach is viewing semiformal verification as a mplifying the design and verification-engineering knowledge already embodied in a testbench and functional test suite," said Steven White, vice president of operations at 0-In Design Automation (San Jose, Calif.), one of the quartet of players active in semiformal analysis. White said that during any HDL simulation run, "seed" states are captured to serve as starting points for the formal methods. A semiformal-verification tool starts from each state in the seed, and tries to find new stimulus sequences that will violate assertions about the design. In so doing, the tool discovers legal behaviors that could have occurred but did not in the functional tests.

Bugs' dig
Dino Caporossi, vice president of marketing at Verplex Systems Inc. (Milpitas, Calif.), said that many of the bugs semiformal tools are ferreting out have caused customers to refabricate, or respin, their designs. "In the past these types of bugs went undetected, because there just isn't enough time to simulate everything you need to check," Caporossi said.

But analyst Smith said that each of the four vendors fielding semiformal tools — 0-In, @HDL, Real Intent and Verplex — uses different assertion methods, and each checks for different classes of bugs. "This is a big issue with users, because they don't want to learn four different languages," Smith said.

However, Smith said that if vendors can agree on one standard language, the market — currently at $3 million and growing at 27 percent per year — could rise at a far greater clip.

"Semiformal has become an established part of the design flow and users want tools, but they also are waiting for the industry to decide on one assertion language," Smith said.

One problem is the lack of one clear leader in the semiformal-analysis niche and, thus, no clear de facto standard that would seem an obvious candidate for industry standardization through formal channels such as IEEE.

That may change in 2002. Standards organization Accellera, the group fo rmed by last year's melding of Open Verilog International and HDL International, has taken upon itself the job of crafting an industry-standard formal-verification language for describing assertions and properties.

Accellera chairman Dennis Brophy said the organization is currently considering four languages for the job: Temporal e from Verisity, CBV from Motorola, Sugar from IBM and ForSpec from Intel. But these languages are directly targeted at creating a standard for model-checking tools. Whether they — or, more likely, subsets of these four languages — will work indirectly for semiformal tools remains to be seen.

"We will have a couple of representatives from other Accellera groups monitoring the formal-verification group," Brophy said. "They will hopefully be able to find synergies that can be applied to their own work."

Brophy said the system Verilog group within Accellera's HDL-plus technical committee will be in charge of assertion constructs for the Verilog language, and will also monitor synergies with Accellera's formal-verification committee. The end goal is to find a language that can be used across formal and semiformal tools, facilitating verification reuse, said Adriana Maggiore, senior staff engineer with TransEDA and a member of Accellera's formal-verification committee.

"The adoption of a standard formal property language by Accellera will be a turning point in the evolution of the verification market," Maggiore said.

Semiformal tools may not turn out to be a standalone market. But along with a standard, reusable formal-verification language, semiformal tools are important components in creating the intelligent testbench, said Tarak Parikh, vice president of product engineering at @HDL (San Jose).

"The 'intelligent RTL [register transfer level] testbench, as coined by Dataquest, is the long-term objective, with semiformal tools being one of the key ingredients," Parikh said.

For the most part, vendors in the semiformal space said they would like to se e a standard and that a language war is not likely to occur. Each of the vendors said it would likely support a formal language and an assertion language if they became industry standards.

Anil Gupta, executive vice president and general manager of Real Intent Corp. (Santa Clara, Calif.), said his preference is a standard that extends HDL. "For assertions, we believe that synthesizable HDL plus a simple 'assert_never' construct is currently the most practical way to support formal-based verification," said White of 0-In. "For formal languages, Accellera is now considering several candidates as the basis for a new standard."

See related chart