( ESNUG 394 Item 7 ) --------------------------------------------- [05/29/02]
Subject: ( SNUG 02 #10 ) Three EDA Users Review Mentor's FormalPro EC Tool
> Gee whiz, I didn't even realize that Mentor *had* an equivalence checker,
> despite the fact that we have other Mentor products in-house. They're
> definitely behind on mindshare, then. :-)
>
> - Natalie Overstreet Ramsey
> Vitesse Semiconductor
From: Rob Christy <rob.christy@jennic.com>
Hi John,
We've been using Mentors' FormalPro product for around a year now. It was
the first formal verification product that we had used in Jennic, although
we had previous experience of Formality and Chrysalis from previous lives.
Based on what we knew 12-15 months ago about the formal verification space,
we evaluated Verplex Tuxedo LEC and FormalPro as we wanted a next generation
product for some of the big SOCs that we had planned. I should say we knew
that FormalPro was still being heavily developed on and was probably at an
advanced beta release at that time. We have a fairly healthy relationship
with Mentor anyway as we use their test tools and they promised us factory
level support if we ran into difficulties.
Our evaluation of Verplex LEC vs FormalPro was run on a number of testcases
(mostly contrived), eg. 64-bit mutiplication, and at the time our only real
design was a 500K 0.18um TSMC device. I should say that both tools
completed all our testcases with relative ease and with similar runtimes
(initially Mentor had an issue with the 64-bit multiplication example, but
this was fixed within 1-2days). We considered RTL vs RTL, RTL vs Gate and
Gate to Gate, with RTL in both VHDL and Verilog.
We opted for FormalPro at the time because it had a significantly smaller
memory footprint, and a claim from Mentor which we have now verified to be
true that it could handle multi-million gate designs flat with RTL vs Gate
(we were skeptical at first)... Plus we knew we could have some input on
how we would like the tool to be improved.
A summary of our results is shown below (score of 1-5, 5 being the highest,
but not necessarily meaning its perfect, but based on previous experiences
of what we wanted or expected for a tool of this nature):
Ease of Use: Verplex LEC 5 FormalPro 5
RTL/RTL (compare): Verplex LEC 5 FormalPro 5
RTL/RTL (debug): Verplex LEC 5 FormalPro 4
RTL/Gate (compare): Verplex LEC 5 FormalPro 5
RTL/Gate (debug): Verplex LEC 4 FormalPro 5
Gate/Gate (compare): Verplex LEC 5 FormalPro 5
Gate/Gate (debug): Verplex LEC 3 FormalPro 5
We thought LEC's debugging was slightly easier for RTL vs Gate, just
because of better cross probing capability, and FormalPro was better at
Gate vs Gate debug. I guess because of the ATPG pattern technology it
has under the hood, it could more quickly identify the real candidate.
From a comparison point of view both tools were fine and there was little
in it. We also had one little plus with mentor in that you could use
Verilog, Synopsys lib and Mentors ATPG library formats as input, which
allowed us to compare these libraries against each other. We had a recent
case when the vendor Verilog supplied library had an an error - we
identified and fixed this very quickly.
Since then Mentor's general debugging/reporting has improved (some at our
request). However now we have run an additional 2 large designs through
the tool to review real capacity.
Design A - 3.2 Mgates 0.18um, Verilog, (macros: rams and ms blocks)
Design B - 2.2 Mgates 0.13um, VHDL, (macros: rams, arm cores, ms blocks)
Both designs can be run completely flat at RTL vs. Gate. I personally
have run through Design A on a Sun Blade (750Mhz, 8GB phys mem, 24GB swap)
in around 2 hours. In fact its memory footprint was only 700MB (so
comfortably within a 32bit OS which is good as we are migrating to a more
Linux related environment and FormalPro runs on this OS).
For us the fact that FormalPro can handle the design flat as opposed to
Verplex LEC which does a hierarchical type comparison, meant that we did
not have as much tool setup to perform for when the physical tools had
manipulated pins through clock tree (insertion and re-insertion), smashed
blocks together, or had other renaming problems. Synopsys DC change_names
and Mentor's default regexp for names rules have worked in all of our
design cases). You can still do a hierachical bottom up style if you like
by black boxing or similar (but for us there seems little point as runtimes
are acceptable).
So what problems did we have, apart from the 64-bit multiplier issue we
saw 12 months ago? We have had only one real error to do with ifdefs in
an always statement in Verilog:
always @(u_status or u_config or u_porten or isb_ad `ifdef UDP_SUPPORT
or udp_config `endif)
This caused the tool to fail with the Verilog reader, and was fixed within
a 1 week time frame. Before the fix we just recoded the failing blocks;
not that our RTL guys were too pleased. The rest of the issues fall into
just gathering experience of the tool ie. knowing which report files mean
anything when debugging and initial setup etc.
We had another instance (not really an error) when the graph matching
within FormalPro was making wrong comparison points - which was touch to
find from a debugging point of view. However turning it off fixed the
problem, but the real root of the issue was some redundant logic and/or
unreachable code had not been discovered with our linting and code
purification environment. Mentor fixed (within the next release) the
debugging of this type of problem, and of course we reviewed our other tools
as to why this was not picked up earlier.
Most of our wishlist for improvements with FormalPro were to do with the
reporting of text to be reduced and spat into side files (which was done),
and to add GUI capable operations (rather than just side files) for
constraining of pins etc. (just so occassional users could benefit, the
power users still wanted the side files). From the Verplex LEC side we
would have preferred reports to be generated in a predefined default
area, plus improve the gate level debugging (we ran one test case where
we inverted the scan mode signal deliberately and LEC identified every flop
in the design as a potential fail plus the inverter - FormalPro gives you
the inverter straight away). We thought this was a resonable test as there
are always a few gate level hacks performed in the final stages for a lot
of the chips we've worked on, and manual mistakes happen). We also wanted
LEC to improve its what-if capabilities eg. for gate swapping and re-running
the comparison.
We are currently using FormalPro version 3.1_4.3 and are waiting for version
4.x of the tool as there are many more improvements. My view is that
FormalPro is now perfectly competitive to any of the other offerings. When
we made our initial purchase there was perhaps some doubt that the tool
could deliver, but felt that the risk was worth it with the first release we
saw. It's been steadily improved since then.
- Rob Christy
Jennic Ltd. Sheffield, England
---- ---- ---- ---- ---- ---- ----
From: Raju Patel <RPatel@ciena.com>
Hi John,
We evaluated Verplex and FormalPro one-year back. For Chrysalis, we told
Avanti our design size and they did not response to us. FormalPro was the
only tool able to handle our 8 million Gate ASIC. When we evaluated
FormalPro it was able to handle only gate-to-gate formal verification. We
are getting good runtimes -- 6 million gate designs finished in about 2.5
hours on a Sun 700 Mhz machine.
In the early use there were several bugs in FormalPro that would not allow
it to do RTL-to-gate formal verification: parameter passing in RTL,
complementary matching problem on flip-flops with only XQ output, handing
Synopsys DesignWare resource comments, floating net handling etc... In
addition to these, there were problems with few switches which were not
working properly.
Mentor has fixed the majority of these in v3-4_0-5 and the only issue not
fixed (complimentary matching) has a workaround script that Mentor gave us
for modifying library cells which have XQ as a output. We are now running
RTL-to-gate formal verification on our latest design to verify that netlist
after ECO's is equivalent to modified RTL. The runtime for this is very
good -- about 3.5 hours for our 6 million gate design.
FormalPro's areas for improvement are:
- no incremental compile capability to further reduce runtime.
- In case of an error in RTL to gate translation, FormalPro reports
error in their internal database directory. It should report in
user log file.
- The complementary matching is not fixed in latest release and
still needs a workaround.
Overall we are happy with the FormalPro results and will continue using it
as a part of our ASIC Design flow.
- Raju Patel
Ciena Corporation Fremont, CA
---- ---- ---- ---- ---- ---- ----
From: Pierre Ragon <pragon@lucent.com>
Hi John,
We have been using FormalPro for almost 2 years to check designs that have a
complexity of up to 2 Mgates and 125,000 flip-flops. I haven't used
Chrysalis/Verplex/Formality. We used Vformal in the past. Then after
Vformal was taken over by Avanti, we stopped using it mainly because we
had no ASIC project at that time. We started cold with FormalPro and did
not evaluate competition. FormalPro works RTL-to-RTL, RTL-to-gates and
gates-to-gates.
We used the RTL-to-gates to verify that Design Compiler has not altered our
design functionality. Interestingly enough the problems that we caught were
not synthesis problems.
One was related with an array that was indexed in such way that the index
overflowed the array range by one:
my_array(idx + 1)
with idx varying within the array bound. FormalPro and DC had a different
interpretation of what the implementation should be when the index
overflowed. This issue had not been detected by the RTL simulations and
could have been missed because it was a very comples corner case.
The other one was related to a synthesis script error. A module was
instantiated several times in our design with some occurences of fixed
inputs. The module was synthesized once with the constant inputs propagated
and then the result of the synthesis was reused for other instances with a
different configuration. This would cause erroneous simulation at gate
level. But it would be difficult to find the cause because it originated in
deeply embedded modules. And it would have taken a lot more time to run the
gate level simulations to pinpoint the error than analyzing equivalency
check results.
Finally we use the gates-to-gates to verify the post-layout netlist with the
pre-layout netlist.
My experience so far is that FormalPro is easy to use (less than a day to
get started), fast (35 minutes to compare two 2-Mgates netlists) and does
not need a lot of memory (less than 512 Meg).
When a difference is found, FormalPro immediately reports both the registers
that do not contribute to both targets and the registers that must be set to
specific values to propagate the difference. That already helps a lot in
many cases to find what is happening. Besides that, schematics of the logic
clouds which features the difference and whatif analysis mode gives some
more help for the more complex cases.
Several FormalPro bugs were found and solved quite quickly thanks to the
support provided by Mentor graphics. Some bug examples:
- The most difficult bug they had to fix had to do with a constant in
VHDL code that was not propagated well by FormalPro synthesis engine.
- Another bug was that synthesis_on/off were not supported correctly.
- The absolute value operator was incorrectly supported: FormalPro removed
the case for the most negative integer in the 2's complement range.
- Using numeric_std library, I found a problem w/ the multiplication
operator used with an integer argument and a signed argument.
These have all been fixed by FormalPro v4-1_0-7.
The main improvment that I would like to see in FormalPro is for its
multiplier verification in RTL-to-gates. There are still cases where it
needs to blackbox the multipliers to complete the verification.
We usually remove the operator heirarchy during one optimization step and it
seems to make it more difficult for FormalPro to verify a multiplier that
has been optimized together with the surrounding logic.
Overall Mentor's synthesis technology is a bit less mature than Design
Compiler. But FormalPro is still very useful and the fact is that DC
results need to be compared to something that has been synthesised with a
different engine (at least for the RTL-to-gates comparison.)
We find FormalPro to be a valuable addition to our design flow and are very
satisfied with the results on the whole.
- Pierre Ragon
Lucent Le Plessis Robinson, France
|
|
