( ESNUG 375 Item 9 ) -------------------------------------------- [06/28/01]
Subject: ( ESNUG 372 #10 ) Verplex Vs. Formality "Data" Very Misleading
> With respect to the gentleman from ST's comments about Formality: here's
> some live data from Verplex-LEC for a just completed design.
>
> Design: about 44K gates with gated clocks and scan. (There were 2917
> comparison points.)
>
> a) Gate-to-gate comparisons run in approx 7 mins on an Ultra II-300MHz
> with 512MB.
>
> b) Gate-to-RTL runs in approx 57 mins on an Ultra II-440MHz with 512MB.
> The RTL and gates don't have exactly the same hierarchy either since
> some blocks get flattened in our synthesis tool.
>
> The above machines run Sun OS 5.6.
>
> - Tom David
> Cygnal
From: Umberto Rossi <Umberto.ROSSI@st.com>
Hi John,
When I reported my figure of ~2.5 hours vs inconclusive for 40K gates, I
meant to show the enhancement of Formality 1999.10-FM1.0 vs Formality
2000.05-FM2.0. For the same versions I reported also the case of ~500K
gates.
Now, 2.5 hours is NOT the typical run time for a 40K gate design, as it
may appear from the comparison between my case and Tom's Verplex numbers.
I have seen a *huge* range of equivalence checking performance over
designs of similar size due to how the design was implemented. You can
find examples - typically datapath - where execution times span from a
few seconds to inconclusive for nearly same design sizes!
I have in my regressions a significant number of designs, but providing
an average performance does not really make sense. I have found cases of
performance similar to Tom's, much worse and much better but, in order to
make an assessment, the comparison should be apples to apples.
I do not think it is really possible to define a set of independent test
cases to be tried on different products as it is for logic simulators. In
fact in the case of simulators, the final target is to minimize the number
of generated events, which represents a benefit for ANY circuit and features
a threshold for each circuit, whereas in Formal Verification world (not only
Equivalence Checking !) each circuit may feature an appropriate "ordering"
that makes the verification run in a few seconds rather than "infinite".
Hope this helps,
- Umberto Rossi
STMicroelectronics Agrate Brianza, Italy
|
|
