( ESNUG 461 Item 3 ) -------------------------------------------- [01/31/07]
Subject: ( ESNUG 458 #4 ) Anyone use Formality in a Cadence or Magma flow?
> Do any of your readers use Formality as an Equivalence Checking (EC) tool
> in their Cadence or Magma flow? In my experience, there's a tight
> coupling between Design Compiler (which creates "dwsvf" files) and
> Formality. These extra "dwsvf" files makes Formality's job a lot easier.
> Without the files Formality sweats. In our last project we had to give
> up on Formality in our Magma flow because the tool just couldn't verify.
>
> - Jay Pragasam
> PLX Technology Sunnyvale, CA
From: Vittorio Melini <vittorio.melini=user domain=xignal not balm>
Hi John,
I'm writing in response to Jay's questions on Formality. I have used both
Conformal and Formality. My company recently decided to purchase Formality
because of the reason Jay is unhappy. The Formality-DC flow is better
integrated than other flows. This makes it easier to use. With a Synopsys
flow, you get some of the setup straight out of DC, so it's not as hard to
setup as when you mix and match tools. This is a technical advantage, not
a deficiency.
Formality is still independent (the data is verified) and it can be used
with Cadence & Magma. You just lose the setup advantage when you're
not using it with DC.
- Vittorio Melini
Xignal Technologies AG Unterhaching, Germany
---- ---- ---- ---- ---- ---- ----
From: [ Papa Smurf ]
Hi John,
Please keep me anon.
I was formerly an AC with Synopsys, but have since moved on into a design
company. I can understand Jay's frustration with trying to get an
equivalence checking tool to work with highly-optimized designs. He's
correct, but I think he is missing an important point.
There are two long poles in the tent of equivalence checking:
1. The difficulty of verifying multipliers and some other datapath
functions (ERCs, parity, sometimes big adders, and combinations like
add-multiply) whose truth tables make it impossible to guarantee
that the verification can be done in the engineer's lifetime.
2. The difficulty of setting up a tool. EC is often run right before
tapeout, usually by a script inherited from central CAD or from the
last tapeout. EC is often viewed by management as more of a checkbox
item than a major task that gets time allocated in the design schedule.
See where this is heading? Nobody wants to debug EC. It has to just
work. Most design teams are horrified if they spend a week debugging
the EC runs just to find out that name changes are confusing the
mapping/matching step, or that a test mode needs to be disabled before
EC will pass, or that the run time could have been shortened by 90% by
setting up the tool in a certain way.
The first point, difficulty of verifying datapath functions, is something we
all have to work around, until there is some theoretical breakthrough in
computer science. Synthesis tools are making more and more sophisticated
optimizations, and the smarter they get, the harder the job will be for the
equivalence checker. It is not unusual to experiment with an EC run and
find that it is capable of solving 99%+ of the chip in under an hour, but
then the last couple of dozen compare points take overnight -- and even then
may not even complete with a conclusive yes/no answer. Invariably, that
proves to be the signature of a gnarly-to-verify function that's just
poisoning the pot for the whole rest of the EC run.
The "dwsvf" files Jay is referring to carry some kind of information about
the architectures that Design Compiler used to implement a few hard datapath
functions. Formality verifies that the architecture info is functionally
correct (it really does -- I've seen it reject dwsvf's), then uses it to
speed up the verification in those hard areas. Without this info, Formality
still tries to verify the logic, it just gets computationally harder. Which
is what Jay meant by "Formality sweats." Some EC tools are better on some
datapath functions than others, but any one of those tools will work better
with guidance than it is without.
This brings up the second "long pole in the tent": the difficulty of setting
up an EC verification. Synopsys has been using a guidance file crafted by
DC and read by Formality for several years now. This file is for mundane
functions like giving Formality the list of name-changes that DC made, or
recording flattenings and regroupings of the hierarchy that occurred during
synthesis. Using this kind of guidance does automate some of the setup that
would otherwise require an engineer doing debugging iterations. (Synopsys
likes to talk about this as a run-time improvement, which I think is missing
the point. My take is that if this kind of guidance can save some poor
engineer a week writing compare rules while his VP of Engineering breathes
down his neck asking why this EC thing is holding up the tapeout, nobody will
ever care if the tool's run time was an hour or overnight.) Ultimately, it
might even save the design team from having to abandon EC in order to tape
out on time, which it sounds like Jay's team did.
The concept that synthesis will write out some guidance for EC to read in is
not at all unique to Formality. Conformal does the same thing -- just check
the Synplicity manual! (Yes, Synplicity, as in FPGA synthesis.) As far as
I can see, the only real difference between the Formality guidance and the
Synplicity-to-Conformal guidance is that the Synplicity/Cadence guidance
file is not a standard. Synopsys finally published their file format as an
open standard (under the name "V-SDC") so that other vendors' tools can read
and write it as desired. When I was at Synopsys, I was told by customers
that there was also a Cadence RTL-Compiler-to-Conformal guidance file, but I
can't verify that. If that file exists, it's not a published standard either.
So in my view as a designer who has experienced a lot of pain from EC,
guidance is GOOD.
The question should not be "where can I find an EC tool that solves anything
I throw at it without any guidance." The better questions is: "When will
the EC vendors finish the job with the guidance?" When will they realize
that guidance should know where the scan_enable pin is and whether to tie it
high or low so I don't have to set it up by hand in the EC tool? When will
the EC vendors finally just record into the guidance file where all the RTL
was when the synthesis tool read it in, so I can use it again for EC and
don't have to go find it and worry about whether it's the same version?
(that can take HOURS!)
I think whichever vendor is the first to finally embrace guidance fully as
a good thing, and not be afraid of it, will be closest to giving me the
push-button EC tool my VP of Engineering seems to believe I already have.
- [ Papa Smurf ]
---- ---- ---- ---- ---- ---- ----
From: [ Count Chocula ]
Hi John,
Please keep me anonymous. My reply to the ESNUG 458 #4 questions.
> Q1. Is Formality an independent tool that can handle designs implemented
> using any flow?
Formality can be used with Magma or Cadence flows, I've done both in the
past. It's easier to use Formality with Design Compiler and SVF for designs
that are tougher to verify formally, such as those with a high degree of
arithmetic optimization, operator merging, etc. But, those designs will be
tough for any tool.
> Q2. Is Formality used because they get bundled with the Synopsys suite or
> does anyone find it technically more advanced than Verplex?
I consider both tools fairly even. I could use either and get the job done.
From a bundling point of view, I've seen this happen on both sides, but with
different angles. Formality is usually bundled with Design Compiler, while
RTL Compiler is usually bundled with Conformal. Synopsys doesn't discount
DC much, and Cadence doesn't discount Conformal much.
> Q3. Who has evaluated Magma Quartz Formal and how does it compare against
> Verplex/Formality?
I wouldn't bother with Magma Quartz Formal. I don't know of anyone who has
used or even tried this tool. In our last evaluation of EC Tools, we didn't
even consider it as an evaluation option.
We work with Magma Tools, including BlastFusion, BlastCreate, etc., so it's
not a slam against Magma.
For the past 10 years, I've personally used Formality or Conformal to verify
hundreds of blocks. I was a very early user of Chrysalis and Formality, as
well as Verplex Tuxedo. There was a lot of pain experienced during that
time, especially in the early days. The tools were primitive, and required
so much manual intervention to complete even a small complex block. I even
evaluated Mentor FormalPro several years ago, & came to the same conclusion
I'm coming to now. A multi-year lead is too much to overcome, especially
given the complexities of today's designs, design styles, libraries, etc.
I have many contacts in the industry, many of them who use Magma for their
backend implementation. And none of them have ever brought up QuartzFormal,
ever. I guess that was my bottom line answer to the gentlemen's question
"Who has evaluated QuartzFormal?" I haven't and most likely won't, and my
industry contacts haven't either.
I hope this helps.
- [ Count Chocula ]
Index
Next->Item
|
|
