( ESNUG 371 Item 11 ) ------------------------------------------- [05/23/01]
Subject: ( SNUG 01 #15 ) STMicroelectronics Defends Synopsys Formality
> 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.
>
> - from the SNUG'01 Trip Report
From: Umberto Rossi <Umberto.ROSSI@st.com>
Hi, John,
I'm the Formal Verification Manager in STMicroelectronics at Milan, Italy.
Formality is by far our most popular tool for the purpose of the Equivalence
Checking in STMicroelectronics worldwide. Formality is our official tool in
the RTL-to-Layout flow, performing RTL-to-Gate and Gate-to-Gate comparisons.
It is packaged in our standard design flow in order to perform Gate2Gate
comparisons with minimal intervention from the designer's side.
Formality has validated hundreds of designs for us in every market covered
by ST -- consumer, telecom, automotive -- in every product line -- ASIC,
microcontroller, set-top-box, graphics, combos and SystemOnChip -- with any
available technology -- .35u, .25u, .18u, .13u -- of sizes up to 2 Million
gates.
Formality has been proven effective for us with a well known synthesis flow
as well as other custom flows -- especially in data-path design.
In Formality, we find many features that are necessary for the verification
flow starting from the library level on up to designs needing sophisticated
setups aimed at the time & power convergence domain (e.g. Inverted Compare
Points, Asynchronous Bypass, Gated Clocks, Retiming, Constrained
Verification.)
Concerning run time performance we have seen a significant improvement in
the recent year and some designs that used to be inconclusive now succeed.
I'm talking about Formality 1999.10-FM1.0 vs. Formality 2000.05-FM2.0.
I can give you some examples: one design was a RTL-to-Gate ~40K gates. It
used to be inconclusive and now passes in ~2.5 hours. Another Gate2Gate
design that was inconclusive now passes in 2 days. In this case I have
just the container sizes around 20Mb (~500K gates). Often divisions send
us containers in order not to make the code available. In effect this is
a strange case for Gate2Gate but I think that designers took the first and
the last version of gate netlists through a very complex flow.
In these experiments we run Formality on the same machine: Sun Solaris
248MHz with 3.5 Gb memory.
Concerning custom design, we have asked Synopsys to address also the
verification of simple memories. Duplication will play a major role in
0.18 um and below and we are asking specific features to have it better
supported.
Concerning comparison with competitors our analysis is a bit out of date
although we think that a competitive race is the best challenge to get
the best performance out of the market. Other formal products definitely
have less features and they seem limited to streamlined design flows.
- Umberto Rossi
STMicroelectronics Agrate Brianza, Italy
|
|
