'Deep' formal verification powers assertions

'Deep' formal verification powers assertions
By Curtis Widdoes and Richard Ho, EEdesign
April 23, 2002 (9:33 p.m. EST)
URL: http://www.eetimes.com/story/OEG20020418S0077

Over the last ten years, we have seen tremendous progress in technologies for formal verification of the behavior of RTL designs. Today, these formal technologies are vastly more thorough than simulation in finding complex functional problems. In this article, we discuss these technologies in the context of assertion-based verification, which has proven to be an effective way of applying formal verification in a mainstream ASIC design flow. In particular, we discuss a breakthrough technology called "deep dynamic formal verification" which promises to substantially improve the efficacy of assertion-based verification. Also, we suggest some useful metrics for comparing formal tools used in assertion-based verification.

Assertion-based verification
Assertion-based verification (ABV) methodology allows formal verification to be easily applied within an existing simulation-based verification flow. In ABV, the design team instruments the RTL code using simulatable assertions. Assertions are statements about how the design is intended to behave at the RTL level. The design team places assertions throughout the design -- on worry cases, inter-block interfaces and complex RTL structures -- wherever the protocols may be misused or the design intent may be incorrectly implemented.

First, the design team runs automatic RTL coding checks. Then, it simulates with the assertions in place. In our experience, a well-instrumented 1M-gate RTL design ends up containing one thousand or more user-specified assertions, most of them monitoring complex sequential behavior. This web of assertions usually catches lots of problems during simulation. Furthermore, since the assertions are embedded in the RTL code, they are always at work, even when the RTL is re-used or the test suite is changed. Assertions in an appropriate format can also be used with simulation accelerators and emulators.

After the design team fixes all the problems that can b e found using assertions in simulation, it moves on to formal verification. To find design bugs, formal verification technologies require some description of the stimulus that is legal at the boundary of the design under test (DUT). This description is called "constraints", since it constrains the formal engine to analyze only legal stimulus. Without constraints, a formal engine will report false errors instead of design bugs.

Constraints are a natural part of ABV. In simulation, the protocol on the boundary of the DUT should be thoroughly checked by assertions to ensure that neighboring logic stimulates the DUT correctly. These assertions describe all the illegal stimulus and thus contain all the information required to constrain formal verification. In ABV, the assertions on the DUT boundary are first verified in simulation. Then they are automatically transformed into constraints for formal verification.

For complex DUT interfaces, accurate monitors are required to watch the protocols and fla g problems. A standard interface monitor (for example, for PCI-X or AMBA) may contain more than one hundred separate assertions. A typical 1M-gate DUT contains several complex interfaces and thus requires several hundred assertions to fully constrain stimulus at its boundary.

Simulation of interface assertions/constraints turns out to be very important for formal verification. If the constraints are too tight, then the formal engine will simply fail to report bugs in the DUT -- without giving any warning to the user. A design can look bug-free to formal verification simply because of overly tight constraints! Simulating the constraints detects the problems -- any constraint that is violated during simulation is either a bug in the RTL (bad protocol) or a constraint that is too tight.

Formal verification
Within ABV, formal verification technology attempts, for each assertion, to either prove that the assertion can never be violated or find a stimulus sequence that violates it (a "cou nter-example") -- both while obeying the constraints. If neither a proof nor a counter-example can be found, then the assertion is called "indeterminate."

Basically, the objective of formal technology in ABV is first, to minimize the number of indeterminate assertions, and second, to provide feedback to the user about how thoroughly each indeterminate assertion has been verified.

Counter-examples have very high value to mainstream ASIC design teams. If the assertions and constraints are correct, then every counter-example represents a real bug in the RTL. If the stimulus for the counter-example is synthesized so that the bug can be exhibited in simulation, it can be tracked down and fixed by the design team. (Since simulation is so widely accepted as a debugging tool and as the final authority on RTL behavior, it is extremely important for any counter-example found by a formal tool to be reproducible using a standard RTL simulator.)

On the other hand, proofs have low value to mainstream ASIC design teams using ABV. Proofs don't tell the design team where to look for problems or what to do next. Only if essentially all of the assertions in a design are proven do the proofs have high value -- and even then, some assertions may be missing. A near-100% completion rate is feasible only for small blocks or for very simple assertions in a larger design. However, the best formal technologies today can prove at most about half of the complex assertions in a large, fully constrained design. Given proofs for half of several thousand assertions, the design team knows for certain only that all the bugs are in the other half!

Proofs and counter-examples require different types of formal-verification technologies. In ABV, a cascade of technologies is used to fully verify the assertions in the RTL, as shown in Figure 1 below.

Figure 1 -- ABV combines multiple technologies

The following technologies are used in ABV:

RTL Coding Checks ("super-lint") eliminate syntactic and shallow "netlist-semantics" errors.

Static Formal Verification filters out any simple assertions that can be proven without constraints.

Simulation with assertions exposes the bugs that are stimulated by the existing diagnostic tests.

Dynamic Formal Verification with partial constraints quickly finds bugs missed by simulation.

Deep Dynamic Formal Verification with full constraints thoroughly verifies assertions late in the design cycle (including post-silicon) when it is critical to expose every bug.

Static formal verification
Static formal verification (SFV) uses a variety of algorithms to prove that it is impossible to violate an assertion, starting from the reset state of the DUT, without violating the constraints. Commercial SFV proof algorithms are primarily based on model checking, symbolic simulation and SAT-based induction. (Theorem proving algorithms require too much human intervention.)

In order to h andle complex assertions in large designs, SFV proof algorithms usually need to abstract parts of the DUT, making it appear to have extra, unintended behavior. If a proof is possible after abstraction, then the proof is valid, but if the proof fails, then the abstraction generally prevents an accurate counter-example from being produced.

Note that for very simple assertions or very small designs -- about 20K gates -- SFV algorithms can sometimes provide counter-examples as well as proofs. In particular, SFV can provide counter-examples for some types of simple, automatically inferred assertions, such as not-simultaneous-set-reset and not-bus-overdriven, before simulation begins. These types of assertions are focused on low-value bugs and are outside the scope of this paper.

Since SFV produces primarily proofs, its value in ABV is only to reduce the number of assertions that need to be verified by other formal technologies.

Dynamic formal verification
Dynamic formal verification is fo cused on finding counter-examples (bugs), not proofs. To maximize efficacy, it starts with full DUT states taken from normal simulation traces, or "seeds," hence the term "dynamic."

The basic DFV algorithm analyzes every seed. Given a seed, for each assertion it uses an ultra-fast bounded model checking (BMC) algorithm to exhaustively search for counter-examples that can be produced within a few cycles starting from the seed, respecting the constraints. It reports any counter-example found and moves on to the next assertion, then to the next seed.

The depth of the exhaustive search around each seed, in cycles, is called the "proof radius." For indeterminate assertions, the proof radius represents comprehensible feedback about the level of verification. The larger the proof radius, the more thorough the verification.

Intuitively, starting from states generated by simulation should help to find bugs. Empirically, it helps a lot. A good simulation test takes the DUT through lots of corner case s, many of which are difficult to reach using formal algorithms alone. By starting at these corner-case states rather than starting from a reset state, DFV can find bugs using a much smaller proof radius. By using a BMC algorithm optimized to run ultra-fast for small proof radius, DFV can analyze a large number of seeds. Traditional BMC algorithms have not been optimized in this way and are too slow to be usable for DFV.

Even with a proof radius as small as five cycles, DFV performs an astonishing amount of verification, measured in terms of equivalent simulation cycles. To be conservative, assume that the DUT has just 10 inputs that can affect the assertion. In that case, there are 1024 possible input patterns each cycle, so there are about 10¹⁵ possible stimulus sequences five cycles deep. To be exhaustive to a proof radius of five in simulation, similar to DFV, all 10¹⁵ 5-cycle stimulus sequences would need to be simulated (see Figure 2). Of course, in typical DUTs, assert ions can be affected by a lot more than 10 inputs.

Figure 2 -- DFV is exhaustive up to a small radius

Deep dynamic formal verification
Deep dynamic formal verification (DDFV) is a revolutionary technology for finding counter-examples. Like DFV, this technology starts with a seed from simulation (hence it is dynamic) and exhaustively searches at large proof radii until it either finds a counter-example or consumes a user-settable time budget. However, DDFV uses a new BMC algorithm that is capable of reaching much greater depth than DFV, given long run times.

Fundamentally, the BMC problem is NP-complete, so all known algorithms are exponential in the proof radius. However, DDFV uses optimizations specific to ABV and RTL circuits in order to achieve tremendous reductions in the time required to verify assertions at large proof radii. In practice, these optimizations allow exhaustive verification of a typical complex ass ertion in a 1M-gate DUT out to a proof radius of 50-150 cycles within 1,000 seconds. At this speed, however, DDFV can be used to analyze only a limited number of seeds.

DDFV is capable of achieving a truly unbelievable level of verification. As the proof radius grows, the number of inputs that can affect an assertion grows as well. Assume that the DUT has 300 inputs that can affect the assertion at large proof radii. In that case, there are 10⁹⁰ possible input patterns each cycle, so a proof radius of 100 cycles is equivalent to about 10⁹⁰⁰⁰ cycles of simulation (see Figure 3).

Figure 3 --- DDFV is exhaustive up to a very large proof radius

Fundamentally, every assertion is either provable (with unbounded CPU time and memory) or has a counter-example. Given that proofs are not tractable for many of the complex assertions in large designs, DDFV provides a practical alternative. DDFV is capable of achieving such a large proof radius that it will almost always find a counter-example if one exists. Practically speaking, for mainstream ASIC design teams using thousands of assertions, exhaustive verification out to a proof radius of 100 cycles is tantamount to a full proof. Also, the proof radius achieved for an assertion serves as comprehensible feedback about how thoroughly the assertion has been verified.

Since DDFV is capable of finding counter-examples as well as "near proofs", it subsumes most of the functionality of static formal tools.

Metrics for DFV and DDFV
To first order, the tool that finds the most bugs is best. If the assertions and constraints are correct, then every counter-example is a bug. Therefore, the most important metric for formal tools is the number of counter-examples found.

Both dynamic formal and deep dynamic formal technologies are necessary in order to maximize the number of counter-examples found. As with simulation, increased speed leads to more t horough verification. At 0-In, we are constantly working to improve two metrics in order to maximize the value that these formal technologies deliver to ABV users:

The objective of dynamic formal is to analyze as many seeds as possible at shallow depth while the constraints are still incomplete, allowing the user to quickly find bugs that simulation missed. The appropriate metric for DFV is thus seeds per second per assertion at a small fixed proof radius (for instance, 5 cycles).
The objective of deep dynamic formal is to analyze a few seeds to the greatest depth possible, allowing the user to find counter-examples for any remaining deep bugs after constraints are complete. The appropriate metric for DDFV is thus the proof radius achieved within a large fixed time (for instance, 1,000 seconds per assertion).

Summary
ABV enables formal verification technology to be easily applied within a mainstream, simulation-based ASIC verification flow. In ABV, the RTL is i nstrumented with assertions, then the assertions are verified in simulation, then formal algorithms are applied in the presence of constraints. Formal algorithms produce proofs and counter-examples, of which counter-examples have much more value.

For many complex assertions in large designs, proofs are intractable. Dynamic formal verification uses ultra-fast bounded model checking technology to find counter-examples by skimming a large number of simulation seeds. Deep dynamic formal verification uses a revolutionary deep bounded model checking algorithm to find counter-examples at great depth from a limited number of seeds. It also provides a level of verification that is tantamount to proof for the remaining indeterminate assertions. Both dynamic and deep dynamic formal verification provide feedback about how thoroughly each assertion has been verified, in terms of "proof radius."

Dr. Curtis Widdoes is a co-founder 0-In Design Automation, currently serving as Chairman of the Board and CTO. H e is widely recognized as a pioneer in the EDA industry, having founded two other successful EDA companies -- Logic Modeling Systems (1987) and Valid Logic Systems (1981). He received a B.S. in engineering and applied science from the California Institute of Technology and a Ph.D. in computer science from Stanford University.

Dr. Richard Ho is a co-founder of 0-In Design Automation. Dr. Ho received a Ph.D. in computer science from Stanford University, where he based his thesis, "Validation Tools for Complex Digital Designs," on practical applications of formal methods. He received M. Eng. and B.Sc. Microelectronic Systems Engineering degrees from the University of Manchester Institute of Science & Technology (UMIST), England.