Assertion-Based Verification Smoothes The Road To IP Reuse

By most estimates, the verification portion of the design of complex ASICs, ASSPs, and systems-on-a-chip (SoCs) now takes 70% or more of the overall design cycle. So we frequently hear designers using the phrase "verification bottleneck," usually along with terms too colorful for these pages. Verification has fallen far behind design itself in terms of productivity.

Theoretically, the use—and subsequent reuse—of intellectual property (IP) should ease the pain of verification. IP lets designers break up the project into self-contained functional blocks, each of which is independently verifiable. Subsequently, IP blocks can be stitched together in various permutations to create new end products.

Unfortunately, sometimes theory diverges significantly from practical reality. The good news is that overall IP quality has risen, with mainstream vendors working hard to ensure that their deliverables are as close to bulletproof as possible. As long as you're not trying to piece together a 20 million-gate SoC based on IP coded up in Verilog by the sleep-deprived guy in the next cubicle, the IP itself probably won't cause verification woes. The key is to coerce the blocks into communicating among themselves in a civilized fashion.

Having a complete understanding of a given IP block's behavior, both internally and as it relates to other blocks within the design, is the critical link in simulation. But unless you designed an IP block yourself, it's highly unlikely you'll have the kind of insight into its behavior to ensure it doesn't complicate verification. "A consumer of an IP block doesn't necessarily have all the expertise to understand that block available in its company resources," says Lisa Lipscomb, vice president of marketing at NurLogic Design Inc.

Enter the concept of assertions. Assertion-based verification methodologies are growing in popularity. Yet, the landscape in the assertion-based world is confusing and somewhat fragmented \[see "The Top 10 Things Designers Don't Know About Assertion-Based Verification (But Should), p. 78\].

Assertions are a way to describe a block's behavior, or the designer's assumptions regarding its behavior, that can be monitored and checked. In essence, an assertion is a statement that a property of a design must be true. Generally, there are two kinds of assertions. Concurrent assertions state that a given property must always be true throughout a simulation, while procedural (sometimes called temporal) assertions apply only for a limited time, or under specified conditions.

Moreover, assertions can be utilized in various ways. They can be included directly within the hardware-description language (HDL) code that comprises the register-transfer level (RTL) description of the design. Or, they can be applied from outside in the form of testbenches, or collections of test vectors, to check the response of the design to stimulus, or to control a stimulus generator or model checker.

"Historically, when IP is delivered to a customer, what comes with the IP is a book containing the rules for integrating the block into a system," says Francine Ferguson, vice president of worldwide marketing for Verisity Design Inc. For example, it might say that when signal A is high, signal B must be low. Or, it could say that a request for a bus grant must result in an acknowledgement within a specified interval. Bear in mind that the quality of such documentation varies widely, depending on the source of a given IP block.

The problem lies in proving the rules are being followed. They're hard enough to check even by looking at a block in isolation. But once you've integrated the IP into an SoC, for instance, and the ports of the IP are being driven by internal parts of the system or a bus, there's no way to manually know whether or not you're violating those rules. Assertions are a way to assess whether rules are being violated.

Just about all advocates of assertions predict they will be implemented both inside the RTL for so-called "white-box" testing as well as outside in the form of testbenches for "black-box" or system-level tests. Most also envision combinations of these approaches. The industry has suffered from a lack of standardization in how assertions or properties are written, what language they're in, and an approach that can enable their use in both simulation and formal verification. Fortunately, standards efforts are chipping away at this problem and show promise. In addition, tool flows are beginning to appear that might help ease the verification crunch.

Almost everyone agrees that it's critical to have the same assertions span the entire verification process. "Assertions are part of the design, not part of the testbench," says Emil Girczyc, president and CEO of 0-In Design Automation Inc. "So if these properties are true, they should hold everywhere that design is used or reused. And as the design gets modified, those assertions should be revalidated to ensure that the changes didn't introduce something that would violate an assertion."

The terminology implemented in today's verification world could make one pause. It's confusing even to those who market verification products. "One of my favorite questions to ask people is 'What's the difference between assertions and properties?'" says Reily Jacoby, product line manager for formal verification products at Mentor Graphics Corp. "Frankly, no one has given me any definitive reason why there should be a distinction. I can accept that assertions are some kind of subset of a more general property language." But he questions the need for separate assertion and property languages.

Yet, there are separate languages with separate standardization efforts under way. One way to sort these out is to think in terms of standards for assertions employed from within RTL design descriptions and those from outside the design. Both efforts are being spearheaded by Accellera.

Accellera's standards efforts in the assertion-based verification arena come on three fronts. One, called procedural assertions, is an assertions construct being added to Verilog. Declarative properties is another. It focuses on the recent selection of IBM's Sugar 2.0 formal property language as the basis for a standard. The third is structural assertions, which is based on the Open Verification Library (OVL) of assertion modules that was donated to Accellera in 2001 by Verplex Systems. All three efforts intersect in various ways with the goal of building a language infrastructure that supports top-down design and bottom-up verification.

The Inside View: Those who believe that assertions belong inside the RTL code for a block of IP make a strong case. Vendors of verification tools sometimes refer to assertions that are included within RTL as in-line assumptions or assertions. "Designers make a lot of assumptions while they're doing their design. In-line assumptions are the best way to capture them and verify that the designer's assumptions and analysis are correct," says Prakash Narain, CEO of Real Intent.

A key advantage to assertions within the RTL is that they function as documentation. "We find that if someone joins a project and wants to modify a state machine, he can see if there are any assumptions about the coding of the state vectors," says 0-In's Girczyc.

As an aside, users of assertion-based flows should consider how they might fare in a verification flow that uses hardware acceleration and emulation. Jason Andrews, product marketing manager at Axis Systems, says it's important to realize that synthesizable RTL-based assertions inside the design trigger a call to display an error message when an assertion is violated. Some hardware acceleration systems can't tolerate these display calls.

Axis' platform, however, performs simulation and emulation simultaneously. If an assertion is violated while the system is in emulation mode, the system can dynamically drop back into simulation mode, print the message on the screen, and return to emulation transparently to the user.

There are a couple of methods for including assertions within an IP block's RTL description. If you're writing in VHDL, you're in luck: VHDL already contains an Assert construct, albeit a basic one. For Verilog users, the release of SystemVerilog 3.0 at this year's Design Automation Conference (DAC) was good news. Also announced at DAC were key new donations to the standard by Synopsys for version 3.1.

Further industry support for SystemVerilog shown at DAC included Mentor Graphics' announcement that it plans to incorporate the new standard into a range of its tools by 2003. These will include ModelSim, Seamless hardware/software co-verification, HDL Designer Series, Precision Synthesis, and emulation products.

SystemVerilog extends Verilog 2001 to handle architectural and behavioral design as well as verification (Fig. 1). The former comes through the language's incorporation of C-language hardware-modeling constructs that lend themselves to top-down design, while the latter comes largely through the addition of an Assertions construct. This construct is based on the Design Assertion Subset (DAS) developed by Co-Design Automation for its Superlog HDL, which was donated to Accellera. Also contained within SystemVerilog are the OVL assertion modules and contributions from Real Intent.

Co-Design has already released its Systemsim 2.0, an upgraded simulator with support for SystemVerilog. The tool unifies simulation with automated testbench features. It also uses the Interfaces construct within SystemVerilog for enhanced modeling of the communication between IP blocks.

Synopsys' donation to Accellera falls under four categories: testbench modeling capabilities, OpenVera assertions, a C/C++ model interface, and a coverage application programming interface (API) that provides links to coverage metrics. "Accellera welcomes Synopsys' donation and is thrilled with its involvement in Accellera's standardization process," says Vassilios Gerousis, technical coordinating committee chair at Accellera.

OpenVera testbench constructs help engineers quickly and easily develop testbenches within the Verilog language. These testbench constructs include dynamic objects such as classes; built-in testbench primitives like mailboxes; and advanced control constructs such as fork-joins and triggers.

The donated OpenVera assertions enable users to write protocol checkers for dynamic simulation and properties for RTL formal analysis. The C/C++ model interface makes it easier to link C/C++ models or modules directly into a Verilog simulation. This enables a more efficient simulation when the full visibility of the Verilog API is not necessary. The coverage API defines a procedural interface that lets users and EDA tool developers have a consistent method of accessing coverage metrics.

The overall effort within Accellera to drive assertions standards is run by its Assertion Technical Committee, which has two main objectives. One is the definition of the Assertions construct for SystemVerilog, which is to be codified as the future IEEE 1364 Verilog standard. The other is standardization and expansion of the OVL.

The OVL itself provides yet another means for designers to insert assertions into their RTL. These Verilog modules contain the logic that checks for particular conditions as true or false. They can be instantiated by designers inside their design to check whether given conditions occur. OVL components work with all IEEE 1364 Verilog simulators, and the library currently contains more than 30 assertion templates (Fig. 2).

Plans are afoot to bring the OVL in line with the Sugar 2.0 formal property language, which was recently chosen by Accellera from among four finalists as the basis for its standards efforts in the formal language arena. "In the OVL effort, we want to borrow and inherit the semantic notion that comes from Sugar," says Dennis Brophy, Accellera's chairman. "The OVL is going to expand because the syntax of Sugar is now known and fixed. So we have to augment the OVL with expansions to match the Sugar syntax." Brophy envisions the OVL as the "poor man's Sugar tool." Eventually, it should mirror quite a bit of what you can do with Sugar.

Looking In From Outside: The intersection of the OVL, a collection of embeddable canned Verilog assertion modules, with the Sugar language, a formal property language, swings the discussion to the ways in which assertions can be applied in external testbenches and formal verification. Accellera's efforts to drive a formal property language standard begs the question raised by Mentor Graphics' Jacoby: How are assertions different from properties and why do we need languages for both?

Dave Kelf, vice president of marketing at Co-Design Automation Inc., offers one answer. "The OVL and the Superlog DAS work at a low transaction level, whereas the property language is for more higher-level specification properties. Formal properties are for use by high-level verification engineers trying to specify large properties that the whole system would want to use. Assertions are used at a lower level to check specific actions," he says.

In the realm of formal property languages, much of the industry has rallied behind Accellera's standardization efforts with Sugar. Accellera settled on Sugar after a long qualification process that included Motorola's CVB, Intel's ForSpec, and Verisity's e. "Sugar 1.3.1 was donated, and then the IBM team worked for a year and a half on bringing the language in line with our requirements," Brophy says. "None of the donations matched them 100%. What's actually the basis for the work that Accellera is going to do is not Sugar 1.3.1, but Sugar 2.0."

Accellera's Formal Property Language committee has completed a draft of a language reference manual (LRM) for Sugar. Version 1.0 of the LRM is expected to be completed in August.

Sugar, like other formal property languages that are currently available commercially, including Verisity's e and Synopsys' Vera, lets users write hardware properties. Those properties can be implemented by a formal verification tool, such as a model checker, as well as by simulators.

Industry endorsements of Sugar are appearing in the form of tool support. For its part, Cadence Design Systems has upgraded its Verification Cockpit environment to include Sugar 2.0 support, extended transaction-based analysis and debug, and new static-checking capabilities (Fig. 3). Users can capture specifications, requirements, and assumptions as assertions. Then they can verify them statically via static-check techniques, or dynamically through Cadence's NC-Sim mixed-language simulator.

Meanwhile, Synopsys and Verisity continue to support their respective formal property languages, Vera and e. The OpenVera language from Synopsys is an open-source language that, like Sugar, is intended for use by both simulation tools and formal tools. OpenVera operates with products from a number of verification tool vendors.

Most recently, @HDL Inc. announced plans for its functional verification tools to work with the language through a bi-directional interface with OpenVera design flows. The @Verifier tool will perform automatic extraction of OpenVera assertions for each design element and verify those assertions using formal model checking technology.

In constructing OpenVera assertions, the language leverages Verilog as a base layer for the Boolean expressions and design modeling. "We set it up by adding layers on top of that," says Stephen Meier, Synopsys' group director of testbench automation. "The first layer is a sequence layer where you can form temporal sequences. Then we added Intel's ForSpec, which had a lot of strength in formal technology. That allows for more complex sequence expressions to happen and adds some directives to guide formal tools."

Verisity's e language drives the Specman Elite testbench generation tool. With e, users can write bus-functional models for simulation as well as the constraints with which Specman Elite creates random and semi-random tests directed at specific areas of a design.

"A more random approach to verification is critically important," says Verisity's Ferguson. Part of the challenge of IP verification in the context of a system is that verification engineers often can't even begin to anticipate all of the different, and potentially incorrect, ways to implement a given piece of IP.

IP For Verifying IP: There's a growing market for what's generally known as verification IP, which is essentially a prepackaged block of code that captures all assertions that can be applied to a bus protocol or other communication standard. A number of commercial vendors offer such IP. One can think of the OVL that's being built into SystemVerilog as a primitive form of verification IP. But more complex and sophisticated forms are taking root.

To Verisity, assertions represent an executable means of determining whether or not the rules governing the integration of an IP block are being adhered to. They're provided as e Verification Components (eVCs). Each eVC includes three integrated components: a stimuli generator for injecting and generating traffic, monitors and checkers for viewing outputs and checking protocol rules, and coverage reports showing the functional coverage of scenarios on the bus. They're available from Verisity for the AMBA High-Performance bus, Ethernet, PCI, and USB. Many others are available from partners for various standard protocols.

0-In Design Automation also offers its Checkerware library of verification IP. This library of assertion checkers is validated with static and dynamic formal technologies. Available verification IP includes over 20 CheckerWare Monitors for industry-standard protocols.

Checkerware spans the range from simple primitive assertions to complex protocol monitors. "By invoking a complex check or monitor, the user is, in fact, putting down anywhere from several to tens of assertions, coverage, metrics, and statistics," says 0-In's Girczyc. It's touted as a more efficient means of employing assertions. 0-In has also announced a version of Checkerware that supports the Sugar assertion language.

In the memory IP realm, Denali Software offers its Memory Modeler-Advanced Verification (MMAV) verification IP. The tool operates at a high, transactional level of abstraction to observe and iron out the communication between memory, processors, and other peripherals before getting down to RTL simulation.

Qualis Design takes an interesting approach to verification IP with its Domain Verification Components (DVCs). These protocol-specific building blocks enable verification engineers to very quickly assemble application-specific verification environments for Vera and Specman Elite. "The Verisity and Synopsys folks have done a great job of creating what we're calling a simulation operating system," says Michael Horne, CEO of Qualis. "On top of that, we're creating a domain-specific layer to really speed up verification."

DVCs permit users to leverage random-based verification without having to delve into all of its intricacies. Nor do users necessarily need to learn the semantics of Vera or e. Instead, they can home in on writing test vectors.

"We view our verification IP as being the first line of attack, where you get the relatively easy-to-hit cases," says Qualis' CTO, Janick Bergeron. DVCs provide broad functional verification coverage. They'll help users find the holes and the hard-to-reach corner cases. "That's when the designer has to decide whether to go to formal verification or to keep tightening the constraints or go directed," Bergeron says.

Going Formal: At some point, an effective IP verification methodology must venture into formal methods. These methods will exhaustively prove whether an assertion or assumption regarding some aspect of a design is true or not. If the rule being tested is violated, the formal analysis should report back with the input sequence to the circuit that made the violation occur.

"What makes assertion-based verification a robust strategy is that you simulate and apply formal verification to the exact same assertions," says 0-In's Girczyc. "The real value of using assertions with formal is when you find an assertion violation. When assertions get violated, they tend to correlate to bugs."

Even though formal verification is being adopted a little more, Ferguson says, most Verisity customers employ a combination of simulation and formal.

"There's two challenges with formal," she explains. "One is that, often, the problem is too hard for the formal tool because the problem space is too large. So you give the formal tool simplified assumptions. If you give it enough simplifying assumptions, it will be able to prove it. But you still require, in simulation, to make sure you check those cases where those assumptions weren't true to make sure that there are no hidden bugs when you unsimplify those assumptions. So, more and more, even formal companies suggest a combined simulation and formal approach."

This sentiment, as well as the notion that assertions must serve the entire verification process to be fully effective, is echoed by others. "Methodologies are emerging where assertions are going to be leveraged in multiple ways to drive the verification processes," says Real Intent's Narain. These might range from serving as constraints for pseudo-random input generation, to constraints for formal analysis, to actual verification objectives.

Standardization drives the ability for assertions to accomplish this lofty goal. With regard to the formal language standards effort in Accellera, Brophy muses that "it would be nice to ensure that whatever people would be using in Vera would be usable in a Real Intent product, or a Mentor or Cadence simulator. Or, it could serve as the basis for use in other formal technologies."

In fact, some see assertion and formal property standards heralding a new era of innovation in verification. "Many companies are developing innovative methodologies based on assertions, but there was no standard," Narain says. "Once a view emerged that an assertion-based standard had the best potential for tackling the verification problems of the future, standardization kicked in. This will fuel even more tool and technology development. Over the next year or two, we'll see very significant innovation in this space."