( ESNUG 389 Item 8 ) --------------------------------------------- [03/06/02]
Subject: ( ESNUG 388 #5 ) Another Customer Likes Formality 2002.03 (Beta)
> We then quickly implemented & verified the fix by running another complete
> RTL-to-Synthesized-Netlist check. I strongly recommend using Beta
> Formality 2002.03, if you can get it from Synopsys. At one point, we
> were afraid we would have to re-synthesize this entire (very complex)
> design. That would have taken 2 days when you consider that you'd have
> to restitch the scan chain back into the new netlist plus redoing all the
> backend stuff. Instead, our problem was completely resolved in a matter
> of hours.
>
> - [ The French Olympic Skating Judge ]
From: Pontus Pleven <pontus.pleven@ebt.ericsson.se>
Hi, John,
I had the opportunity to evaluate Formality 2002.03 (Beta), too. Overall
we were fairly pleased with Formality's improvements.
We've used other LEC solutions (FormalPro, Chrysalis) but they were not to
our complete satisfaction. These LEC tools plus previous versions of
Formality had problems verifying our designs. Either they were difficult
to setup and use or they had long or inconclusive verifications. We've
found that these improper tool setups usually leads to false verification
failures that take forever to debug.
Our 300K gate scalable Bluetooth Core IP is in both VHDL and Verilog as two
tracks. (We have to serve both Verilog and VHDL customers equally.) But
these different languages, we don't want to double the time we spend on
simulations and verification. It's same functionality. So we save a lot of
time by using a LEC tool at this phase.
Our LEC situation was so bad for one chip we had to deliver verification
results based on different LEC tools! Our RTL-RTL LEC was verified with
Mentor FormalPro but not with Formality. The RTL-Gatelevel LEC did not work
with FormalPro so we used an old version of Formality instead. On top of
this, Chrysalis was the sign-off tool. We were forced to deliver Chrysalis
LEC with exceptions and unverified points.
The VHDL and Verilog readers behave differently on certain code structures
and Design Compiler has yet another view. No wonder the tools will get
problems. Intensive simulations on both Verilog & VHDL and FPGA testing
told us we had a correct flow. We weren't happy with this messy LEC flow.
All this changed with beta Formality 2002.03. We used it both for RTL-RTL
and RTL-Gatelevel LEC with great success. It was hard to believe.
Chrysalis still gives us unverified key points on the same design.
Formality 2002.03 beta's new interface was extremely easy to get into, and
the new debugging capabilities have been a big help. I especially liked
the source browsing.
During our beta period, we managed to spot some redundant logic, which
we removed from our design. A process which completed within a few
hours of work. Perhaps we made no big savings of logic but for sure it
saved us a lot of time by quickly pinpointing the issue.
Another thing we liked was easily setting constraints directly in its GUI.
Compare point matching are a major pain for LEC tools. Ideally, you want
the tool to do all the matching automatically. I still haven't seen a tool
that can automatically match all points all the time. But Formality 2002.03
got pretty close. And with the new intercative matching capabilities, we
were able to quickly verify that our constraints worked before running a
complete run. Writing batch scripts was as easy as running the GUI.
Another major problem using LEC tools is understanding why and where it
fails. Formality 2002.03 beta gave us some pretty good hints where by
listing error candidates while showing logic cones graphically.
Overall we are very happy with the new Formality 2002.03 since it's easy to
use, fast, and gives us no problems within our flow. Simple as that.
- Pontus Pleven
Ericsson Technology Licensing AB Lund, Sweden
|
|
