( DAC 00 Item 16 ) --------------------------------------------- [ 7/13/00 ]
Subject: 0-In '0-In Search', Silicon Forest Research 'Assertion Compiler'
DEFENDING THE WALLS: The mystery date of DAC'98 (where they got everyone's
attention with no product but some awful big promises) was 0-in. Since
then, they've gone through some heavy ups and even more painful downs to now
find themselves in the unexpected position of being the Olde Guard for
formal verification type of tools. Their long time rival, Silicon Forest
Research still seems to be playing catch-up, too.
"0-in was very disappointing this year. They were giving the SAME spiel
that they were giving back in DAC '98 two years ago. Almost no new
features or ideas. Seems to me that it took them a LOT longer to get a
stable tool than they had originally anticipated. Still has a lot of
promise, though."
- an anon engineer
"0-In Design Automation 2 stars (out of 3 possible)
0-In Search
0-In makes a "white-box" formal verification tool which combines
elements of simulation and formal model checking which examines a
simulation trace of a design and explores the potential state-space
which can be reached within N vectors of the simulation trace. 0-In
provides a library of over 50 different checkers which can be
implemented in the code using special comment statements or can be
included via a separate checker control file.
The checkers are used to instrument the code, a simulation is then run,
and the results are then "amplified" by the tool to explore the design
and identify potential problems. VCD waveforms can be generated and
dumped which demonstrate the problem areas identified during the
amplification process. The checkers are implemented using Verilog
source code and typically impose a 15-20% runtime overhead. Of all the
companies promoting so-called assertion checker or formal checking
tools, I found the 0-In tool to be the most mature and have the most
assertion checkers of any of the different vendors."
- an anon engineer
"Silicon Forest Research 1 star (out of 3 possible)
Assertion Compiler
SFR also provides an assertion checking tool called Assertion Compiler.
Their premise is that the most common errors found during debug are not
the ones that require the most debug effort (things like datapath
computation errors, control state logic errors, etc.) Instead, the
bugs which cause the most effort to debug are more subtle and are likely
to belong to one of two groups; (1) race conditions resulting from event
order ambiguity, and (2) simulation/synthesis mismatches. Assertion
Compiler is PLI based and is run as a background operation during a
normal simulation run. Currently, only NC-Verilog and Verilog-XL are
supported albeit VCS support is planned in a future release. Going
through a PLI interface typically adds a 1.5 to 5x performance penalty.
I still struggle to see why simulation is needed for several of the
"bug" classes that are supposed to be detected by this tool.
Furthermore, the quality of the checks are highly dependent on the
quality of the test vectors which are applied during the simulation
run. Examples of some coverage checks are as follows:
- multiple drivers
- floating bus
- read operation while floating bus
- write/write operation without an intermediate read
- Latch an x or z into a state variable
- Read an uninitiated value
Due to the ambuguity in the Verilog spec, race conditions are indeed
often difficult to find and debug. On the other hand, simulation
mismatches with synthesis are often the result of poor coding styles
which can be handled adequately by static lint checkers and other
purification tools which don't require simulation. The tool is still
evolving, but until more sophisticated assertion checkers are available,
I don't have a strong feeling about the capabilities of this tool."
- an anon engineer
"0-In ("zero-in" - www.0-In.com) got a lot of attention from verification
wienies last year. 0-in calls normal functional verification "black
box", since stimulus and response are at the I/O. They call their
technique "white box verification", since they have checkers embedded
in the code. Their claim is that black box checking is the best
technique for finding high level functional problems early in the design
cycle. Later in the design cycle, when people are looking at odd corner
cases, they say their technique is far superior. Their Check program
identifies places where a bug is most likely to first appear, like
registers shared by more than one controller. It adds hundreds of
checkers per 100K gates of control logic. These check for common bugs;
for example, overwriting data without using it. Because the checkers
are internal, they can find bugs that never propagate to the outputs.
There is a library of over 30 checkers, and the user can customize
checking, for example ignoring data loss during pipeline flush. They
are trying to find odd corner cases that are generally caused by two
things interacting, like a FIFO filling up on the same clock as a mode
change. In addition to checking internal states, they generate new
tests using what they call a directed search methodology. They take a
signal trace from a simulation, use a formal verification tool to find
interactions that you almost found between controllers, and generates
new vectors that branch out from your existing traces. It hops back and
forth in time (in your trace file) looking for different controller
interactions, so these incremental simulations are supposedly not very
time consuming. The tool currently only support synthesizeable Verilog.
VHDL is due 3Q2001 (Modeltech only)."
- an anon engineer
|
|
