( ESNUG 331 Item 6 ) --------------------------------------------- [10/7/99]
Subject: ( ESNUG 321 #4 329 #15 ) Chrysalis, Formality, Verplex, Quickturn
> to do the equivalency checking between RTL and gates, Chrysalis forces
> you to have to break up your design in 5K to 10K gate blocks. Equivalency
> checkers do a sort of voodoo synthesis on RTL (to convert it to equations)
> and on gates (to convert that to equations) and then it compares both sets
> of equations. Go beyond 10K gates, and the tool chokes. So, doing the
> math, using Chrysalis meant we'd have to do comparisons of roughly 100
> 'blocks'. Seemed like a lot of work for very little return. Also, the
> indications were, that equivalency checking between RTL and GATEs runs
> very slow.
>
> - Don Mills
> LCMD Engineering South Jordan, UT
From: Howard Landman <HowardL@SiTera.com>
John,
Since Chrysalis Design Verifyer (DV) was a critical component of my
methodology for the R5900 processor (heart of the Sony PlayStation 2
"Emotion Engine" chip), and we even ended up buying a second license,
perhaps it would be of interest to explain what we did with it.
The earliest application was library verification. We ended up with as
many as 5 different Verilog models of each library cell: behavioral (reg),
behavioral (wire+assign), behavioral (primitive), structural, and
transistor. This may have been a few too many, but some were forced on us
because they were written by other groups and some we wrote ourselves to
get significant speedups in simulation.
Using DV, it was fairly straightforward to set up a library verification
script that ran all 5 libraries against each other pairwise. This was
overkill (4 verifications should have been enough to check 5 libs), but it
ran so fast (under 2 minutes per check) that I just couldn't see not doing
them all. The full set was run any time any library changed. We found
quite a few bugs this way, both early problems, and the more dangerous
"last minute fix" bugs when someone changes something close to tapeout.
Of course, at this point we were only using about 1% of the license. DV is
like Library Compiler sometimes -- one license could serve dozens or even
hundreds of users - -IF you're only doing easy stuff.
The second application was trying to verify the transistor level design of
our custom blocks (mainly datapath elements). We had a method to abstract
a gate-level description back from the actual transistors, and we tried to
verify that against the RTL. This was the hardest and least successful
application, but it wasn't entirely the tool's fault. The transistor-level
block designers had not been given any constraints such as "keep the same
hierarchy, instance names, and signal names whenever possible". So
naturally, being engineers, they changed all of the above. This effectively
screwed all of the built-in shortcuts that DV takes when trying to figure
out what to match up with what, and caused very long run times.
Despite this, it was a useful exercise. Even with those handicaps, we still
found around a dozen bugs. More importantly, several of those bugs turned
out to be ones that we would never have caught by simulation. Generally,
the kinds of bugs that were found most easily by formal verification were
different from the ones that were found most easily by simulation.
This stage was heavily CPU intensive though - some blocks ran for 40 hours.
It was this which led us to purchase a 2nd license, so we could do more
than one at a time.
But in the end, we had done RTL-to-gates for all the control logic (except a
small piece which had intentional logic loops) and some portions of the
custom blocks.
Third application: when we made a small change to one block which was not
*supposed* to be a functional change (for example a timing improvement) we
could verify it 100% against the old version by running only that module.
To do this via simulation, we would have had to build a full-processor (or
full-chip!) model, run a large number of vectors against that huge model,
and then have to settle for 90% confidence. Formal is much faster and more
thorough in this situation. Of course, not all changes fall into this
category, but we still saved probably 2 to 4 weeks times our entire compute
farm of regression simulation over the course of the project.
And finally, in the back-end, there were a number of transformations made
to the netlist, including clock tree, reset distribution, IPO, repeater
insertion, scan chain, etc. Some of these processes had subtle problems.
Although I was too thickheaded to see the necessity at first, by the time
we taped out successfully I had implemented a complete chain of pairwise
gate-to-gate comparisons. *Every* single step of backend processing had
the before and after netlists verified against each other. This took about
25 minutes per comparison (for about 100,000 gates of control logic -- we
didn't verify the datapath because it didn't change). Really cheap
insurance, if you ask me. And it saved our posteriors more than once. The
reason to do every step (instead of waiting until the end and verifying
once) is that, when something goes wrong, you want to find out ASAP, and
not a week later. And you want to know immediately *what* step failed.
Partly due to this work, and partly due to other extensive verification
efforts (such as booting Linux on a Quickturn emulation of the gates and
running multiple simultaneous applications!), the R5900 was functional
on first silicon, and the second tapeout effort was able to concentrate
on timing improvements to reach full speed. This too was successful.
Sony shipped development systems to game developers built with 2nd
tapeout chips. Not bad for the first commercial 128-bit microprocessor!
- Howard Landman
SiTera, Inc. Longmount, CO
---- ---- ---- ---- ---- ---- ----
From: [ To Have And Have Not ]
John,
I saw this posting on ESNUG about problems with Chrysalis. Have you looked
at Verplex? <http://www.verplex.com> Using it, we've found it runs at
least 10x faster and handles greater than 300K gate comparisons. The key
to getting equivalency checks working are:
1. pre-mapping all gate-vs-RTL state points (flip-flops) before
comparison
2. matching RTL hierarchy with gate hierarchy
3. correctly modelling your flip-flops (gate often sees them as two
latches)
We've eliminated gate-simulation with Verplex. Good luck with your million
gate designs and please keep me anonymous.
- [ To Have And Have Not ]
---- ---- ---- ---- ---- ---- ----
From: Mike Sullivan <mikes@dal.asp.ti.com>
Hi John,
I would have to disagree with Don in his comments that EC is not worth the
effort. Granted, EC vendors today are much more mature than they were just
a few years ago. And there is still a way to go to make all designers
happy with using EC, especially in handling some types of RTL. But let me
illustrate what another user is currently getting out of EC vendors.
On the most recent project I was involved in, cycle based RTL regression
took 2 weeks on an LSF queue of 100 shared CPUs. In context to a single
CPU, that would be 80 weeks of regression time. If event based regression
was used, that would equate to 5X these performance numbers. Using EC
vendors, the need for such full long regressions has been greatly reduced.
In a significantly shorter time frame, we have found numerous design
differences. And more importantly, the reasons why were quickly located
using EC debug capabilities. The differences found were the result of both
designer and tool hiccups.
Yes, today's vendors (and that's plural) are limited in their ability to
handle some types of RTL comparisons where the RTL is highly abstract or
too complex. And they admit that. We did not have our full RTL environment
under EC because of these limitations. But we did successfully apply it
where we could. For those areas where any type of RTL EC comparisons can
be applied, the gains fully outweigh any setup effort involved. Doesn't
one also put effort into setting up for hierarchical synthesis?
Outside of RTL, the two real strengths of current EC vendors are in the
areas of custom/library development and Gate2Gate. To solve the need for
speed, designs may have the requirement for custom circuit libraries. One
needs to ensure these custom circuits match up with the simulation views.
For Gate2Gate, Don is correct in saying it could be useful for technology
migrations. But in practice, Gate2Gate EC solves more than just that.
Especially now with a lot of the actual Gate optimization work being done by
the placement+router tools themselves. Gate2Gate EC becomes very important.
In our experience with both custom/library and Gate2Gate EC, similar gains
were achieved as with our RTL EC successes. Complete, fast, and static
results.
Not getting into a debate on which EC vendor is best, we use the two main
players, Chrysalis (Avant!) and Formality. They both have their pros and
cons, where in our environment, each is used in the area it has strengths
in. This may be compared to how multiple simulators could be used on a
design project to get the particular benefits of each. Example: cycle
based simulator for RTL simulations and event based simulator for any
required Gate simulations.
Overall, our mentality is that designer and computing resources should be
spent getting the RTL correct to begin with, not on any derivation of it.
Dynamic tools may still be required for things such as verification of
ATPG, multiple clock domains, and reset logic. But where possible, I'd
much prefer to stay in the static world. ;)
- Mike Sullivan
Texas Instruments Dallas, TX
|
|
