( DAC'18 Item 7 ) ------------------------------------------------- [02/14/19]
Subject: CDNS JasperGold dominates over SNPS VC Formal as #7 "Best of 2018"
JASPER STILL KICKS ASS: Two years ago back in 2016, I had two spies report
very different histograms for 2016 Formal ABV market.
One 2016 spy said the $84M 2016 ABV market broke out to:
Cadence Jasper : :############################# $58M (69%)
OneSpin : :###### $12M (14%)
Mentor Questa FV : :## $4M (5%)
Synopsys VC Formal : :# $2M (3%)
While the other spy in 2016 said the $84 2016 ABV market broke out to:
Cadence Jasper : :######################### $50M (60%)
Mentor Questa FV : :########## $17M (20%)
OneSpin : :##### $11M (13%)
Synopsys VC Formal : :### $6M (7%)
But now two years later in 2018, using these ABV user comments as a proxy
for market dollars, the 2018 ~$100M histogram now ballpark breaks out to:
Cadence Jasper : :################################## $67M (67%)
Synopsys VC Formal : :######## $17M (17%)
OneSpin : :###### $10M (10%)
Mentor Questa FV : :## $4M (4%)
Mind you this is my best guess estimate with lots of voodoo involved. It
can be argued many ways on how the exact details are wrong -- but what this
data (after all the yelling is done) overall roughly says is:
0. From 2016 to 2018, the entire Formal market grew from $84M
to ~$100M, which is a 19% growth over 2 year.
1. Cadence Jasper is still kicking ass as the overall leader in ABV.
2. Synopsys VC Formal has moved from a distant #4 in 2016, to now
in 2018 being the #2 in ABV.
3. OneSpin and Questa FV are in the much weaker #3 and #4 slots.
AART'S (FORMAL) OFFENSIVE: So how did SNPS VC Formal go from ~5% marketshare
in 2016, to two years later getting ~17% in 2018 for ABV?!! A 3X jump!
First off, Aart did ballsy no-punches-pulled head-on marketing against
JasperGold by name!
And after that (from what I've heard) Aart's Salesdroids gave deep discounts
to customers switching away from JasperGold -- thus making his VC Formal a
very sexy option as long as it did 70% of what JasperGold does. This gave
the ABV customers the choice of:
CDNS JasperGold SNPS VC Formal
(Excellent plus Pricey?) - or - (Good Enough plus Cheap?)
Not bad for a SNPS ABV R&D team that's outnumbered 3 to 1 by CDNS ABV R&D.
---- ---- ---- ---- ---- ---- ----
TECH DIFFERENCE: This year the Herr Docktor Formal experts joined the survey
results for the first time in numbers -- compared to the more common Designer
Who Uses Formal Apps guys. The "experts" are ~30% of the formal base, while
the Apps runners are ~70%. How to ID an "expert" is they talk about "proof
engines"; something the Apps runners very rarely do.
THE FUTURE IS APPS: The other "win" that you'll see for Jasper is the users
are talking a lot about Jasper Apps in the comments. In contrast, not
one user spoke about VC Formal, OneSpin, nor Questa VF apps in the survey.
This is a "win" for Jasper because it's in Apps -- which an average designer
can use -- is where 80% of the future growth for *all* Formal will be.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen this year? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
CADENCE JASPERGOLD
For best of 2018, I'm recommending two Jasper Apps.
a. Jasper FPV App
Cadence's JasperGold FPV app has become our go-to app for formal
verification of several of our designs. Its improvements have
been impressive.
1. Proof Orchestration and powerful engines
Techniques like orchestration that allow a new user (who may
not be familiar with Jasper's engines) to take advantage
of the best engines. Engines like L allow us to go deep in
the design looking for bugs. And B-swarm, proof-grid, etc.
are allowing us to explore more of the design space and
observe the progress of engines. Some of the advanced engine
options (like engine B optimizations and abstraction engines)
have helped manage the complexity of our proofs.
2. "check_assumptions"
There are techniques that help us sanitize our test-bench
constraints, check if they are consistent, or if they are
leading to dead-end states.
3. "get_needed_assumptions"
With a complex testbench and several formal verification
engineers working a project, it's important to extract that
*one* set of assumptions that leads to some failing property
or unreachable cover. What used to be a manual binary search
among the set of assumptions is now, with this command, a
very effective technique to get the minimal set of conflicting
assumptions.
We also have a "save/restore database" for proof runs now, so we can
save off the proof results in a database and restore them when needed,
and then continue from the saved state -- instead of rerunning the
proofs again. This saves us a lot of time and licenses.
The Visualize that we use with FPV is also impressive because it allows
us to trace a failure to its root cause; while keeping track of the
signal values (through "why") in the source browser. Visualize has
become our de facto tool to understand the design by writing simple
cover targets and observing the cover trace. Features like Quiet
trace and wave-edit mode has made working with traces much simpler.
b. JasperGold Sequential Equivalence Checking App
After working with Jasper tools for almost 6 years, we've seen the
JasperGold SEC app grow from a cut-point script to a scalable, automated
tool. The automated generation of helper assertions and double-sided
cut-points have made the tool almost push-button.
I'd definitely recommend the JasperGold FPV and SEC apps.
---- ---- ---- ---- ---- ---- ----
We're long time Jasper users. Over the years we're seeing a move
from less simulation to more formal.
- Some verification tasks are difficult to handle with simulation
only -- or they are always partial with simulation -- whereas
they can be trivial with formal.
- So we now regularly brainstorm about these difficult bits -- and
more and more often decide to go on with a formal-only validation
of some features.
- JasperGold's progress in their proof engines often let us get
exhaustive proofs on these problem cases, so our confidence in
not needing to run any simulation is high.
Jasper is also high on usability. We see more and more designers being
able to "drive" the tool by themselves through the Apps. Even so, to
ensure our formal testbenches and setup are bullet proof, we prefer
to have them supervised by our formal experts.
Capacity always a concern for formal verification. Jasper's been
increasing that every year.
Cadence's newly integrated flows are efficient and have allowed us to
drop our custom flows -- especially for bug hunting. Their support is
good, and they've taken our improvement requests seriously.
We are now curious to see what Cadence R&D will do to add machine
learning into Jasper itself plus its Formal Apps.
---- ---- ---- ---- ---- ---- ----
I have been using Jasper Formal for quite some time now. From the
beginning, I was struck by its ease of use.
We frequently use the FPV, SEC, and Connectivity Apps.
1. JasperGold SEC App
I had an ideal opportunity to apply the Jasper SEC app on a
recent atypical project, where our existing design IP was
being radiation hardened.
I used SEC extensively on about 80+ modules, and was able to
either a) find issues due to due to radiation hardening
changes and/or addition of new logic and/or b) prove there
were no issues.
At a very high level, the SEC App was low effort & high value;
pretty much push button.
2. JasperGold FPV App
I also applied Jasper FPV app on the same project, using
get_fanin and get_fanout to verify a design change (in
addition to formal proofs). It came in very handy.
The first thing I use with FPV is Visualize/design
exploration. It lets me play around and get familiar with
the design, and then get a pulse check/heartbeat of the design.
It's very useful to both design and DV engineers.
FPV's feature enhancements -- or more precisely automation,
because we used to do these manually -- for reset and counter
abstraction look promising. Plus, the formal coverage helps
me grade my formal effort.
3. JasperGold Connectivity App
We use forward connectivity because we solve connectivity
plus functional verification. In this context, reverse
connectivity has not worked for us, but that is something
I would like to explore to eliminate the need to create
a .csv file.
Any discussion of Jasper formal would be incomplete without mentioning
Cadence's AE support for Jasper. When the acquisition happened, we
fear its support would go in the toilet, a commong cost cutting move
that happens after being acquired. Instead, Cadence beefed up Jasper
support and has kept it very high since.
I learned early on from Jasper and later Cadence AEs that in addition
to the tool itself, formal verification is all about how to approach
a problem in formal and how to apply it.
---- ---- ---- ---- ---- ---- ----
I used Cadence's Jasper connectivity app - along with the reverse
connectivity feature on a project.
We focused the tool on two areas for our mixed-signal SoC project.
1. The first was to ensure end-to-end connectivity of a few
dozen SoC IO signals under various control signal and state
conditions.
2. The second was to perform an exhaustive proof of a 23 input to
one output OR circuit - where the circuit had been implemented
as a multi-level cascade of NAND, NOR, and inverter gates using
the Virtuoso schematic design tool.
Jasper Apps performed wonderfully. Plus, I found Cadence to be very
helpful to get me past all the hurdles in adopting the Jasper app for
that mixed-signal project. (I'm not a formal expert by any measure.)
---- ---- ---- ---- ---- ---- ----
I've been using JasperGold tools for the last 6 years and have
definitely seen performance improvements -- mostly driven by newer,
better engines, orchestration techniques, etc. It's let us be more
productive in verifying our designs of ever-increasing complexity.
Jasper's Visualize (and its associated features) is powerful for both
debugging counterexample waves and for understanding the design itself.
Typically, you can:
- Write a set of cover properties on interesting output signals
in the design
- Observe the traces in Visualize and use "why" to understand
the flow of logic from inputs to the outputs.
Visualize's best features are:
1. Wave-edit mode. Wave-edit mode allows us to do further
experimentation on the fly. We can set the signal and bus
values of interest and explore where it takes the design
state to.
2. Free, extend, and replot. A feature that we constantly use
to freeze the trace and extend it with constraints. It lets
us explore some interesting scenarios that we might
otherwise overlook.
It gives an intuitive way of figuring out if one bad scenario
(as evidenced by a counterexample trace) can lead to another
bad scenario (allowed by trace extension).
3. Quiet trace. Quiet trace allows us to simplify the trace to
be manageable in most cases -- even for traces showing
occurrence of several events.
4. Signal annotation. The integration of the source browser with
signal value annotations while working our way through the
trace is a very intuitive way to understand the logic.
Bug hunting has become our go-to technique as we look for the last bug
before we freeze our code. Given today's design complexity, arriving at
full proofs for many of the interesting properties always remains a
pain, despite tool improvements.
WARNING: We need to still analyze the micro-architecture to establish
if proof bounds are sufficient. And in many cases, when we are at the
borderline depth, we want to make sure we are not letting things fall
through the cracks.
We typically choose the set of properties which we would like to target
for deep corner-case bugs and run hunt with different configurations.
---- ---- ---- ---- ---- ---- ----
So far today from our experience, Cadence JasperGold has outperformed
both OneSpin and VC Formal. We use Jasper for both small and large
blocks -- it handled both well.
- The Visualize debugger is good. You can basically ask it why
something happened, and it traces it for you. That's pretty
useful.
- Bug hunting. Cadence has an "engine L" that you can use to do
searches to reach deeper point in the design. Usually what I
do is good enough, so I don't need the deeper exploration.
At our company, our designers use JasperGold. Many companies don't
invest the time for the designers to use it, but we did. (Designers
must be trained in its basics. It's not a click and forget tool.)
It works best when the designer take a first shot at catching errors
before turning over to the verification team.
Jasper Coverage App works well for what our designers want.
My own general use of formal vs. simulation for verification hasn't
changed much, as I've used formal for verification since I started --
because I don't need to write testbenches. I do write assertions, but
I don't have to do so. I haven't needed to use Cadence support much.
---- ---- ---- ---- ---- ---- ----
This was my experience a few years ago, comparing JasperGold with other
formal tools:
- We had pretty typical situation: according to an FPGA
simulation one of our design blocks had a bug, which,
according to our designer, was "not possible at all" !?
- We had to prove/disprove this designer's statement.
- The formal "goal" for proof was pretty easy, but some vendor
formal tools (who I won't name) provided unrealistic results.
- So, we were going to stop the effort, but then somebody
suggested we evaluate Jasper.
- After ~ 1 hour of preparing the design for Jasper, the results
were just great. JasperGold showed clearly that our designer
was wrong, and he had to debug the situation in his design.
It was so impressive! Since then, I've respected both JasperGold and
its creators.
Also, since then, I've worked with other formal tools (again, who I
won't name) and have a pretty mixed impression of them.
---- ---- ---- ---- ---- ---- ----
Cadence JasperGold FPV
JasperGold Formal Property Verification's strength is that it can
automatically and exhaustively explore all states that are within a
given radius of a target starting state.
For some designs/properties this achievable radius is sufficient for
reaching all states of the design, hence yielding a full proof.
However, for most realistic, non-trivial cases (particularly with
scoreboard-based/end-to-end checks) the achievable radius only yields
a bounded proof.
In this case, engineering analysis is required to ascertain:
a) whether the bound-achieved-by-the-proof-engine is sufficient
for this design and property, and
b) whether additional proof starting points are needed.
If the bound-achieved-by-the-proof-engine is deemed insufficient, then
a combination of techniques can be applied to solve this problem by:
- Design reduction
- Stimulus Divide & Conquer -- by piece-wise over-constraining of
the input scenarios
- Assume-Guarantee Divide & Conquer --by partitioning the design
and building compositional proofs from there)
If you need additional proof starting points, you instruct Jasper FPV
to reach the desired coverage point by state-space search -- and then
start your next new proof from that new state-space point.
The sweet spot for JasperGold FPV is designer-level RTL blocks with:
- moderate sequential depth (50 clocks or less)
- lots of complexity
- myriads of interleaving orders of critical events that can
cause deadlock, or other failures if mishandled by the design.
JasperGold FPV's ability to find the shortest path to a bug means that
failure waveforms are shallow, simple and directly to the point (i.e.
to the bug). Debugging with FPV is much simpler than with simulation.
Formal property verification requires methodology and planning in the
same way that constrained-random RTL simulation-based functional
verification does. They're just different in the details. Cadence's
AE team is strong, and they are always able to help explain these
differences.
---- ---- ---- ---- ---- ---- ----
Jasper plus our in-house connectivity platform
We've been using Cadence JasperGold extensively for around 6 years.
It's the best tool available in the market for formal verification.
In our business unit, we primarily use it for chip-level connectivity
verification. We rarely use Cadence's connectivity app, but JasperGold
is the main workhorse behind our in-house connectivity platform. There
have been occasional bugs, but the excellent support provided by Cadence
have fixed them in a timely manner.
While a typical in-house tool run can use 100s of JasperGold licenses
and servers in a medium complexity chip, we are happy that we have
finally automated the top level manual review of the chip, reducing our
effort almost by 80%.
---- ---- ---- ---- ---- ---- ----
We initially used the Jasper SEC only for clock-gating verification.
We now use it much more widely. When we start a new project with a mix
of new and reused modules, we have many new uses for SEC.
It's surprisingly easy to get full proofs with SEC, even on large
modules, thanks to the built-in proof features such as automatic
cut-points and dedicated engines.
---- ---- ---- ---- ---- ---- ----
I've used Cadence JasperGold for over a year to perform unit level
formal verification on next generation CPU designs.
WHAT WORKS REALLY WELL:
JasperGold is both easy to learn and easy to use. Coupled with some
basic training in formal principles, any verification engineer should
be able to add formal to his or her verification toolbox.
Starting from an empty screen in Jasper can seem daunting. Loading a
testbench usually necessitates a common setup script; however, once the
design is loaded, analyzed, and elaborated, everything is right where
you need it.
As with other tools and languages, you only need to know about 20% of
the features in order to do 80% of your work.
You can easily access common workflow items such as adding properties,
running proofs, and debugging counterexamples. Anything deeper than
that usually requires the command line, which can be a hassle without
prior experience. (Especially without tab completion!)
The Jasper waveform debugger, Visualize, is one of the best debuggers
I have used. It's why-analysis and in-place wave editing are powerful
and allow for efficient root cause analysis without having to waste
time searching for relevant signals.
The why-analysis lets me step through a large codebase while focusing
only on the signals I need. Performing the analysis at different cycles
in the wave provides even more design insight. The signals are color
coded by type (net, flop, latch, input,) which makes it easier to
determine where the issues might be. (Without Visualize, Jasper
wouldn't be nearly as capable or approachable to a new user.)
WHAT NEEDS IMPROVEMENT:
JasperGold could improve its over-constraint detection, reporting, and
handling. In large designs, it is inevitable that some signal will be
over-constrained or incorrectly constrained, which leads to undetermined
or unreachable covers and incorrect proof results.
Currently, the best way of determining which assumptions contribute to
an over-constraint is with the get_needed_assumptions command. However,
this command is slow and only produces a large list of assumptions to
investigate.
With a large design that has many assumptions, this process has rarely
been efficient for fixing over-constraints. Knowing the relevant
constraints for each property, and additional info about constraints,
such as potential redundancy, would be helpful.
The check_assumptions command, while a good starting point, does not
provide enough information about how to resolve potential conflicts or
dead ends in a design's constraints.
On a side note, Jasper's new proof caching, should greatly speed up
the formal workflow, but I haven't used it myself yet.
---- ---- ---- ---- ---- ---- ----
JasperGold's high capacity.
I've run JasperGold with blocks with 1000 flops and gotten convergence.
I've always impressed with Quiet Trace, (which cuts down signal
activity) although I wish it was faster when dealing with large
designs. Good response time when exploring the design.
---- ---- ---- ---- ---- ---- ----
Cadence JasperGold
We've found many complex bugs during early RTL development on several
blocks for a complex SOC.
For one block, using its static formal verification found bugs that
resulted in one of our designers needing to make architectural changes.
---- ---- ---- ---- ---- ---- ----
Jasper is one of them for this year. We just bought it.
---- ---- ---- ---- ---- ---- ----
Jasper & Palladium.
---- ---- ---- ---- ---- ---- ----
We use some of the Jasper Apps to good effect.
---- ---- ---- ---- ---- ---- ----
Kathryn sold us Jasper. Still works well despite being acquired.
---- ---- ---- ---- ---- ---- ----
Jasper
---- ---- ---- ---- ---- ---- ----
We looked at Jasper and VC Formal. Choose Jasper.
---- ---- ---- ---- ---- ---- ----
My Cadence FAE says Jasper is selling like hotcakes.
---- ---- ---- ---- ---- ---- ----
We're very happy that Jasper didn't die under the Cadence buyout.
---- ---- ---- ---- ---- ---- ----
We use Jasper
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
SYNOPSYS VC FORMAL
We got VC Formal in a bundle. It works.
---- ---- ---- ---- ---- ---- ----
I think we're now a Synopsys VC Formal house for verification.
I'll ask and get back to you.
---- ---- ---- ---- ---- ---- ----
SNPS has been pretty aggressive about displacing Jasper seats with
their own VC Formal. The nice thing is they'll sell for cheaper.
---- ---- ---- ---- ---- ---- ----
Just bought VC Formal. Goes well with Verdi/VCS
---- ---- ---- ---- ---- ---- ----
VCS, Zebu, VC Formal
---- ---- ---- ---- ---- ---- ----
Synopsys is offering deep discounts on VC Formal. Mgmt wants us
to give it a serious look.
---- ---- ---- ---- ---- ---- ----
We like the price competition SNPS is giving against Jasper.
---- ---- ---- ---- ---- ---- ----
SNUG seriously pushed VC Formal. We're looking at it now.
---- ---- ---- ---- ---- ---- ----
My company did an extensive eval comparing formal + simulators.
Both Candence and Synopsys have excellent full bundles that
were roughly equal. VCS better than Incisive, Jasper better
than VC Formal. We didn't feel comparing Zebu vs. Palladium
made sense because they're so very different. What caused us
to pick Synopsys was because our designers and verif. guys
both loved the Veridi environment than what Cadence offered.
---- ---- ---- ---- ---- ---- ----
We're interally torn between Jasper and VC Formal right now.
---- ---- ---- ---- ---- ---- ----
Verdi, VCS, VC Formal in a 3 year bundle.
---- ---- ---- ---- ---- ---- ----
We got VC Formal at a better price than Jasper.
---- ---- ---- ---- ---- ---- ----
Verdi + VC Formal. Hooks to VCS nicely.
---- ---- ---- ---- ---- ---- ----
Testing Jasper vs. VC Formal. Leaning to SNPS because of a cheaper
overall bundle price when adjacent verf tools thrown in.
---- ---- ---- ---- ---- ---- ----
Our guys luv Verdi. We're considering VC Formal.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
ONESPIN
John Rochfort recently pitched us on OneSpin. Looks good.
---- ---- ---- ---- ---- ---- ----
OneSpin 360 DV something maybe? I can't remember which.
---- ---- ---- ---- ---- ---- ----
Since we're a German company, it's natural we're OneSpin.
---- ---- ---- ---- ---- ---- ----
We bought an early version of OneSpin from Raik. I'm fairly
certain we're still using it. Updated version, of course.
---- ---- ---- ---- ---- ---- ----
OneSpin
It does much of what Jasper does for far cheaper. Better suited
for automotive.
---- ---- ---- ---- ---- ---- ----
OneSpin (for FPGA)
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
MENTOR QUESTA FV
My FPGA verification guys are happy with Mentor Questa FV.
---- ---- ---- ---- ---- ---- ----
Veloce, Questa FV
---- ---- ---- ---- ---- ---- ----
Questa Formal gets honorable mention.
---- ---- ---- ---- ---- ---- ----
Related Articles
JasperGold and OneSpin both get #11 in 2017 for "Best of" EDA tools
Jasper's #1 in #1 "Best of 2016", through killer capacity & debug
OneSpin's #2 in #1 "Best of 2016", the "we try harder" company
And how JasperGold compares to OneSpin in the Formal Apps biz
Join
Index
Next->Item
|
|
