( ESNUG 329 Item 15 ) -------------------------------------------- [9/22/99]
Subject: ( ESNUG 321 #4 ) Extra 'Equivalency Checking' Hoops Not Worth It
> 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
From: Don Mills <mills@lcdm-eng.com>
But, Mike, these items "On the flip-side" I consider much more constraining
then you make them out to be. Maintaining hierarchy between RTL and GATE
is often much harder to do then just following a flow. I have often been
constrained to make hierarchy changes just to accommodate EDA and Foundry
tool requirements. The hoops I have to jump through are for Foundries
are tough enough without added additional tools with additional hoops.
Additionally, my designs have been RAM and arithmetic based. From my
perspective and yours, formal tools have many constraints that need to be
met to be used and are not applicable in some cases -- like the ones I have
been associated with.
- Don Mills
LCMD Engineering South Jordan, UT
|
|
