Why Formal Verification Should Be Part of Your Verification Plan

SoC Design, Design Verification, ASIC Design
Mar 23, 2017 7:27:00 AM

Designing an ASIC that is free of functional bugs is an important requirement for first spin success. Yet as designs grow larger and more complex, the goal of 100% functional coverage using traditional simulation based techniques becomes increasingly more difficult to achieve. The vast number of directed tests that would have to be written to cover all the functional behavior of a large SoC makes it impossible to exhaustively simulate most modern ASICs. Other testing strategies can help, such as:

developing use cases to flush out performance or complex sequencing bugs, and
using randomly generated tests to bypass designer bias, potentially exposing unanticipated problems.

But even with these strategies, long simulation times will make it practically impossible to exhaustively test a design using simulation alone. Eventually you hit a point of diminishing returns where further progress becomes increasingly more expensive.

simulation-based-verification-to-achieve-coverage-diminishes-over-time.png

Figure 1: Ability of Simulation Based Verification to Achieve Coverage Diminishes Over Time

Clearly additional strategies are needed. At Intrinsix, we have been using formal verification as a successful adjunct to simulation based verification for years. Unlike simulation, formal verification proves design correctness with static analysis algorithms that:

use equivalency checking to compare a design against a known good referent, or
use model checking to prove that design properties and assertions are satisfied.

The latter is called property-driven verification, or PDV. Both of these techniques offer the promise of greater efficiency, and more complete coverage. Most importantly, they don't require the development of test cases. This has several distinct advantages:

long simulation runs are not required to obtain good coverage,
the verification results do not rely on the quality of the test cases; in fact the algorithms prove correctness for all test cases.

formal verification

As a consequence, formal verification eliminates the problem highlighted in Figure 1. After the first and second order bugs are flushed out, it takes increasingly more time to find the deeply hidden higher order bugs, causing diminishing returns on time invested. Eventually, management will have to weigh schedule and budget constraints against the risk of additional bugs in the silicon, and make an educated guess about when to stop testing. Formal verification takes the guesswork out of this, and eliminates the risk of bugs in the silicon.

But it doesn't come for free. To make use of PDV, designers must specify design intent, usually in the form of properties or assertions. These give the tools a formal basis to reason about the design, and to identify violations that signify problems or bugs.

Formal verification has traditionally been a high effort process, requiring specialized expertise - usually relegated to a user base of math majors and researchers. The techniques for specifying properties, and for running the tools were complicated and too esoteric for mainstream use. But recent advances in the art have rendered the tools much easier to use, allowing them to migrate into the mainstream. Property specification languages are now built directly into hardware descriptions languages; for example, SystemVerilog Assertions (SVA) is part of SystemVerilog, and is widely supported by verification tool suites. As a consequence, formal verification tools are readily available, and can be used by anyone looking for ways to reduce verification schedule and risk.

A good way to begin using this powerful methodology is to start small, and work up to more comprehensive use of formal techniques. This will increase the odds of realizing value from the technology and will allow the team to gain confidence in the new methodology. Small successes will lead to greater adoption. In time, the methodology can make measurable improvements in verification quality, coverage and schedule.

One place to start is with functions that don't lend themselves to comprehensive verification using simulation. For example, functions that have a large number of input combinations, but whose behavior can easily be modeled are good candidates for PDV. These functions are impractical to simulate exhaustively, but writing and placing properties in the RTL is relatively straight-forward, and will yield immediate benefits. As the technology begins to prove itself, PDV can be used at higher levels, such as at the interfaces between high level components in the design.

Not all functions lend themselves to formal verification. At Intrinsix, we have learned over the course of many projects where formal methods are successful, and where they fall short. We have worked with clients to identify sections of their designs that would benefit from formal methods, and have helped develop formal verification strategies for their projects. Used properly, formal methods can play a significant role in increasing verification coverage, reducing risk, and shortening the overall verification process.

Peter is a Technical Manager at Intrinsix’s Marlborough Design Center. As a verification architect he creates verification and coverage plans, implements and leads teams of engineers building environments based on SystemVerilog/UVM methodologies, and drives verification closure. Along with the experience of many ASIC designs successfully released into production and introducing the latest verification tools and methodologies into the Intrinsix verification flow, he is able to reduce product risk and schedule risk in the ASIC verification process.