( SNUG 99 Item 31 ) ----------------------------------------------- [3/31/99]
DAVE? DAVE'S NOT HERE! Formality-The-Big-New-Change-In-The-Way-Designs-
Are-Verified has only *one* class scheduled??! Huh? Do a DejaNews
on Formality and you get lots of weird unrelated alt.religion.scientology
quotes. In the ESNUG archives, Formality is only mentioned in 5 letters;
and that was after it was announced. After that, nada, no bugs, no usual
user gripes, nothing. (In contrast, Module Compiler generated 21 user
letters in ESNUG and MC is a specialized tool for a niche market. Commonly
used EDA like Verilog or VHDL generates thousands of user letters.) For a
tool that's supposedly being used by so many different companies, Formality
should have generated more than a grand total of 5 user letters. At the
recent DAC'98, ten other EDA companies announced formal verification
products (along with Formality) to go against Chrysalis. The New Darling
at the time was the FV tool from Bell Labs EDA -- which Cadence later
bought. Maybe Chrysalis still mostly owns the formal verification market
with their Design Verifier equivalency checker? (See www.chrysalis.com)
Or maybe formal verification is more of an expensive EDA toy than a
required tool. All I know is that there is no external evidence that
Formality is being used by very many customers.
"Formal Verification:
A) Mike Barrett of ST Microelectronics - Formality
Good talk on applying Formality to 6 kinds of design problems (basic
synth, datapaths, backend, libraries, signoff, and migration).
Backend and migration are highest benefit. For migration, they
started with library cell compares and then higher level compares.
Positive feedback that formaility is easy to set up and use,
and debug. Still need tool experts on most runs he said, and
especially for debug. Worth it overall. Reduces gate level sims.
B) Chrystian Roy of LSI Logic - Formality
Wonder if he is any relation to Patrick Roy, the fabulous goalie of
my blessed Colorado Avalanche. Formality is the recommeded tool for
LSI's FlexStream process releases. Not required. 15 min to learn
gui. Good for gate to gate. RTL coming along. Scan bypass worked.
Clock tree bypass worked. Buffersize stuff worked. 650K gates with
hier took 3 hours & 1.16Meg mem. 800K gates flat took 30 min, but
tons of memory. Limits: multipliers, matching/finding compare
points, rtl to rtl.
C) ditched on 3rd guy. He was from ST Microelectronics as well. Looked
same talks. Saw a bit of David Black's Behavioral Compiler pitch.
Great as usual. Also saw some of Focus Enhancment pitch on run_proj
script. Great auto harness for simulation with hooks to cvs.
The one cool thing at the vendor faire was a new formal Verification
company called Verplex. Supose to blow the others away for speed and
memory uses."
- Peet James of Qualis Design
|
|
