( ESNUG 320 Item 3 ) ---------------------------------------------- [6/2/99]
From: Don Mills <mills@lcdm-eng.com>
Subject: Formal Verification Equivalency Checking Didn't Buy Us Anything
Dear John,
I just saw in EE Times that Avant! just bought Chrysalis. I see that as
just trying to keep up with the "Jones" or in this case Synopsys's. In
my prior job, we looked at Chrysalis 3 or 4 times over the years and just
didn't think using any equivalence checker would buy us much. (I guess
then, my following comments could apply to Formality, too. Oh, well.)
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
|
|
