( ESNUG 394 Item 4 ) --------------------------------------------- [05/29/02]
Subject: ( SNUG 02 #10 ) Two Evals Of Verplex Tuxedo vs. Synopsys Formality
> We recently evaluated Verplex vs. Formality. Our conclusion was that both
> tools are equivalent, and we decided to go with Synopsys mostly for
> business reasons. We already taped out two designs with Formality and
> although we found some bugs and some limitations (mostly in the
> hierarchical RTL-to-flat-gates domain), we are very happy."
>
> - Nir Sever
> Zoran
From: Uwe Koenig <Uwe.Koenig@eed.ericsson.se>
Hi John,
Two years ago, I evaluated Verplex 'Tuxedo', Mentor 'FormalPro' and Synopsys
'Formality'. I tested RTL-to-gate as well as gate-to-gate. The outcome was
that we bought Verplex.
The main PROs of Tuxedo are that it is easy to learn and easy to use, and
that you really SEE what happens, or what the problem is. It's just
intuitive. You use the same tool for verifying and debugging, you can
switch the GUI on and off, you can even change the hierarchy level while
the tool runs, let the tool generate scripts for hierarchical comparison,
and you have shorter runtimes and memory usage than the other tools.
Another aspect is that it runs very stable, while Formality often crashed
(Synopsys probably they solved this problem now, this was 2 years ago I did
this eval.) Also, it was impressive that Verplex FAE needed only 20 min to
install the tool, then we could start working.
Today I also use Chrysalis 'Design Verifyer', and it works OK, but whenever
problems occur (and we had some with the VHDL reader) I switch to Verplex
'Conformal' which is the new version of Tuxedo, to understand better what
exactly the problem is. Design Verifyer has coding restrictions, since it
doesn't understand VHDL-93 or later. They announced it for the new version
in autumn. Mainly I have the impression that all suppliers of FV tools try
to get to the point where Verplex already is.
- Uwe Koenig
Ericsson Eurolab Deutschland GmbH Germany
---- ---- ---- ---- ---- ---- ----
From: [ A Bridge Too Far ]
Hi, John,
Here is our benchmark of Formality vs. Verplex LEC. Please keep me anon.
Formality version 2001.06 from Synopsys
Tuxedo - LEC version 3.0.1.a from Verplex
Test Cases:
1. VHDL to Verilog: (gate to gate)
Size: 110K Gates
CPU Time Memory Usage Compare Points Result
Formality 386.13 sec 92.09 MB 6828 Pass
Tuxedo-LEC 1373.05 sec 90.62 MB 6718 Pass
2. Pre-route to Post-route: (gate to gate)
Size: 750K Gates
CPU Time Memory Usage Compare Points Result
Formality 1800.64 sec 460.02 MB 37034 Pass
Tuxedo-LEC 2867.12 sec 463.12 MB 36585 Pass
3. Before/After Clock tree insertion: (gate to gate)
Size: 1M Gates
CPU Time Memory Usage Compare Points Result
Formality 1188.26 sec 379.18 MB 49849 Pass
Tuxedo-LEC 1526.73 sec 527.53 MB 49507 Pass
Comparing Tools:
In all cases Formality was faster than Tuxedo-LEC. Formality ranged from
3.5X to 1.3X faster than Tuxedo. Tuxedo matched or used more memory than
Formality. Tuxedo used 1.4X more memory than Formality on 1M gate design.
Both tools crashed several times for unknown reason. It happened to
Formality more often. For Tuxedo-LEC, it will generate some hidden files
that you can email back to Verplex to see what caused the crash, but for
Formality, you will only get message "segmentation fault" and a core file
when the tool crashed.
Formality accepts more formats including Synopsys .db & .lib (for library).
Tuxedo-LEC can reports more stuff like Black Box, Modules, etc. That could
be useful sometimes.
Formality relies on naming matching. If instance names are very different
between two netlists, very few compare points can be matched. Tuxedo has
better matching engine.
Formality cannot access netlist. Tuxedo uses Debussy as their debug system.
User can refer schematic and netlist easily. Debussy will break into the
macro. You will see dff_udp, and other and gate, or gate, etc. Formality
keeps the original cell in the schematic, for example, SDFERQ1.
Formality can remove/isolate any sub-cone from schematic to make it easier
to debug. Tuxedo cannot remove any part of schematic.
Formality can save design in binary format. So next time you use this
design again, you can just read in the binary format without doing
everything from scratch. Tuxedo needs to do everything from scratch.
Formality doesn't know which one is the top-level design, user has to
specify. Tuxedo will know the top-level design name.
Formality is one of Synopsys tools, if Design Compiler didn't synthesis
correctly, Formality will not be able to find out since they use the same
synthesis engine. Tuxedo is a third party tool. Better for design that
is synthesized by Synopsys.
- [ A Bridge Too Far ]
|
|
