( ESNUG 412 Item 4 ) -------------------------------------------- [05/22/03]
Subject: ( SNUG 03 #14 ) Three Mentor FormalPro Users Defending FormalPro
> FormalPro was not able to complete this stage with every flop defined.
> One problem was that some self-fed spare flops in the design were
> discarded somewhere between the reading of the design and matching. A
> second problem was that some of the unmapped points could not be found in
> any report. Specifically, benign points were reported in the log, but not
> found in a report. Another problem was that it was hard to find a report
> that correlated to all of the categories in the log file, the Target
> Display in the GUI was really the only way to understand what happened to
> every compare point. I also needed to declare some state machines as
> 1-hot. I did not put much credibility into the results of FormalPro since
> I could not account for every flop.
>
> - Joe Hasting
> Agere Systems
From: Russ Petersen <russp=engineer domain=subasic.sciatl knot qualm>
John,
I have to react to some of the comments in the SNUG trip report about
FormalPro. I have no doubt that there are issues with Formalpro because in
fact we see them daily. However, Mentor is aggressively working to fix them
and in any case they involve complex solve problems that any tool really
doing a compare would likely have (ie: unsolved, etc...)
We did a direct compare of the 3 tools last year and found that Formality,
true to its standard, bombed out with a very, very inexecusable bug on the
reading of the library cells. It was a parsing 101 error that should have
been found in the first 5 minutes of testing. Further Formality failed to
complete even simple compares. Given that we had a copy of Formality in
house that we had been using for about 2 years at that point (or should I
say tried to use off an on with very little success) we booted it to the AC
and said basically, "Hey, if you can make it work on this design then we
will look at it, otherwise we don't want it any more." That was the end of
our Formality trial.
Verplex. It ran OK and seemed to be comparing all right but when we really
digged into things it had about 1/3 the compare points that Formality and
FormalPro came up with. I asked but never got very satisfactory answers to
this (possibly due to my own ignorance in this area) but we felt that
Verplex does a lot of hand-waving/assumptions in their compares which scared
the heck out of us.
Formalpro. What can I say? It works great, the support is there, it has
saved us from ugly disaster several times on the latest chips. It still
needs improvement in solving complex stuff but which tool doesn't? We were
also very happy with the quality of the individuals answering our questions.
We ended up speaking with PHDs who really knew formal verification and could
explain how and why their tool did something a particular way. I really
felt that they, most of all, knew what they were doing and cared about doing
a good job.
My challenge to those looking at the 3 tools. Really push each vendor to
engage you with their best people and see what kind of answers you get. I'm
guessing you will find Mentor to be the most knowledgeable in this area.
- Russ Petersen
Scientific Atlanta, Inc. Lawrenceville, GA
---- ---- ---- ---- ---- ---- ----
From: Jorgen Lundgren <jorgen.lundgren=person company=emw.ericsson.se>
Hi John,
We started to evaluate tools for equivalence checking in early 1998 but when
the tool we did choose (Check-Off from Abstract Hardware) disappeared from
the market, we did the evaluation all over again late 1998.
That was when we came across FormalPro from Mentor. Unfortunately FormalPro
did not support VHDL at this time, which caused us to disqualify it for this
evaluation. We kept in touch with Mentor and when we could not verify our
netlists in summer 1999, we decided to try FormalPro again. The problem for
our other equivalence checker (DesignVerifyer from Chrysalis) was that extra
hierarchy had been included in the netlists, but this was not a problem for
FormalPro since it always flatten everything.
It took some time longer before we accepted FormalPro for RTL-(VHDL)-to-gate
verification and this was mainly caused by poor matching and compilation and
other things that forced us to do changes directly in our revision handled
code. All these issues are fixed now. Compilation has been the main
struggle during the years for all formal verification tools we have seen
We've been using Formality from Synopsys, Heck from Cadence, DesignVerifyer
from Chrysalis, FormalPro from Mentor, Averant, Verifier from SafeLogic and
Verysys. Today I can say that FormalPro is the only tool that we have been
using that can handle the way we design. There are usually no problems as
soon as the compilation has succeeded. When we started to use equivalence
checkers we did use three (Formality, DesignVerifyer and FormalPro) in
parallel for a while because we just did not trust the technique at first.
We found more bugs in the tools than in our design. But today equivalence
checking is mature enough to stand on its own.
We have been using FormalPro to verify 20 ASIC's ranging from 300k gate to
8M gate, using technologies from six different ASIC vendors. All of the
chips used FormalPro for gate-to-gate comparison (Verilog) and at least 10
of them have been verified (RTL-gate) with help of FormalPro.
The best success story from us must be that we were able to verify a
chip RTL-VHDL-to-gate-Verilog (year 2001) in the size of 1.5M gates in
one go using FormalPro version 3-4_0-4 ! (Today we use FormalPro version
4-4_4-5.) This took us no more than 2 hours 30 min on a Sun Starfire with
the memory consumption less than 500 MB. With DesignVerifyer version
2001.3 we had to do 84 verifications to cover the design which took us
16 hours before we had completed the task, not to mention the time for
setting up the design. This showed us that FormalPro could handle pretty
large designs and also that it is fast. We also liked the reports it
generates together with cross probing. It has a good debugg environment
that does "what if" analysis that one can use to, for example, replace a
cell and see if this change did make the designs equivalent. This
feature has been especially good in comparing two netlists where one
contained a lot of ECO's. I do not know how this should have been verified
without this feature, not touching our code.
FormalPro is very easy to setup and get started with. We use it both in
GUI mode as well as in batch runs. The idea is that as soon as a Design
Compiler run is done, FormalPro will start and give us a result that tells
us if the synthesis was correct or not. We would like to find the problems
up front and not wait to find them. If we can catch synthesis or
verification related problems early we will save both time and money
Do we find bugs using equivalence checking? The answer is yes, we find
bugs coming from EDA tools, wrong versions that has been used for synthesis
(it should not happen but it does), we find problems during integration,
ECO's at gate and RTL level not having the same functionality, etc.
In the beginning I was using tools from Chrysalis, Mentor and Synopsys in
parallel because they were not mature enough. Today I use just FormalPro
and I have been doing so the last two years.
- Jorgen Lundgren
Ericsson AB Sweden
---- ---- ---- ---- ---- ---- ----
From: Maynard Hammond <captain=maynard.hammond ship=sciatl rot prom>
Hi, John,
I just wanted to let you know we are using FormalPro from Mentor. As all
EDA tools, it has its own limitations and bugs. However, we have received
excellent support. On our last chip which is about 12 million gates, we
have approximately 1500 unsolved end-points. They are still working with
us on these. I might also point out that the unsolved points come from
complex Module Compiler code that is building multiplier and multiplier-
accumulator circuits. If we black-box these circuits, we get 100%
verification. (In the past Formality was unable to solve these, too.)
FormalPro has allowed me to do RTL to gates or other RTL compares. I am
modifying our processor. To start off, I am re-writing all of the code.
I've been able to use FormalPro to verify that I have not introduced any
errors in the initial rewrite. It has verified 100% of what I've done.
This is an RTL to RTL comparison of very different code. We use a lot of
MCL. I've been able to use the .bvrl that comes out of Module Compiler
to do my RTL to RTL comparisons.
As I mentioned earlier, we have gotten extremely good support on this tool.
Mentor comes to our campus. They follow up on calls. Their AEs stop by
after the sale. They have sent us new solve orders to find more end-points.
I have been very happy with FormalPro and their support. I'm probably
biased, but I think they have the best solution.
- Maynard Hammond
Scientific-Atlanta, Inc. Lawrenceville, GA
|
|
