Set of assertions serves multiple tools

ince no single technology can effectively verify today's large, complex designs, design teams generally use a combination of tools to find the most design errors in the least amount of time. As a result, design and verification engineers frequently have been forced to master a diverse set of proprietary, and sometimes, complex languages and interfaces.

One way to create a verifiable specification that can drive multiple tools is by using a set of standard assertion modules to define design behaviors. The recently launched Open Verification Library open-source initiative provides just such a set of standard assertion modules. The assertions in OVL can be used in any standard hardware description language (HDL)-based simulator and can also be used with the BlackTie functional checker formal verification product from Verplex Systems Inc.

To understand assertions, it is helpful to define the concept of an event. An event is defined as an HDL (Boolean) expression, which evaluates to a "true" value. For example, when the expression "c_req == 1 && c_ack == 1" evaluates "true," then an event has occurred during verification. An assertion, then, is a claim about an event or sequence of events in a design during verification. For example, an "assert_one_hot" assertion module may be used to state that a finite-state machine always has one hot state encoding. The event would be the change in value of any of the state bits.

An assertion can be used either as something to be verified or as an input constraint. When used as constraints, assertions define legal input behavior for a design. The notion of constraints is important for formal verification techniques, since all possible input combinations that satisfy the constraints will be considered during the process of proving some assertion. Constraints are also useful in the constrained-random vector generation process used in some testbench automation tools. Vectors are generated that satisfy the input constraints.

An effective assertion methodology is one where the design engineer captures the assertions during RTL code development and embeds them directly in the design. This has advantages over the two other approaches-changing the RTL with assertions after code completion, and containing the assertions in files separate from the design files.

The Verilog OVL assertion monitor library allows capture of the assertions independently of the design source file. However, embedding assertions directly in the RTL design facilitates capturing design assumptions and knowledge at the point of development. Thus the assertions become a permanent and portable record of the design intent.

In one customer test case involving 47,000 lines of RTL code (2 million equivalent gates), engineers added assertion monitors between block boundaries, and at partitions of the design that were created by different engineers. This enabled them to more formally define the interface requirements.

Simulation with the assertion monitors enabled quick detection of bugs caused by misinterpretation of interface requirements. Many other assertion monitors were added to the design to check for illegal design behaviors (e.g., state-machine transactions, queue underflow and overflow conditions, etc.). More than 2,500 assertions were added to the ASIC design on this project using the OVL methodology. Assertion monitors found many design errors while adding only a 3 percent overhead to the system-level simulations.

OVL assertions in simulation
In this environment, design engineers were responsible for running their own block-level simulations prior to delivering their individual blocks for integration into the system simulation model. Those blocks containing a higher percentage of assertions were delivered with higher quality, as measured by the relative number of bugs found during system simulation.

Formal verification tools increase design coverage and design confidence because of the exhaustive nature of the technology. The BlackTie functional checker from Verplex Systems is a formal RTL design-verification tool that has native support for the OVL assertion monitor library. BlackTie also provides a number of automatically extracted, pre-defined checks that detect errors such as bus contention, set-reset conflicts on flip-flops or latches and full-case, parallel-case problems without user specification of the assertions.

Formal's full reach
The same set of user-defined assertions specified by the designer for use in simulation can be used for formal verification in BlackTie. The formal tool exhaustively verifies all the assertion monitors in the design, providing 100 percent coverage of the design for user-specified assertions and automatic checks that are proven.

A 650,000-gate-equivalent subset of the RTL design discussed above was formally verified in BlackTie, with 421 of 429 assertions exhaustively proven. The remaining eight could not be exhaustively verified.

However, BlackTie provides a mechanism where partial sequential analysis can be performed for such cases, increasing the design coverage. Exhaustive formal proof of 98 percent of the assertions on the design greatly increased confidence in design quality. If the formal verification had been done prior to simulation, a large portion of simulation time and effort would have been eliminated.

Another benefit of the OVL is that it eases adoption of formal tools, since no complex proprietary formal languages need to be learned to formally verify design behavior.

The OVL assertion monitor library, which includes Verilog source code and full documentation, can be downloaded free from the Open Verification Library Web site, at www.verificationlib.org. The goal is to establish the OVL as a standard for assertion specification that supports multiple design-verification tools from multiple EDA vendors.

K.C. Chen is Vice President of Research and Development and John Emmitt is Product Marketing Manager at Verplex Systems Inc. (Milpitas, Calif.).