( ESNUG 376 Item 20 ) ------------------------------------------- [08/29/01]
Subject: ( DAC 01 #16 ) User Undoes Formality Jab; Synopsys Marketing Puffs
> "We are just about to get rid of our Formality licenses and go with
> Verplex. Not that it's a surprise, but Synopsys is totally lying when
> they say Formality doesn't use any of the same algorithms that DC does.
> Formality missed something in one of our chips that Verplex easily
> caught. If formal verification had been done that the module level,
> Formality would have caught (we later determined) the problem in this
> piece of DesignWare."
>
> - Duncan Halstead, LSI Logic
From: "Duncan Halstead" <duncanh@lsil.com>
Hi, John,
In the DAC trip report I stated that Formality missed a bug in a design that
Verplex easily caught. Regretfully, I didn't have all my facts correct and
I wanted to straighten things out. This was more of a methodology problem
than a tool problem. Gtech .db files were being used to do verification
against gates instead of the original RTL.
There was a width mismatch in an assign statement, and the Design Compiler
reader (HDL Compiler) made a translation error. Since the resulting HDL
Compiler output was the starting point for Formality, Formality could not
catch the problem. This issue has been resolved in the latest version of
DC 2000.11 SP2-2.
As a result of all this, I have also followed up with Synopsys to verify
that Formality really doesn't use the same RTL reader as Design Compiler.
Synopsys confirmed that prior to 1999.05 Formality and DC shared that same
RTL reader; however, Formality now uses a completely new, completely
independent Verilog reader.
If we had been doing things properly, John, this never would have been an
issue. So, I would encourage everyone to NEVER do your formal verification
from anything other than the golden source RTL and a gate level netlist.
- Duncan Halstead
LSI Logic
---- ---- ---- ---- ---- ---- ----
From: Robert Hoogenstryd <robertwh@synopsys.com>
Hi John,
You are right; the Formality team has been busy improving the product. Over
the last year, Formality customers have benefited from more that 10X faster
performance and 3X more capacity. In fact, recent customer benchmarks not
only confirm Formality's performance benefits, but highlights Formality's
leading 2K gates/MB capacity for the verification of very large SoC designs.
These improvements come from continued technology investments like Hier-IQ,
available now in the latest Formality release, FM 2001.08. Hier-IQ combines
hierarchical verification's performance and memory advantages with flat
verification's accuracy and ease-of-use.
- Robert Hoogenstryd, Formality Marketing
Synopsys, Inc. Mountain View, CA
============================================================================
Trying to figure out a Synopsys bug? Want to hear how 11,000+ other users
dealt with it? Then join the E-Mail Synopsys Users Group (ESNUG)!
!!! "It's not a BUG, jcooley@world.std.com
/o o\ / it's a FEATURE!" (508) 429-4357
( > )
\ - / - John Cooley, EDA & ASIC Design Consultant in Synopsys,
_] [_ Verilog, VHDL and numerous Design Methodologies.
Holliston Poor Farm, P.O. Box 6222, Holliston, MA 01746-6222
Legal Disclaimer: "As always, anything said here is only opinion."
The complete, searchable ESNUG Archive Site is at http://www.DeepChip.com
|
|
