( ESNUG 387 Item 15 ) -------------------------------------------- [01/23/02]
Subject: ( ESNUG 386 #6 ) Formality And Verplex Each Have Their Own Issues
> I was successful in running both tools and they both gave me the correct
> results. However, Formality was easier to use. It had better debugging
> capabilities, and I liked the fact that it has a TCL interface. The
> performance results also clearly favored Formality. In verifying a 700K
> design, approximately 40% RAM (using Magma P&R), Formality was 25% faster
> and 4X better in capacity over Verplex on the same design.
>
> Our team did decided to buy Formality because of our eval results.
>
> - [ From The Land Of Pokemon ]
From: Jay Pragasam <jlk@brecis.com>
Hi John,
Based on our usage I think Formality and Verplex LEC both have advantages
and drawbacks on their own.
1. On flat netlists, both Formality and LEC run more or less the same
time, but setting up Formality is more simpler, if you are a person
who hates the renaming culture of LEC.
2. The debugging capabilities to me are not drastically different. Both
EC tools present the same debugging utilities with different wrappers.
3. But doing hierarchical verification with Formality is a pain. It is
so nice with LEC that we can write out a hierarchical script and also
the tool takes care of keeping the whole design in memory and traverse
into every submodule for verification. In Formality you must manually
create scripts to verify every submodule. Since black boxing isn't
that easy with Formality, we have to take extra effort to tell the
tool that I have verified the submodule and so treat it as a black box.
Also if you have clock trees, then the user has to say that the
different clock nets going into the submodule are all the same and one
clock when going hierarchical with Formality!!
4. Formality is BAD in handling parametrized designs. It can't do the job
if there are a lot of mathematical manipulations of parameters whose
value is used inside the design. You have to tweak the RTL to make the
tool happy. Synopsys claimed that it was fixed in 2001.08-SP1, but
doesn't appear so. Maybe in the SP3 version.
Both EC tools sweat big time if there are additions like A+B+C+D+E. They're
not really smart about the implementation and often fail if it's implemented
as (A+D)+(B+C)+E for example.
- Jay Pragasam
Brecis Communications
|
|
