( ESNUG 368 Item 11 ) -------------------------------------------- [04/12/01]
Subject: ( SNUG'01 #15 ) Howard On Avanti's Chrysalis "Design Verifier"
> EXIT WOUNDS: Out of the 27 e-mails I received on Formality, Verplex or
> Chrysalis: 22 were pro-Verplex; 5 were pro-Formality; and none were pro-
> Chrysalis. Years ago, Chrysalis owned the Equivalence Checking market.
From: Howard Landman <howard.landman@vitesse.com>
Hi, John,
I haven't had time to re-evaluate all the other guys. I'm too busy taping
chips out with "Chrysalis" (should be Avanti Formal now) Design Verifier.
I'd like to see the ability for it to handle retiming (pushing logic through
registers), but nobody really does it yet. Synopsys *claimed* Formality
would do it, but when I pushed I found out that they could only do it when
there's no feedback between pipe stages. (This was a while back and they
may have improved by now.) This covers 0% of the interesting cases.
(Ever heard of a 7 stage CPU pipeline with no feedback between the
pipe stages? Sheesh. Get real. Stall signals are a fact of life.)
I haven't *completely* automated our DV flow yet - I'd guess only 50-60% of
the modules go through with no manual intervention at all. The other ones
either need tweaks to the paths (use submodules in non-standard locations),
or need extra attributes to deal with things like one-hot state machines or
tristate busses. Working on submodules of the main modules also takes a
bit of hands-on to map pins before-and-after Clock Tree Synthesis and
scan insertion. It would be nice if this was a bit more automatic (for
example, if Apollo CTS automatically wrote out commands to map over the
changes it makes - I mean, these *ARE* both Avanti tools now, right?), but
it's not a major pain.
Anyway we routinely run Chrysalis RTL-to-gates and gates-to-layout formal
verification on all the modules (except PLLs, memories, etc.), and
gates-to-layout on the chip top level (the RTL and gates are the same at
that level so I can verify with "cmp" :-).
It catches simple errors much more quickly than regression simulation. It's
been especially useful when making ECOs for metal mask spins, where both the
RTL and gates have been hand edited. A couple of modules don't get to 100%
complete (1 or a few nets time out); I hope to overcome that soon.
The 3.0.1 release of DV seems a bit shaky though. They claim you don't need
to specify algorithm anymore, but I got excessive runtime on some modules
when I unspecified Aggressive Algorithm 4. I'm still using 2.5 (with AA4)
as our workhorse until I understand this better.
- Howard Landman
Vitesse Semiconductor Longmont, CO
|
|
