'Deep' formal verification powers assertions

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).

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.