( ESNUG 400 Item 11 ) -------------------------------------------- [10/10/02]
Subject: ( DAC 02 #9 ) Three Users Defend Innologic's ESP-CV Symbolic Tool
> "Innologic sells a PLI that will turn your ordinary Verilog simulator
> into a symbolic simulator and can also add formal verification
> capability. In addition to signals taking on values of "0", "1", "X"
> or "Z" they can take on any arbitrary string as a value. If you have
> an AND gate and the inputs are "0" and "1", the output is "0", just
> like an ordinary simulator. If the inputs are "A" and "1", the output
> is "A". If the inputs are "A" and "B", the output is "A&B". If you
> have a lot of symbols, signal values can turn into big, ugly equations,
> which can get uglier with each new clock cycle. They say their formal
> verification tool will give you the simplest possible example of how
> an erroneous value can occur. They say they use very clever BDDs to
> allow signals to take on really big equations as values, but if you use
> enough different symbols for enough clocks the tool will run out of
> steam. Note however that since you are checking for all possible
> values of the pins with symbolic values on them, your simulation may be
> much shorter to effectively check your design."
>
> - John Weiland of Intrinsix
From: Mayank Gupta <mgupta@shromila.com>
Hi John,
We used the ESP-CV tool from Innologic quite extensively in my past company.
I wanted to offer a slightly different opinion of Innologic's ESP-CV tool
than what was said by John Weiland of Intrinsix:
1. ESP-CV does not turn your existing "Verilog simulator into a symbolic
simulator", but includes a symbolic simulator as part of the tool.
This is a plus as it does not "occupy" a typically constrained resource
such as Verilog simulator.
2. I agree, ESP-CV will run out of steam if you run "enough different
symbols for enough clocks". But the whole idea is to NOT run enough
clocks. Most datapath designs that we did were verifyable in 4
symbolic clocks + ~4 binary setup (fast). A few went to ~8 symbolic
cycles. In reality, I even had one design run ~1M cycle because it
had a unique sequential architecture.
3a. I used the Innologic ESP-CV tool for equivalency checking between
RTL (behavioral Verilog) and gate level (Verilog netlist) for full
custom 64-bit superscaler microprocessor with large on-chip caches.
We broke the design into ~12 functional datapaths and another ~12
associated control blocks. In our methodology, at the "floorplan"
block level the RTL (Verilog) implementation must match identically
to the "hand-drawn" custom logic (schematic capture). We verified
each of the above datapath blocks in both RTL and gate level netlist
using Innologic as a equivalency checker. We did the same for
synthesized control blocks, too. The only difference was that we
had to run more cycles to get adequate coverage. The control blocks
required more cycles due to sequential state machines while the
datapaths were generally straight forward.
3b. The other application for this tool was as a regression everytime
RTL or gate level changed for timing, resizing gates, LVS related
changes etc. etc. This regression was very effective as it would
pinpoint the erroneous change in minutes as opposed to hours of
functional vectors.
4. Usability: The tool is easy to use once you understand the purpose
and application of this tool. To start out we got a tutorial of the
tool. We used the default testbench generation feature to put together
the shell and that typically took care of ~75% of the manual tedious
work. For people who do cut and paste style editing it is quite easy
from that point to put together the rest of it. Next the designer
(knowledgeable person) goes in and puts the appropriate reset and
operating constraints. In reality, this should be very small for
properly coded RTL. The rest the tool takes care of it. In the final
stage, the circuit implementor simply generates a gatelevel netlist and
"checks-out" the RTL and testbench and types one command and gets
"Pass/Fail" indicator. I should also point out the "Failing Test
Vector" in binary verilog or VCD dump is produced for the failing case.
It literaly is a few cycles of simulation pinpointing the failure.
Personally, I am quite sold on the concept and simulation capability of this
tool as a equivalency checker. We found a number of bugs in the design at
block level that would have taken a lot longer to find on a full chip level.
Circuit designers actually prefer this tool for verifying initial design and
all changes. Also, since the setup and run is a lot simpler, it is even
preferred over formal verification.
- Mayank Gupta
Shromila
---- ---- ---- ---- ---- ---- ----
From: Jason Su <Jason_Su@pmc-sierra.com>
John,
As a circuit designer using Innologic's ESP for 2 years and recently having
a successful tapeout on a MIPS microprocessor, I see clearly what the
confusion and fear are in the mind of John Weiland of Intrinsix. Confusion
about what a symbolic simulator really is, and fear of new things. If you
first understand there are 4 basic types of verifications: SPICE, Verilog
or VHDL, Formal Verification (such as Chrysalis, Verplex, etc.), and
Symbolic; and what we do with each:
1. SPICE: analog simulation is accurate on devices but not on systems
due to drastic simplification often required to be made on the models;
its limited capacity and speed make it inappropriate for serving as a
logic verification tool for even a typical RAM design (even with the
most modification and simplification).
2. Verilog/VHDL: binary digital simulator for logic verification which
doesn't require high coverage, or CPU time isn't an issue.
3. Formal Verification: a tool to guarantee 100% coverage, if everything
in the design is straightforward like static logic; otherwise, like
SPICE, manipulations such as attribute labeling, black-boxing, etc.
are required. This is where you lose your coverage.
4. Symbolic: just like "2" having the coverage of "3" w/o manipulations.
So it does sound like what John Weiland said, "turn your ordinary Verilog
simulator into a symbolic simulator and can also add formal verification",
is not quite true. Symbolic simulation is no formal verification tool. It
is a simulator which makes covering all cases possible (especially with its
hierarchical compression).
- Jason Su
PMC-Sierra
---- ---- ---- ---- ---- ---- ----
From: Dennis Yau <dyau@t-ram.com>
Dear John,
It is quite interesting to read those comments on Innologic tools. From
my experience, I think it's more a front-end tool for the back-end
designers. I have been using ESP-CV from InnoLogic in my current company.
We used it for equivalence checking of our SPICE netlist against our RTL
model for the full custom design blocks including register files, memories,
caches and etc. ESP-CV requires very minimum logic modeling effort for
custom designed blocks. Most of the net-lists from schematic can just
directly go to the flow, for circuit designers who usually are
uncomfortable with modeling that is a big plus.
- Dennis Yau
T-Ram, Inc. San Jose, CA
|
|
