( SNUG 10 Item 12 ) --------------------------------------------- [04/15/10]
Subject: What 238 users think of Formality vs. Conformal
CHEAP VS. GOOD: If you look at answer 5 to this question, you might come
up with the conclusion that the equivalence checking business is split
roughly 50-50 between Synopsys and Cadence. WRONG. The reality is that
there's an awful lot of users who use both. (Read the user comments.)
The truth is that a great number of users get Formality for "free" in a
SPNS package deal (because it's distrusted so) and they gladly fully pay
for Cadence Verplex Conformal because its trusted more.
With regards to using Formality equivalence checking to check
Design Compiler's output, we think (choose ALL that applies):
1a- Having one vendor check its own work ain't too smart.
: ############################################### 47%
1b- We like having one vendor check its own work.
: ###### 6%
2a- Formality's is good stuff; we're happy to pay for it.
: ##### 5%
2b- Formality's free; we got it in a SNPS package deal.
: ########################## 26%
3a- Formality is fairly easy to use and bug free.
: ########### 11%
3b- Formality is a swamp of exceptions and a bug fest.
: ############### 15%
4a- Support for Formality is pretty good.
: ###### 6%
4a- Support for Formality is pretty bad.
: ######## 8%
5- We use Cadence Verplex Conformal instead.
: ################################################### 51%
6- We trust Conformal (choose: MORE or LESS) than Formality.
MORE : ##################### 21%
LESS : # 1%
Comments?
---- ---- ---- ---- ---- ---- ----
We use both, and both have been useful to catch bugs.
In the past, Conformal was the preferred choice (not necessarily for
reasons of trust); currently the balance is slowly shifting.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
I'd say it's useful to have *both* Formality and Conformal. I don't
have a problem with Formality checking DC. It's marketing FUD to
think they use the same algorithms. It's pretty obvious after using
it that they don't.
It's easy to use in the sense that the commands & scripting language
are pretty straightforward. But it's always a release or two behind
DC in terms of the synthesis algorithms that it can verify. (See my
previous email about needing to work with a Synopsys AE for 3 months
to debug all the LEC on a complex chip.)
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Thing is, we used to use DC for synthesis and Conformal LEC for formal
verification, but that stopped working pretty much with DC Ultra which
makes optimisations that Conformal LEC can't follow. I've switched to
RTL Compiler and so far I'm content. Not enthusiastic, but satisfied.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Hey, it's free; we got it in a SNPS package deal. Would prefer
another vendor for formal equivalence but have reasonably good
confidence in Formality.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We used to have both Conformal and Formality, got rid of Conformal
(cost reasons), but may bring it back since Formality isn't a very
independent checker for DC.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We use Formality sometimes to debug Conformal bugs.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We have licenses for Formality and Verplex but use Conformal all the
time unless it doe not compare for some reason.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Even though we use Formality, we would like to also use Conformal as a
cross check. Also given complex power island flows with different power
formats, enabling both verification tools and cross checking their
results is necessary.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Occasionally we will use Formality on re-timed circuits, but our
standard flow uses Verplex.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
I don't have a complete distrust of Formality but since we have
Conformal it's good to get the independent check. When I last tried
Formality the runtimes were much worse than Conformal.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Having one vendor check its own work ain't too smart. However, we
still use Formality. Proven to be good, reliable, so far. Very
important for ECO work.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality checking on DC -- The blind leading the blind.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We are Conformal users for many years because of having one vendor
checking the other and because Conformal is seen as a better product.
Lately we found the difference between Conformal and Formality has
narrowed (seems that Conformal gets mixed up by DC's optimizations).
We are now contemplating a change. (Formality is cheaper)
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality sucks at actually doing logic-to-logic comparisons. We only
use it for an initial RTL-to-netlist comparison, and we have to jump
through hoops to make this happen.
Essentially Formality will only work if we keep all design hierarchy and
go really easy on optimizations. Hence we output a netlist directly
from mapping, run a comparison, then take that netlist and optimize the
heck out of it, and run it through back end. Then we compare the
initial netlist to the final with Conformal. (Formality doesn't stand a
chance at doing this.)
We always have to worry that some RTL parsing is equally wrong in both
DC and formality, however we haven't seen this so knock on wood.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Conformal rocks, especially their ECO capability ... amazing. In a past
life Synopsys swore up and down that their readers for DC and Formality
were different. Turns out at the time they were the same and Synopsys
lied to us. As a result we ended up with a bad chip.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality worked out OK and actually found stuff.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We got Conformal "cheap" as part of the Cadence deal, Formality would
cost money.
I still believe it's a serious problem that it's effectively impossible
to use Formality to check CDNS RTL Compiler's output and equally
impossible to use Conformal LEC to check DC Ultra's output. Nowadays
you have to use the same vendor for synthesis and formal equivalency
checking.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
In 2005, Conformal won the shootout. The cost to change is too high.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
I haven't tried Formality. We have an in-house LEC tool we use which is
much more powerful then Verplex, but also a lot more complicated.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Been using Formality for years and it still is a major pain to get it
working sometimes. Pretty good for checking manual netlist patches.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Partially we are still using a former inhouse tool
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
I don't think that this is a matter of trusting one vendor's tools over
another; we use Conformal because that's what we use.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality supports UPF, Conformal does not, so we currently don't have
much of a choice here.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality is easy to use, but interactions between FM/DC (read: SVF)
occur commonly and are a pain to debug.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
SNPS needs to fully debug Formality's interface to make it easier
to find and fix mismatches.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We trust Conformal LESS than Formality. Conformal is a RPIA. And
you can't be sure it catches all errors. But we will be forced to
use Conformal. Conformal-ECO is the WORST.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
Formality can't verify our designs.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We did not get too many bugs, but the tool's default behavior cannot be
trusted. Formality needs to set way too many variables to do something
useful. The default behavior will give false positives, which is a very
dangerous thing.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We used Mentor Formalpro before, but it couldn't cope with our code.
So we had to use Formality instead.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We use FormalPro from Mentor and sometimes Verplex (too pricey).
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We have a long tradition in using OneSpin and are pretty happy with it.
- [ An Anon EDA User ]
---- ---- ---- ---- ---- ---- ----
We have been using OneSpin (formerly CVE, Siemens development) before.
They gave up the EC business (but still doing property checking) so we
needed an alternative. We have been testing both Formality & Conformal
and had the impression that Conformal can do a better job in spite of
Formality being able to use SVF (can we trust that?). An everlasting
problem for all third party EC, however, is with DesignWare.
- [ An Anon EDA User ]
Sign up for ESNUGs! Fun!
Index
Next->Item
|
|
