During the decade of the 1980s, it was clear when functional verification of a new chip was finished: The chip was ready to tape out when the engineers had finished simulating everything they could think of. Sometime during the 1990s, that simple metric stopped working.

Today, when you are developing a multi-million-gate chip, functional verification is never really finished. You can always write more directed tests, run more pseudo-random simulation, specify more assertions, or let formal verification tools explore deeper. Without metrics that tell you when to tape out, you'll miss your market window.

Advanced assertion-based coverage metrics are the key to making tape-out decisions for multi-million-gate chips. Assertion-based coverage metrics can provide a quantitative measure of the thoroughness of verification, measure verification progress, and provide guidance about what to do next. Furthermore, the metrics require no effort by the development team beyond the effort of using assertions in the first place.

Simple code-coverage metrics such as line, branch and sub-expression coverage have been used for many years. These metrics simply identify areas of the RTL code that have not been exercised at all in simulation. In the '80s, code coverage was an adequate metric and was widely adopted because it was easy to measure and easy to understand. However, for a complex, multi-million-gate design, 100% code coverage represents only a small initial step towards verification completion; after this step is completed, the metric is of no further use.

Some development teams have augmented simple code-coverage metrics with higher-order metrics such as state and arc coverage. These measures are applicable only to state machines and disregard other worrisome areas, such as interactions between state machines. Again, when state and arc coverage reaches 100%, most of the tough verification still lies ahead. Worse yet, development teams can waste a lot of time and effort trying to figure out whether the coverage numbers are low because the tests are bad or because the targeted states and arcs are impossible to reach.

Functional coverage metrics, including coverage points, more closely approximate what is needed today for effective coverage-driven verification. These metrics are designed to check that the verification tests have exercised specific key functionality — for example, executing all instruction types or transmitting and receiving all packet types. Such metrics are design-specific, so they need to be redeveloped for each new design. Developing a full set of custom functional coverage metrics and the monitors to measure them can represent a prohibitively large investment for the verification team.

Assertion-based verification (ABV) has enabled dramatically more effective metrics for coverage-driven verification. In ABV, the development team instruments the RTL code using simulatable assertions. (Assertions are statements about how the design is intended to behave at the RTL level.) The development team places assertions throughout the design — on worry cases, inter-block interfaces, and complex RTL structures — wherever the protocols may be misused, assumptions violated, or design intent incorrectly implemented.

Typically, thousands of assertions are embedded in a multi-million-gate design. The development team runs directed simulation tests with the assertions in place and then applies formal verification directly targeting the assertions. The embedded assertions increase observability, so simulation finds more bugs faster. Formal verification exhaustively explores the behavior of the design, revealing tough bugs that simulation misses.

The purpose of assertions is to monitor worry cases in the design. Obviously, measuring the functional coverage associated with a worry case is of great value in determining whether the worry case has been adequately stressed by the verification tests. One new assertion-based coverage metric, called simulation structural coverage, measures the coverage of corner cases and other functional behavior closely associated with a given assertion in the design.

Measuring and aggregating all the functional coverage associated with all the worry cases, inter-block interfaces, and complex RTL structures in a multi-million-gate design represents a breakthrough in coverage-driven verification. But each different type of assertion requires a different functional coverage monitor.

For example, the appropriate functional behavior to measure for a FIFO assertion (an assertion to detect FIFO overflow and underflow bugs) is the number of en-queue operations, the number of de-queue operations, the number of times filled, the number of times emptied from a partially-filled state, and the maximum number of entries. On the other hand, the appropriate functional behavior to measure for an arbiter assertion includes the number of requests on each channel, and the minimum and maximum delays from request to grant.

To use simulation structural coverage cost-effectively, it makes more sense to call out assertions from a library than to code them from scratch using a basic assertion language. Given an assertion library approach, the appropriate coverage monitor for each assertion type can be pre-coded and built into the assertion library element.

Then, wherever an assertion is placed in the design, the embedded coverage monitor can measure detailed functional coverage information that is specific to the assertion. A web of thousands of assertions in a multi-million-gate design can collect an enormous amount of specific, relevant functional coverage data that can be used to accurately judge the thoroughness of the simulation tests.

Two additional assertion-based coverage metrics tell the development team whether the design needs more assertions. Assertion density measures the number of assertions of each type in each module. (As with simulation structural coverage, assertion density is most relevant when using complex, high-value assertions, such as those in an assertion library.) Minimum sequential distance measures the minimum number of levels of sequential logic from a given register to any assertion. Together, these metrics give the development team guidance about where to add more assertions.

After a design has been instrumented with assertions, the power of exhaustive formal verification can be brought to bear on the assertions, replacing most extended pseudo-random simulation and finding bugs that are missed by other verification methods. Although formal verification tools can exercise a design's behavior much more thoroughly than simulation can, they have their limits; for many complex assertions in large designs, these tools are unable to prove that no bug exists.

An additional assertion-based coverage metric, called proof radius, measures the amount of verification that was actually accomplished by the formal verification tool. For example, if the proof radius achieved is 200 cycles, then the formal tool has exhaustively proven that no bugs can be triggered within 200 cycles of the initial state, regardless of what stimulus is used. With proof radius as a guide, the development team can judge whether formal verification is complete and tape-out can begin.

The use of assertions has been proven to be tremendously effective in finding more bugs faster in large chip designs. At the same time, traditional coverage metrics have become inefficient and ineffective as designs have grown. Fortunately, advanced metrics tied directly to assertions are providing a new basis for effective coverage-driven verification. Using assertion-based coverage metrics, development teams can determine when the time has come to stop verification and tape out with confidence.

Curt Widdoes is chairman and CTO of 0-In Design Automation, Inc.