( ESNUG 434 Item 6 ) -------------------------------------------- [11/18/04]
From: [ The Man In The Iron Mask ]
Subject: We Use Real Intent, Then Magellan, Then JasperGold As Our Flow
Hi, John,
I saw in your DAC Trip Report survey that you're asking users to compare
Real Intent vs. Magellan vs. JasperGold. I think you're seeing this
wrongly.
First some context. We have evaluated these tools for more than a year
and/or own most of the formal verification (FV) tools on the market.
All our in-house evaluators have a research background in formal methods.
We long ago made a commitment to formal because we build some of the most
complex chips in the world, and simulation is just not sufficient.
Formal functional verification tools divide into 3 major categories:
- Automatically-Extracted Checks (AEC) like Real Intent, which we
own.
- Bug-Hunters of user defined properties. We considered Magellan,
0-In, Averent, RuleBase, BlackTie and Real Intent. We chose
Magellan in this category for its better overall performance.
- Exhaustive Formal. We use Jasper and Magellan.
With the AEC tools, you can find a class of functional bugs that are
easy to fix, with little effort in the form of dead code, stuck-at
flops etc. We use Real Intent's Implied Intent for that purpose and
numerous early design bugs were found in the previous projects which
accelerated overall verification time specially when our simulation
wasnt yet ready or matured. This tool usage is in the process of
getting mandated in our designer's code.
With Bug-Hunters like Magellan, you can find complicated user-defined
black box as well as white box property bugs with minimal effort. A
significant number of them were found across various projects. It also
can prove properties, although limited in capacity due to it being
completely automatic. We use Magellan as our default formal verif tool
for user defined properties (best for bug hunting until now). We have
empirical evidence of its semi-formal engine finding hard to find bugs
which random simulation or pure formal engines failed to see. Most
importantly, Magellan's semi-formal engine found black box property
bugs at the unit level which were missed by simulation (>100k flop
design, 2 designers code) which pure formal tools will never scale.
Exhaustive Formal is what we use to prove the correctness of properties
at sub-unit level (1 designer's code). This is the best measure of
the "are we done yet?" question. After some successes in bug-hunting
using formal, our management has made a fundamental shift in attitude
about formal: from "go find bugs" to "prove the blocks are clean".
Jasper is currently the only tool that can have us acheive this goal.
(We had a sub-unit where all the other tools missed a deep bug and
Jasper's manual proof technique helped us find it. Note that Magellan
with its semi-formal method can even find simulation missed bugs at
big unit levels which no formal tool can find but can it can miss bugs
in the sub-unit level that requires Jasper's manual approach. On the
other hand Jasper won't scale for big unit levels, as the manual effort
would be impractically huge.)
When we first used Jasper, the use model was essentially manual. So we
used Magellan on the properties that it could handle to prove, and then
switched to Jasper to navigate to full proofs and found few more bugs
in the process.
Recently, we have a beta version of JasperGold 3.0. The user interface
is more natural, in comparison to its predecessor. It navigates the
user (in our case, NOT the original designer) through the proof process
and the design. It gives next-step guidance at various stages in the
proof process and finally reaches proof or a falsification missed by
simulation as well as fully automated formal or semi-formal techniques.
JasperGold 3.0 also has a new fully automated mode that seems very
promising in performance, and will allow us to run the tool in multiple
modes.
Bottom line, Implied Intent helps us find early functional bugs even
before simulation is ready or not yet mature at sub-unit level. Then
Magellan helps us find many more complex bugs during or post simulation
at both the unit & sub-unit level. Jasper completes the verification
by reaching proofs on the most important properties at sub-unit level.
- [ The Man In The Iron Mask ]
|
|
