The problem with assertion checkers.

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 3.15, Item 8.0)

From: Richard Ho

This description of 0-In Search is incorrect. Actually, 0-In Search
performs an exhaustive analysis of ALL input combinations, while
obeying input constraints. 0-In Search uses a technology called
Dynamic Formal Verification (DFV). The key difference in DFV from
traditional formal verification is that the exhaustive analysis is
bounded (so that capacity limits are not exceeded). The formal
analysis is then repeated from many different initial states. This
allows the formal analysis to be effective in different parts of the
state-space of the design. The end result is formal verification that
is usable with much larger designs than traditional formal
verification.

By giving DFV many initial states from a simulation, DFV can find bugs
that traditional formal verification cannot. Traditional FV spends
large amounts of computational effort on paths that are of little
interest. This limits the depth that can be searched. However with DFV
you can focus only on the areas that are of interest to you, allowing
deeper and more meaningful results. DFV uses the same algorithms as
static formal verification, it just applies them in a way optimized to
find bugs in large designs.

Using assertions as part of a full ABV methodology that includes
simulation, formal analysis and maybe even hardware emulation has a
clear benefit -- reducing the amount of time needed during the last
stage of verification (sometimes called "extended verification") when
the bug rate is being monitored for tape-out. Tools such as 0-In
Search find more bugs faster using fewer directed simulations. The
engineering effort spent on each directed simulation is leveraged and
amplified to find more bugs. End result is that the bug rate drops
faster and projects can tape-out sooner.

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.1, Item 3.0)

From: Jeff Li

It is nice learning from the insiders. So, DFV (0-In Search) can miss
bugs in 2 more ways than formal verification theorectically can: (1)
by starting from only selected initial states, and (2) by finishing
within limited times. It is always good to know the truth though the
truth may hurt or help.

Exhaustive verification sounds positive but it also has a negative
side. It normally implies no meaningful progress at all unless the
time and computer memory allows reaching the final conclusion. This
black-white style of success brings more undesired risks than the
gradual style of success in simulation. To reduce the risk of zero ROI
of any effort, people have to use exhaustive methods on small blocks
or on low level features.

0-In Search breaks the big success of exhaustive verification of a
property/assertion into smaller successes by going from one initial
state to another initial state and by going from one time limit to the
next time limit. If some of the successes are not achieved, the other
successes can still tell something about bugs' existence.

This breakdown of exhaustive verification more or less widens the
possible application of formal verification to larger blocks or to
higher level features. Any further steps away from exhaustive
verification may do even better.

What I said above can be interpreted as that missing bugs is good. At
least, more tools in the kit can be better than less. According to the
complexity theory, it is impractical to assure catching all bugs. Any
tool completely betting on catching all bugs is missing the
reality. The nature of verification has to be getting as close to the
ideal as possible, and the tools should not prevent engineers from
deciding what bugs are more critical than others.

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.1, Item 3.1)

From: Andrew MacCormack

> I'm not yet familiar with any tools that support Sugar-based
> assertions...

NCSim 4.1 is now released and includes native support for inline Sugar
assertions as comments in Verilog and VHDL. There is also extensive
support for them in the GUI and waveform viewers. I haven't tried it
yet myself, but it looks pretty exciting!

Incidentally, if you're looking for assertions for an AMBA AHB setup,
http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ps/Paper_80.pdf
gives an interesting starting point.

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.2, Item 3.0)

From: Ben Cohen

> NCSim 4.1 is now released and includes native support for inline
> Sugar assertions as comments in Verilog and VHDL.

I had the opportunity to play with NcSim 4.1 on Linux, and I can tell
you that Cadence did an outstanding job at integrating Sugar into the
NcSim toolset. You have the compiler, the debug environment, putting
assertions on waveforms, seeing with the browser information about the
assertions. It's really a super commendable job!

I believe that Sugar type of ABV is very helpful in the verification
process, not only form a monitor/simulation standpoint, but
particularly from a documentation, spec requirement standpoint because
it really causes a user to THINK about the requirements of the design
by expressing those requirements in a concise manner. It also
facilitates code reviews. Coupling Sugar definitions with Static
Formal Verification (SFV) and/or Dynamic FV (DFV) is icing on the
cake!

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.2, Item 3.1)

From: Foster White

> It is nice learning from the insiders. So, DFV (0-In Search) can
> miss bugs in 2 more ways than formal verification theorectically
> can: (1) by starting from only selected initial states, and (2) by
> finishing within limited times. It is always good to know the truth
> though the truth may hurt or help.

DFV can miss verification combinations that can include invalid
verification space. If verification space is defined as a function of
inputs, state elements and time (or clocks in synchronous designs),
then there are combinations of the state space that are invalid. That
is, the design can never and will never have that combination of state
conditions (such as multiple bits on in a one-hot state machine).
Otherwise, you could randomly preset all state elements and inputs,
clock the simulator some number of clocks and get the most effective
use of simulator cycles. The problem is that there are too many
invalid combinations that result in countless hours of debugging "non
bugs." 0-In Search eliminates invalid state space combinations by
sampling those state combinations from simulation of the design. If
the state space is invalid, is that considered a bug? I would not
consider those "misses" as bugs. Yes, there are bugs that can be
missed, but there are also invalid combinations that will be avoided.