( DAC'19 Item 5a ) ------------------------------------------------ [02/28/20]
Subject: OneSpin DV-Verify's surprise comeback in ABV is Best of 2019 #5a
ONESPIN'S SURPRISE COMEBACK: In the "Best of 2018", last year OneSpin was
amazingly weak. Users wrote 4,988 words about ABV tools in 2018; and only
a measily 59 words were about *anything* OneSpin. (Talk about weak! Ouch!)
But now, for "Best of 2019", OneSpin got ~3,000 users words on the OneSpin
vs. JasperGold wars covered here and in DAC'19 #5b -- plus ~1,400 more user
words OneSpin's other tools. (See DAC'19 5c.) Talk about a comeback!
---- ---- ---- ---- ---- ---- ----
WHERE ONESPIN WINS: The 3 areas where users gave OneSpin high marks were
assertion observation coverage, speed, and safety (fault injection).
1. Assertion Observation Coverage
"OneSpin's Quantify app uses the 'mutation' method. The mutation
method injects a forced logic state on each individual signal,
then evaluates if the assertion passes or fails. This gives you
100% coverage. ... JasperGold's Cone of Influence (COI) coverage
method is less comprehensive than mutation."
2. Speed
"OneSpin is better than JasperGold for complex properties. For
example, to prove a complex property on one design we verified,
OneSpin took 2 hours, JasperGold took 20 hours However, it
is difficult to generalize these results from a few designs."
3. Fault Injection
"With fault injection, to ensure your design won't let catastrophic
failures occur, Faults are deliberately injected. OneSpin has a
fault injection capability in their core tool. Cadence does not
include fault injection in their core tool -- it's an add-on."
---- ---- ---- ---- ---- ---- ----
WHERE JASPER WINS: From the user comments, JasperGold has this amazing debug
capabilty that's intuitive -- while OneSpin is seen as basic at best:
"OneSpin's user interface is a bit old-fashioned."
"It's debugging complex counter examples is painful within the GUI."
"OneSpin's debugger takes some getting used to."
"Their code debugging is "ugh"."
But beyond this GUI drawback, OneSpin has some killer capabilities.
---- ---- ---- ---- ---- ---- ----
AND WHERE COMPETITION IS GOOD: And another factor is OneSpin is cheaper to
buy than JasperGold is ... just read this first user comment below to
see what I mean.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen this year? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify Formal Verification
We recently decided to purchase OneSpin for our ABV, after evaluating
both OneSpin DV-Verify and Cadence JasperGold for ABV.
Our company needed a formal verification tool. We went to Cadence
first, since JasperGold is considered the market leader. However, we
choked on the price they quoted, and decided to evaluate an alternative.
After looking at some of the user write-ups in DeepChip, we decided to
also evaluate OneSpin.
FYI, Cadence actually lowered their price later to be competitive, but
by then we had decided that OneSpin had the best technology for our
specific needs.
Below is a summary of our eval.
All our designers do both the design and verification for their blocks.
They may write 12's to 100+ assertions in System Verilog, and then run
in 100K gate block or less through either formal tool.
Noise-level & Debug -
When you run your formal verification tool, if all your stimulus pass,
that means the RTL works for all your assertions. Alternatively, the
tool will show a failure, and the exact signals and sequences that
caused the failure.
However, like all static tools, including STA, formal verification has
noise, (i.e. not all of the message violations and warnings are actual
failures.)
- Noise level was about the same for JasperGold and OneSpin.
- Both OneSpin and Jasper also have wave displays, with
sufficient info to debug.
Assertion Observation Coverage -
The big question is, what did our assertions actually cover? The two
primary methods here are: 1) Mutation and 2) Cone of Influence.
OneSpin DV-Verify vs. Cadence JasperGold -
- OneSpin's Quantify app uses the "mutation" method. The
mutation method injects a forced logic fault state on each
individual signal, then evaluates if the assertion passes
or fails. This gives you 100% coverage.
Fault mutation is very compute intensive, so OneSpin has written
algorithms to collapse the design database to improve execution time.
- JasperGold uses a Cone of Influence (COI) coverage method.
COI looks at the logic cone going backwards from the assertion
to identify the RTL constructs that lead to the assertion's
operation. COI's coverage is less comprehensive than
mutation, but the coverage is sufficient for the vast majority
of the cases.
- Cadence understands that mutation method has higher coverage
and has recently said they are adding mutation. However,
OneSpin has an 8-year head start in deploying mutation, so
Cadence will likely have to go through the growing pains of
new software features. Additionally, it is unclear how much
Cadence will do to mitigate the compute intensive slowdown
for fault mutation coverage in their initial release(s).
Our company's present verification initiatives require a strict 100%
verification coverage, so OneSpin's Quantify app was our deciding
technical factor.
User Interface -
OneSpin's UI is very good. It shows all your code, then has colors for
each line of code coverage for its Quantify App.
- Green. The assertion covers it.
- Red. The assertion doesn't cover it, so you need to write
an assertion.
- Yellow. Partial coverage.
The JasperGold user interface is clear, useable and comprehensive. We
found no clear differentiation here from OneSpin regarding menus,
pulldowns, buttons and ease of use.
Fault Injection -
My company has an internal initiative to get higher reliability by way
of verification. One major goal we have is to check the safety
operation of our designs.
With fault injection, you ensure your design won't let catastrophic
failures occur:
- Faults are deliberately injected, i.e. you inject the
combination of inputs or modes that would cause the
catastrophic failure.
- You then observe the fault's impact -- the tool tells you if
the fault can get through and/or your design's response to it.
OneSpin DV-Verify vs. Cadence JasperGold -
- OneSpin -- has fault injection in their core tool
- Cadence -- does not have fault injection in the core
tool; it's an add-on
OneSpin also has a tool called DV-Inspect, which looks for code blocks
and unreachable code based on tool internal assertions. Although this
wasn't a determining technical factor for us, we plan to use it, so
it played into our cost/value assessment.
Our designers write their own assertions, so it's a good a starting
point for our new designers who don't yet have experience writing
comprehensive assertions.
Demo vs. Running a Real Design -
Most companies come out with a canned demo.
OneSpin came out and ran one of my actual block designs through their
DV-Verify. Since I knew the circuit, it helped me to better assess
their tool quality. The tool did identify a signal width issue that
later became a top-level simulation failure.
Support -
OneSpin has better support for second tier companies like ours. OneSpin
claims they want customers to help them enhance their tool and expand
capabilities; and their support shows it. We can call the applications
engineers directly by phone, rather than filling a ticket.
Bigger companies often have a CAD department with a formal tool expert
who can answer most questions. We don't have that, so the OneSpin
method and level of support is very significant to us.
Conclusion -
Cadence has some very good tools -- we use a lot of them. For formal
verification, OneSpin had a superior technology and support model for
our specific circumstances, better pricing/value, a more straightforward
sales process, and a support model implemented with person-to-person
contact.
OneSpin's entire focus is on formal tools and this enabled them to
better meet the specific circumstances for our company's needs.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify is a formal verification tool that we use to verify
many digital designs.
We primarily use it for property checking.
- When we have a new requirement, first, our design team does
unit testing using functional simulation, and then our
verification team runs DV-Verify.
- We write our assertions using OneSpin's proprietary ITL
language, along with SVA.
- ITL is a feature rich language; writing properties in ITL is
more intuitive than in SVA. It's a bit unfortunate that ITL
is not the standard property specification language.
I've used OneSpin for a few years now. I've also used JasperGold during
that time, so I can make a couple of comparisons.
Performance
Each formal tool has over 20 formal engines. When you check a property
for pass/fail, the tool picks the right engine -- some take longer to
run than others.
- OneSpin is better than JasperGold for complex properties. If
a property takes days to pass (property runtime), OneSpin does
better -- on some designs it can be 10x faster.
For example, to prove a complex property on one design we
verified:
- OneSpin took 2 hours
- JasperGold took 20 hours
However, it is difficult to generalize these results from a few designs.
In certain scenarios I have seen JasperGold performing better
than OneSpin. When there are large number of simple properties,
which need a proof runtime of one or two minutes, Jasper runs
faster.
For example, to prove a simple property:
- JasperGold might take 30 seconds
- OneSpin might take 2 minutes
Debug
- OneSpin has same debug features as JasperGold.
- JasperGold's debug is more intuitive and user friendly.
OneSpin DV-Inspect App
We also use OneSpin's DV-Inspect app as a sanity check on our RTL code
quality and to ensure semantic checks such as initialization, deadlock,
FSM checks, and register initialization checks.
Our design team uses Real Intent Ascent Lint for checking the RTL code
quality and they follow coding guidelines as well.
OneSpin support is excellent. We have great rapport and they are
responsive in accommodating our request.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify
We use DV-Verify with SVA to check our mixed VHDL/Verilog code. The
tool checks our RTL code 100% against our user-defined conditions
with constraints.
I've used DV-Verify both at my current company and my previous one.
We mostly use it for block verification and for general auto checks.
We also use it when we want to quickly get a 100% statement about a
specific behavior.
DV-Verify's biggest strengths are:
- No test bench needed
- Checks the conditions 100%
- Shows very fast first results (minutes)
- Can show system behaviors that the user didn't think of
OneSpin's debug window displays both the important and the related
signals. One major improvement that OneSpin made is that it is now
possible to view the debug window while other checks are running.
We also use OneSpin's DV-Inspect apps, mostly to check for dead code,
unused signals, open states, cycle count to change states, sensitivity
list, and initialization.
The largest blocks we used DV-Verify on were IPs with 250K gates
- The tool's performance is normally very fast. (minutes)
- We occasionally have performance problems, mostly if our code
is not clean. We must remove the RAM from the checks.
One big challenge is the use of multiple clocks in assertions. OneSpin
has performance problems with this (as does JasperGold and DV Formal),
and our verification engineer has headaches with the clock domain
descriptions -- but it works. In short, we need seperate specialized
CDC tools even when we use formal ASV tools.
Formal verification is in a different world from simulation. In
simulation, I define pattern sequences and then check the behavior of
the block against my expected results.
With formal, auto checks are the first step and are very simple. The
assertions checks are next. We start with simple functions tests and
then increase the complexity until we fully verify the block.
However, complex checks are not easy -- you need a lot of experience.
For example, there can often be a difference between what I thought I
had described and what I actually wrote in my properties.
Tip: Write properties to check both sides of a requested function:
1) the event is correctly reached under all conditions, and
2) that under all fail conditions, the event is not reached.
As for the noise level of the violation report, there is a learning
curve here with OneSpin. When we start, we get a lot of violations.
This improves as our verification engineers begin to understand the
design and the designer sees the results.
I would recommend that designers use OneSpin DV-Verify during the
design phase -- it is very helpful then. The designers know where
the design's critical points are and can use it to check for issues
against all conditions. The small blocks are very easy to check.
Tip: If runtime for a particular check is very long, check your
warnings first, as the problem is usually a combinational
loop.
From the verification engineering side, DV-Verify is also helpful to
get a full understanding about the functionality actually implemented
in the design e.g. if the specification is incorrect or incomplete.
Another good use case for the tool is to verify a specific system
behavior under all conditions.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify
It lets us automatically prove if a given set of properties -- such
as System Verilog assertions -- hold for a particular digital design
(RTL code). Although OneSpin supports multiple languages, we mostly
use SVA, and only seldomly use PSL.
OneSpin's formal tool checks whether the given assertions hold for all
execution of the design. This is in contrast with simulation, where
generally only some possible executions of the design are considered.
We use OneSpin for consistency checking (DV Inspect), block level
verification, and top-level connectivity checks.
- Our RTL designers use DV Inspect consistency checking, to
understand all the failing checks, to determine which ones
can be waived.
- Our verification engineers use DV-Verify property checking
to ensure functional correctness of the design.
DV-Verify's general performance is very good, it's 22 engines can
be tweaked to get the necessary proofs.
The largest design we've run recently on OneSpin DV-Verify was about
5,000 lines of code with over 100 I/Os and severe sequential depth.
The tool was able to completely formally verify the design.
Quantify Observation Coverage -
OneSpin has a feature called "Quantify Observation Coverage" that uses
a mutation algorithm.
The mutation algorithms not only ensure that there is a property aiming
at each signal in the RTL code, but also systematically manipulate the
RTL code (under the hood) to check if a change in the RTL would be
observed by at least one assertion failing.
This is one of our favorite OneSpin features, and it does not need any
further user input beyond your original assertions and your design.
UI and Debug -
OneSpin provides a simple user interface combined with helpful debugging
features and strong proving engines.
- The debugger is powerful -- we can interactively trace
from the signals of the failing assertion through our design
code to find the wrong assignment (bug) in the RTL.
- The RTL code annotation helps to keep an overview of current
values of the design at a certain point in time.
- Its waveform view supports understanding a counter example.
However, debugging complex counter examples is painful
within the GUI -- so currently, we mostly rely on external
tools to do that. OneSpin is actively discussing improvements
with us for this problem on a regular basis.
- OneSpin's user interface is a bit old-fashioned, but rather
simple to learn. All user interface actions can also be
accessed using console commands, which is great for scripting
purposes.
- Violated properties are highlighted in the user interface and
can also be reported in a textual form. You can adjust the
"verbosity" of your reports.
DV-Inspect Apps
We have used the DV-Inspect Structural Analysis app. It does a
syntactic and semantic analysis of source code. It's a pipe cleaner to
determine whether the delivered RTL code is free of basic flaws (stuck
signals, incomplete sensitivity lists, possible synthesis problems,
etc.).
We've also used the Activation Checks app, which ensures that specific
design functions can be executed and are not blocked by unreachability.
This is part of the consistency checking. It's easy to use and very
helpful to us before we start verification process.
Connectivity App
OneSpin's connectivity app allows us to read in an Excel (CSV) sheet
specifying 1) the connections between signals in the design, and 2) if
needed, the additional conditions under which certain signals are
connected. The assertions are automatically generated from the sheet,
no need for manually writing them.
We recommend OneSpin DV-Verify, and the DV-Inspect apps, and the
Connectivity app.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify
Does unbounded model checking, equivalence checking, and completeness
checking.
We have been using OneSpin for years. It has several differentiating
features for safety critical designs that we rely on. DV-Verify's
biggest strengths:
- 22 formal verification engines that can deal with complex
designs with high sequential depth
- Two unique methodologies for proving completeness of formal
verification. Useful for safety critical designs:
Quantify -- code-based completeness
GapFree -- functional completeness
- And a Debugger, which improves with every release
Quantify
We use OneSpin's Quantify whenever we must verify a block completely
with formal. Unlike the traditional code coverage of simulators,
Quantify provides *observation coverage*. A line of code is marked red
if it is possible to change it in such a way that no property finds the
problem -- and the change leads to a functional difference.
Quantify also marks the code fragments that are dead due to over-
constraining. It works very well for designs with several 1,000's of
lines of code and is great at uncovering functional coverage gaps.
DV-Verify Use Cases
DV-Verify is easy to use and works for the three languages we work with:
SVA, Verilog and VHDL. We use DV-Verify for the following:
1. Module verification against properties in SVA, including completeness
checks for safety-critical designs (mostly with Quantify, sometimes
with the GapFree methodology).
Some of our modules have included: microprocessors / DSPs with up to
25K lines of code; serial interface slaves (SPI, JTAG, I2C, LVDS...);
and complex FSMs and control logic.
2. Verification of bus infrastructure (arbiters, bridges, decoders) and
memory mapped registers, e.g. for APB, AHB, AXI4-lite, and
proprietary buses.
3. Verification of connectivity on top-level -- including analog
netlists.
4. Design "consistency checks" on module- and top-level. Examples are
dead code checks, signal stick checks, array bound checks, FSM
reachability checks, etc.
5. RTL vs. RTL equivalence checks (after design rework, bug fixing,
etc.)
6. Ad-hoc verification of properties that are critical or hard to
verify by Verilog/VHDL simulation.
DV-Verify's fit with our Methodology
We usually decide early whether we will verify a design block with
simulation or with formal. We do formal verification as soon as the
block-level spec and RTL implementation are ready.
Sometimes, we design our RTL with formal verification "in mind" to
improve verification performance and coverage.
We also sometimes go for formal verification if we find out that our
simulation coverage is insufficient, requires too much simulation time,
and/or needs additional attention due to safety concerns. In these
cases, we verify the relevant design parts using formal.
Additionally, our digital designers use DV-Verify for "consistency
checks" during module-level design (stick checks, dead code checks,
array bound violations, FSM reachability checks etc.).
Debugger
OneSpin's debugger takes some getting used to. It is not the best part
of the tool but with some practice you can be efficient with it.
Some debugging features are good -- especially the GapFree debugging
capabilities.
Others are "ugh": code debugging is "ugh"; the waveform viewer for
large counterexamples is slow; plus Quantify traces showing why a
certain piece of code is not fully covered needs work.
DV-Inspect Apps
DV-Inspect has a "linter feature" that we use to check for major
problems such as unintended latches; we use a commercial linting tool
(SpyGlass) for the rest. It also has "model building checks" that
check whether it is possible to violate array bounds, have multiple
drivers active on a single signal (X/Z checks), etc.; "stuck checks",
dead-code checks, and FSM reachability checks in DV-Verify.
Connectivity App
OneSpin's DV-Verify Connectivity App does both functional connectivity
checks ("a===b"; also, conditional) and structural connectivity checks
("netlist traversal" / "only" for wiring).
We have worked with it in the past and it did what it was supposed to
do. It can handle very large designs and does some under-the-hood
optimizations. However, we usually generate properties for connectivity
checks from our proprietary formats and verify them with DV-Verify
without using the Connectivity App.
---- ---- ---- ---- ---- ---- ----
I've known Raik since 2007. Of course we nominate OneSpin as best.
---- ---- ---- ---- ---- ---- ----
We're German. OneSpin is best.
---- ---- ---- ---- ---- ---- ----
OneSpin.
It matches Jasper but for a lot less $$$.
---- ---- ---- ---- ---- ---- ----
DV-Verify and DV-Inspect.
---- ---- ---- ---- ---- ---- ----
Related Articles
OneSpin DV-Verify's surprise comeback in ABV is Best of 2019 #5a
Cadence JasperGold still formal ABV favorite is Best of 2019 #5b
OneSpin in formal areas where Cadence is NOT is Best of 2019 #5c
Join
Index
Next->Item
|
|
