Design intents raise verification level

any case studies have shown that functional verification often consumes more than 60 percent of the engineer-hours in system-on-chip (SoC) projects. The collision arises because design reuse tends to shift the overall development effort even more toward functional verification and to entrench verification as the bottleneck for reducing development time. To solve that problem, a number of innovative ideas have emerged, including the adoption of an assertion-based verification methodology at both the virtual component (VC) and SoC levels.

Assertions are executable statements of designer assumptions or design intent that are independent of the implementation. In fact, assertions are a form of verification reuse that can be said to form the missing link between design reuse and functional verification.

The details of assertions vary widely but several key concepts are common. The assertions should be self-documenting and easy to specify. They should be able to capture complex rules for design structures and interfaces. They should be checked in simulation and be usable for formal and/or semiformal verification. Finally, the assertions should travel with the VC so that they can be reused during full SoC verification.

From the standpoint of a VC creator working in register-transfer level (RTL)-Verilog or VHDL-assertions document design assumptions and help with standalone VC verification. In this way, assertions help to verify a VC in much the same way that they help to verify any RTL design. Assertions on both internal design structures and on interfaces help to ensure that the virtual component is behaving correctly during simulations.

As an example, many VCs contain first-in, first-out (FIFOs) to buffer data flowing between the interfaces. During the design phase, bugs related to FIFOs are quite common. A FIFO may accept a write request even when it is already full, leading to overflow and data loss. Similarly, a FIFO may accept a read request when empty, generating an underflow and producing invalid data. In such cases, the design error could be either in the FIFO itself or in the control logic issuing the reads and writes to the FIFO.

An assertion that the FIFO should never see a write when full or a read when empty is an excellent way to ensure that this part of the VC operates properly. Such an assertion is a valuable complement to traditional "black-box" verification. Although a testbench for end-to-end behavior may be able to detect that data has been corrupted within the VC, backtracking to the source of the bug can be very hard.

In addition to defining proper behavior for internal structures such as FIFOs and state machines, assertions can capture the protocol rules for the VC interfaces. Assertions on VC inputs help during testbench development since they can report a violation whenever bus-functional models or other testbench components stimulate the VC incorrectly. Assertions on VC outputs check that the VC is operating correctly.

If the VC creator has access to formal or semiformal verification tools, the assertions may have value beyond RTL documentation and simulation. Ideally, the assertions can be automatically converted to targets for formal-based verification. A formal or semiformal tool can target each assertion-for example, that a FIFO should never overflow-and mathematically consider behaviors that could violate this assertion.

Unlike the limited exercise of a VC in simulation, formal analysis may be able to mathematically prove that the assertion can never be violated. Alternatively, the formal or semiformal tool may provide a "counter-example" that shows a way that the assertion could be violated. This counter-example must have a valid sequence of behaviors that could have occurred in simulation if the test suite had happened to generate that particular sequence.

When formal analysis considers possible behaviors for the VC, it must ensure that only legal input sequences are considered. This requires a set of constraints to define the protocol rules for the VC inputs.

Some formal and semiformal tools allow assertions on the VC inputs in simulation to be automatically converted to constraints. Thus, simulation assertions may be reused in formal analysis as either targets or constraints as appropriate.

Assertions on the VC inputs are especially important, since they can also help to verify that the SoC is using the VC correctly. If the assertions travel with the VC as part of the RTL description, then they are available for SoC verification. If the SoC logic that stimulates the VC does not obey the protocol rules for the VC inputs, this can be detected as an interface assertion violation in SoC simulation.

It is impossible to overestimate the value of immediately detecting misuse of a VC within the SoC. SoC designers achieve rapid debug of errors in their understanding of the VC protocol or bugs in their interface logic implementation. The VC provider also benefits from lower support costs since improper stimulus of the VC often puts the VC into anomalous states that are hard to debug.

Finally, the description of the VC interfaces in the form of assertions may also allow the SoC designs to employ formal or semiformal verification for the VC interface logic.

Industry efforts
There are several industry efforts to develop a common assertion method that works for simulation, formal verification and semiformal verification. 0-In is partnering with other EDA vendors to support its flexible RTL directive syntax, while Synopsys Inc. (Mountain View, Calif.) recently created the Vera Open Source Initiative to broaden support for the OpenVera language.

The OVL initiative is encouraging wide adoption of its RTL assertion library by both simulation and formal-based EDA vendors; Accellera has a working group developing a common assertion language that leverages best practices from a number of industry experts.

Thomas L. Anderson is Co-chair of the VSIA Functional Verification Development Working Group (DWG) and Vice President of Applications Engineering at 0-in Design Automation Inc. (San Jose, Calif.).