( ESNUG 501 Item 3 ) -------------------------------------------- [04/04/12]
Editor's Note: Since this was written before DVcon'12, I'd like to
ask the users and vendors to add any new data that's missing. - John
Subject: Conformal, 0-in, Jasper, RealIntent, OneSpin, NextOpt, Magellan
From: John Weiland
Hi, John,
Here's my report on Formal, Mixed Sim & Formal, and CDC tools.
Cadence's Conformal (the former Verplex tool) is probably the market leader
here. There is a new Conformal Low Power version that understands CPF and
check low power circuitry. Their full formal tool, Incisive Formal Verifier
(IFV) can automatically create and verify assertions (System Verilog, PSL
or OVA) without vectors. Cadence emphasizes this allows verification to
start before any testbenches are running. They also sell a Conformal ECO
(Engineering Change Order) Designer tool, which helps check minor logic
changes. I believe this tool is unique. The upgraded version also helps
pick which spare gates to use for metal-only logic changes.
Mentor's 0-In division sells full formal checkers. It can automatically
insert some basic checks and allows power users to do more sophisticated
checks. It includes monitors and assertions for standard interfaces and
blocks, like AMBA, PCI, USB and Ethernet.
Mentor also sells an equivalence checker called FormalPro that they say is
extremely fast. It has support for checking low power constructs and
support for FPGAs. Mentor Precision can move pipeline registers (retiming)
now and can now provide a "hints" file to FormalPro the way Synopsys DC does
to Formality (note that Cadence claims the "hints" file can sometimes cause
Formality to pass a bad design).
Synopsys sells Formality, an equivalence checker that understands UPF and
can check low power circuitry. Its one edge is that Design Compiler can
generate a file of hints when it goes messing about with pipeline registers
and the like, and only Formality can read those hints. (We've had designs
that Formality could check but Conformal couldn't because of this. The
local Cadence Conformal salesman claims that sometimes the hints are
incorrect and can mask errors; not sure how true that is.) As far as I know
Synopsys does not have any model checker or theorem prover type tools.
Synopsys also bought the transistor level symbolic simulator from Innologic.
This is really neat technology but is almost impossible to explain to anyone
because the concepts are so foreign. A version of the tool called ESP-CV is
packaged for checking memories which does not require the user to understand
much about the technology.
Calypto sells a sequential equivalence checker called SLEC. It can compare
two designs even with sequential changes (for example, a state machine in
one might use binary encoding while the equivalent machine in the other
might use one hot encoding). It obviously requires more computation than
ordinary combinational checking on a design.
Jasper sells JasperGold. The original product was guaranteed to find
a solution but to do that in a reasonable time required a user snip away
states he didn't care about, based on information the tool gave him about
counters, FIFOs, etc. Their tool can accept VCD to get to a useful initial
state, which is how it should probably be used. They said architects can
use it to prove things about protocols, and they provide proof kits for
AMBA and PCI Express.
The Jasper guys say RTL designers can use JasperGold to create/manipulate
waveforms and testbenches using scenarios created in their GUI via formal
engines. They say verification engineers can use it for "design tunneling"
to check things like "no packets will be dropped" that take lots of clocks
to verify. For post-silicon debug, they say they can help identify the
sources of problems. If you specify that the bug you are observing can
never occur, the Jasper tool will attempt to create a counter example where
it does occur.
New last year is a Jasper tool that takes RTL and questions input via a GUI
and produces SVA or PSL properties and waveforms. Apparently there is an
IP application on the horizon. They also sell a tool for planning the
verification process.
RealIntent had two formal tools, a "formal for dummies" tool called Ascent
and a "formal for gurus" tool called Conquest, both of which take assertions
in System Verilog (SVA) or OVL, but they now emphasize only Ascent. It
finds a fixed set of bugs like deadlock between state machines, etc., and
is rumored to be in the standard flow at Apple. It now includes linting
capability. In beta is the capability of tracking down X propagation.
Axiom (formerly @HDL) has an unusual "formal for history majors" tool that
automatically checked for things like FSM deadlock and code reachability
without having to learn any new languages.
OneSpin Solutions sells two formal tools. The first is a property checker,
which is unique because in addition to normal checks (both automatic checks
and ones defined by the user) they claim it checks whether the property
specifications completely describe the function of the block. If the
specifications are not complete the user can add more properties as directed
by the tool. Interestingly they do not look at the RTL at all to gauge
completeness, only the assertions and list of IP. They told me blocks need
to be under about 20K lines of RTL code, or under 10K flip-flops. They have
a structural assertion analyzer to help debug assertion failures, a temporal
fan-in analyzer, and annotation to RTL for debug.
The second OneSpin tool is an equivalence checker for ASICs and FPGAs that
they say is better than some competing tools because it is not tied to tools
used to create the design. Claim better X analysis and X verification.
NextOp Software sells a tool that takes RTL and a testbench and produces
assertions in SVA, PSL or Verilog. These can be thought of either as
assertions that additional testbenches should meet, or functional coverage
holes (interesting how that works); the user gets to pick which.
Hyper Analytix has a formal tool. It uses a GUI to correlate requirements
to assertions and does assertion based verification using coverage. I did
not get details.
Avery Design Systems sells a tool called Insight that takes a testbench with
assertions and uses symbolic simulation to try to come up with a set of
vectors that will trigger those assertions. It includes X verification, and
they say it finds reset and low power transition issues, and has formal
reachability analysis. New last year was DFT analysis for at-speed testing
done at RTL level. They compete against Atrenta and Real Intent here.
Mixed Formal/Simulation Tools:
Synopsys Magellan uses a mix of simulation and formal techniques (gets to
an interesting state via simulation and then explores the area with formal
engines), but unlike 0-In it generates the simulation vectors itself. I
don't know how popular it is but it's on the Synopsys web site.
One way of handling state space explosion in model checkers is to use
ordinary simulation to get to interesting states and then explore the state
space around that with a formal tool. Star Trek fans might think of it as
using warp drive to get to a star system and then impulse power to explore
it. This is what the original 0-In tool did (using the designer's testbench
as a starting point and exploring nearby states). I had a friend who
discovered a bug he would have never found otherwise using 0-in. I can't
even find this tool on the Mentor web site now but I'm told it is still
supported.
Cadence has a tool called Incisive Enterprise Verifier (IEV) which sounds
similar to the Magellan tool from Synopsys. It creates simulation vectors
itself based on assertions.
Clock Domain Crossing (CDC) Tools:
Mentor's 0-In division sells a clock domain crossing tool. They say it does
1. static CDC analysis
2. Protocol verification (can add assertions automatically if desired)
3. Reconvergence verification.
Axiom sells a clock domain crossing tool that does both static and functional
checks.
Atrenta sells Spyglass CDC for analyzing clock domain crossings. It sees
multi-flop cells, FIFOs, handshaking and reconvergent paths.
Cadence sells a clock domain crossing tool called Conformal CDC that they
say is very good are recognizing parts of the circuits.
RealIntent sells Meridian CDC. Claims it is the only tool where setup is
done with SDC constraints, so it is the fastest tool to get running. They
also claim to have beaten 0-In on a recent customer benchmark.
- John Weiland
Abraxas Corp. Columbia, MD
Join
Index
Next->Item
|
|
