Method ensures on-track designs

In addition to design properties that can be automatically extracted, there are more complex properties that require detailed knowledge about the design and its implementation. The lack of a standard way of specifying user-defined properties for use in multiple verification tools has been a problem. To address this issue, the Open Verification Library (OVL) initiative has been launched to provide design and verification engineers with a single interface for HDL implementation property specifi cation. The OVL assertions provide the designer with a simple specify-once technique for capturing user-defined properties. Several verification tools, including standard HDL simulators as well as formal verification tools, can use this property specification technique.

We present automatic bus-contention property check results for a gate-level design from C-Cube Microsystems (now part of LSI Logic) and then explain a methodology used on a large ASIC project to specify user-defined assertions using the OVL. This methodology includes using OVL assertions to capture implementation corner-case concerns, as well as defining a set of interface assertions on design sub-blocks. These interface assertions form a "verifiable contract" between the multiple design blocks and multiple design engineers.

Finally, we address the use of HDL assertions during RTL implementation and how this method of specification differs from assertion specification using hardware-verification languages or higher-level prop erty languages.

Many automatic checks can be extracted from the design using today's emerging verification tools, eliminating the need for the user to specify assertions to verify many common design functions. These automatic checks can be analyzed at both the RT and gate levels. As with user-defined assertions, no testbench creation effort is required to formally verify the automatic checks, thus shortening the verification cycle.

The unreachable full-case check is an example of an automatically extracted property. In this case, the RTL full_case synthesis pragma asserts that all possible branches of a case statement are covered. This prevents the inference of a latch during the synthesis process, while enabling the synthesis optimizer to treat unspecified branches as "don't cares." However, unlike synthesis tools, simulators do not recognize the various synthesis pragmas.

Two designs can be logically equivalent and a functional error in the RTL could be faithfully reproduced in th e gate-level model-a particularly insidious situation. There is a class of design errors that cannot be easily exposed during RTL simulation or using RTL-to-gate equivalence checking, yet are readily revealed using gate-level simulation.

To verify this class of bugs, the Verplex Systems BlackTie functional checker automatically extracts all full- and parallel-case properties from the design and proves that they are correct for all sequential patterns leading into the case statement, thus eliminating the need for gate-level simulation.

In addition to the full-case check, the problem could have been identified on either the RTL or gate-level module using its automatic bus-contention checks. Bus-contention checking has proven to be very valuable as part of the verification methodology at a number of companies, including C-Cube Microsystems.

In testing a C-C ube design, certain buses were not disabled during scan mode. Using formal property-checking techniques, the bus-contention problem was quickly identified as a result of the scan_mode signal being asserted. Formal analysis of automatic contention checks involves a full sequential analysis of the design, to determine whether a contention or bus floating condition can ever occur.

As another example of an automatic property, let's examine an asynchronous clock-domain crossing check. This type of automatic check allows the user to specify a synchronization scheme that can then be verified to ensure that all clock-domain crossings are not violated. For example, a common scheme is to use one or more extra flip-flops clocked by CLK B when going from the domain of CLK A to the domain of CLK B.

Extracting, and then formally verifying, a very large number of properties from today's design is one technique for shortening the verification cycle while achieving higher confidence in the design's functiona l correctness. For example, one design team formally verified more than 300,000 automatic functional checks on a 2.7 million-gate design in 21 minutes using a standard desktop workstation So, why code HDL assertions during design implementation? Software engineers have known for years that it is probably a good idea to check that a pointer passed into their code is not a NULL value prior to use. If a NULL pointer is encountered during normal execution, the problem can be quickly isolated when an assertion is used. Of course, asserting that a pointer will not be NULL says nothing about who is going to test what. In other words, the designer is placing a proposition into his code which states that a particular implementation property will always be TRUE. This is know as design-by-contract and is consistent with the redundancy verification convergence model of Janick Bergeron (author of Writing Testbenches: Functional Verification of HDL Models): that is, that the design engineer should not verify his own desig n, since the designer is only stating a proposition. In fact, the verification engineer will read the design specification and create a set of test scenarios to validate the designer's implementation. During the course of verification, if a sequence of events emerges where a calling routine passes a NULL pointer, then the problem is quickly isolated via the implementer's assertion, dramatically simplifying debug.

Applying assertion techniques during hardware implementation should be no different from software implementation. For example, an RTL design engineer might claim that a particular queue counter will never overflow from 8'hFF to 8'h00. If the counter does unexpectedly overflow illegally during simulation, then isolating the implementation bug through the assertion firing is significantly easier than tracking down an invalid bus transaction, which is a result of the implementation bug. Furthermore, adding the assertion for the queue counter provides a target for the formal engine for exhaustiv e verification.

The Open Verification Library contains a rich set of assertion modules written in standard HDL (Verilog) syntax. These assertions can easily be instantiated in the design under verification to flag violations of specified functional design behavior. The design team on a large ASIC project instantiated more than 3,600 OVL assertions within their design to provide a vendor-independent mechanism for specifying design intent. The designers targeted the same assertion at simulation and with formal verification tools and found that 85 percent of all bugs discovered during the verification process were identified by an HDL assertion. Furthermore, debug time was reduced on average from days down to minutes.

There are many examples of HDL implementation as assertions. Assertion examples include checkers for a valid combination of states, valid combinations of active signals for a given state, mutual exclusions, one_hot, parity, valid cycle relationship between combinations of signals, valid min/max cycle duration for a given signal and so forth.

As another example, we might assert that a particular design's memory address remains constant for exactly five clocks after the memory cycles have begun. Using the OVL assertions for this example, the engineer would code:

assert_unchange #(0,`WIDTH, 5)

stable_address (ck, rst_n, mem_ cyc, mem_address);

where "mem_cyc" is the start_

event that initiates checking of the test_expr, and "mem_address" is the test_expr.

Embedded assertion modules also provide a way to verify reusable intellectual property. The assertions in the IP block create a permanent and portable record of design intent. This can help IP consumers to verify that they have used the IP in their design in the manner that was intended. Input assertions (constraints) can be used to verify that the blocks driving those inputs are satisfying the IP block input requirements. Output assertions ensure that the IP block is behaving correctly in the SoC design.

So why do HDL implementation properties use a hardware-verification language (HVL) or a higher-level property-specification language? After all, many HVLs provide powerful language features that can be used to describe correct temporal behavior. These HVLs can be used for data generation and results analysis. In addition, the Accellera Formal Ve rification committee is actively defining a property-specification language that multiple verification processes can leverage. Therefore, it could be argued that either HVLs or formal property languages should be able to provide all the power necessary to express assertions within the design. However, a variety of stakeholders in the design and verification flow necessitate a variety of approaches to specifying design properties.

The reality of the contemporary design and verification flow requires a broader look at the issues and an understanding of the goals of the various stakeholders. The value white-box testing (through assertions) provides over a black-box testing approach has been validated by numerous sources. And white-box testing can be performed with assertions, HVLs or formal property languages. However, experience shows that verification engineers, whose goal is design validation, prefer an HVL approach to specifying properties of the design. On the other hand, the design engineers' focu s is on implementation using hardware-description languages (HDLs).

In addition to the dichotomy of goals, this issue also encompasses the areas of expertise of the various stakeholders. Quite often, the verification engineer lacks sufficient in-depth knowledge of design implementation details to provide effective white-box assertion coverage. On the other hand, during the course of RTL development, the design engineer makes low-level assumptions about the design's environment as well as other implementation assumptions. Experience has shown that if design assumptions or concerns are not captured during the process of RTL implementation, then many lower-level implementation properties are lost (that is, they will not be verified). For example, the verification engineer might wish to verify that a PCI-bus controller exhibits correct behavior. This can be accomplished by using an HVL to generate correct bus-functional stimulus and validate correct bus-functional results. The verification engineer, howe ver, would not validate specific implementation properties.

Continuing with this example, assume that the PCI controller contains multiple state machines. The design engineer's decision to implement a particular state machine as a one-hot vs. some other type of encoding is irrelevant to the verification engineer-provided that the PCI controller exhibits correct bus-functional behavior. Yet capturing properties of the implementation (for example, one-hot) during the design process provides better white-box coverage.

Hence, although there is some overlap in HDL assertion specification vs. HVL and property-language specification, the end user of the particular form of specification is different. As a result, the convenience of HDL assertion specification must be a consideration. A very effective property-checking methodology can be constructed that combines automatic property checking and HDL implementation assertion checking using the OVL and HVLs with higher-level forms of property specification.

By applying the property-checking methodology described, the engineer will experience a dramatic improvement in traditional simulation productivity. By incorporating formal property-checking technology into the design process, complex bugs that are often missed can be exposed. Furthermore, formal property checking can reduce the simulation and testbench development effort. Until recently, however, it has been difficult to adopt formal verification tools into existing verification flows because of ease-of-use limitations.