( ESNUG 321 Item 4 ) ---------------------------------------------- [6/8/99]
Subject: ( ESNUG 320 #3 ) Actually, We Found Equivalency Checking Useful
> Here's where we were coming from when we were looking at Chrysalis. We
> were designing a 1 million gate design that had multiple clock zones
> ranging from 75 MHz to 180 Mhz with about a third of the design being
> RAM. This meant we had roughly 700,000 gates of custom logic to test.
> Like everyone else doing these big, massive ASICs, we were looking for
> alternatives to the SLOW task of running gate level functional vectors.
> We were looking to group a couple approaches to accomplish this task
> such as static timing analysis with "equivalency checking". As I
> recall, 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. Additionally, the indications were, that equivalency
> checking between RTL and GATEs runs very slow.
>
> The place where I can see equivalence checkers helping is with testing
> gates-to-gates technology translations of design -- like porting a 0.35
> um design to 0.18 um, or from vendor A to vendor B-- but we weren't
> doing that, so Chrysalis was pretty much useless for us.
>
> - Don Mills
> LCDM Engineering South Jordan, UT
From: "Anders Nordstrom" <andersn@nortelnetworks.com>
Dear John,
Having done an 850k gate design with very little gatelevel simulation I have
do disagree with Don that Formal Verification is not useful. RTL-to-gate
verification is certainly the most tedious task and you do have to do it in
pieces but the alternative, gatelevel simulation, isn't very pretty either.
We did equivalence checking on the same modules we did synthesis on and
they ranged in size from 5k to 30k gates in Chrysalis.
I agree with Don that at this point it is most useful at gate-to-gate
comparisons. This is not a small benefit though. You have to verify
insertion of test logic, clock trees, buffer trees and in-place
optimizations. At this point in the design cycle you can verify the
enire gatelevel netlist at once in a reasonable time whereas gatelevel
simulations with the full chip take days.
- Anders Nordstrom
Nortel Networks Ottawa, Ontario, Canada
---- ---- ---- ---- ---- ---- ----
From: [ Snoopy, Charlie Brown's Dog ]
Hi John,
Can you please keep me anonymous as we are currently evaluating some
formal verification tools.
It must be a while since Don used Chrysalis.
We've recently done an evaluation of Chrysalis Design verifier and it had
no problems doing an RTL-to-Gate equivalence check on a 500K design which
was broken up into 100K gate blocks. For Gate-to-Gate, the tool was able
to handle the entire design at once, without breaking it up into smaller
blocks. On a Sparc Ultra-2:
The RTL-to-Gate equivalence check took approx 3.5 hours.
The Gate-to-Gate equivalence check took approx 2 hours.
These are pretty impressive figures on their own. Even more so when you
take into account the users's inexperience with the tool and the fact that
the machine we used for the benchmark was not particularly powerful.
- [ Snoopy, Charlie Brown's Dog ]
---- ---- ---- ---- ---- ---- ----
From: Mike Bartley <bartley@bristol.st.com>
John,
Maybe it is time for Don Mills to look at equivalence checking again.
I am a verification manager at STMicroelectronics and also responsible for
equivalence checking for a large part of STMicroelectronics. (I am also
on the Boston SNUG Tech Committee, which is how I got your email, and I
couldn't resist the challenge offered by Don's posting).
At ST (and quite a few other companies now) equivalence checking is just
like air. Don is right that gate-gate proofs are easier and that technology
porting is an obvious application. But there are a number of other
applications. Specifically, what does RTL-Gate buy you?
- faster checking of gates than simulation does
- more complete checking of gates than simulation does
- earlier checking (i.e. you can check just a block rather than wait
for a simulation environment to run it in -- yes, this is just a flow
issue, but we find equivalence checkers provide an enhanced flow that
allows more checking at lower levels, finding problems earlier.)
We have automated most things here at ST -- so designers can just type a
single, short command to run their proof.
On the flip-side -- there are capacity problems -- but not as bad as you
suggest. Equivalence checkers work hierarchically, so large designs aren't
a problem if they have matching hierarchy. The main problems are:
- RTL to gates if there is not matching hierarchy. But flow can solve
this. Use an RTL to hierarchical-gates proof, then a hierarchical to
flat gates proof,
- RAM's remain hard. We still use simulation to do this, but we will
probably start to use symbolic simulation pretty soon.
- large arithmetic blocks are also hard. Most equivalence checkers run out
of steam on RTL-gates at around 17 or 18 bits.
- re-timed designs and duplicated logic (e.g. duplicating state for
physical considerations) can cause problems.
and of course there may be others that I don't see.
In conclusion, equivalence checkers are pretty mature now and are being
used by a lot of companies on a lot of designs. Currently ST has about 10
on-going designs that use Formality as part of their flow with only a few
problems.
- Mike Bartley
STMicroelectronics Bristol, UK
|
|
