( DAC'19 Item 5b ) ------------------------------------------------ [02/28/20]
Subject: Cadence JasperGold still formal ABV favorite is Best of 2019 #5b
JASPER STILL GOT GAME: Since 2012, Jasper has continued to earn user kudos
as the formal verification favorite every year.
http://www.deepchip.com/items/dac12-05.html
http://www.deepchip.com/items/dac13-02.html
http://www.deepchip.com/items/dac14-07.html
Except in 2015 where there's suddenly *no* JasperGold DAC'15 "Best of"!
http://www.deepchip.com/items/dac16-01b.html
http://www.deepchip.com/items/dac17-11.html
http://www.deepchip.com/items/dac18-07.html
http://www.deepchip.com/items/dac19-05b.html
Because users (naturally) had concerns on how a Cadence-Jasper acquisition
would work. Sometimes acquisitions are good. Sometimes they're disasters.
In this case, it went amazingly well. And Jasper even got #1 "Best of"
in 2016!
---- ---- ---- ---- ---- ---- ----
AART JUMPS IN: Sensing an opening in 2015, Aart has his SNPS R&D launch
his VC Formal in 2016 to get 5% initial marketshare -- and after 2 years of
very ballsy agressive direct marketing against JasperGold by name plus some
heavy discounting -- by 2018 Aart got ~17% of the ABV marketshare.
BUT NOT ON PAR: What that in turn meant is that by 2019, some JasperGold
users were able to give direct comparisons.
"JasperGold is clearly hands down better than VC Formal. JasperGold
has better proof engines, better user control over what the tool
does and 1 - 1.5X better performance."
"Comparing Cadence JasperGold with Synopsys VC Formal, JasperGold
is easy to setup. From my experience, I also prefer JasperGold
because it has better support and a larger user community."
And the 2019 users also commented on what they liked about JasperGold now:
Visualize debugger
|
Jasper support
|
"As my first step in doing formal, I always run the Visualize
debugger. Visualize helps get me more insight into my design;
and I invariably find the 1st bug using it."
"After 10 years of use, I'd recommend JasperGold for functional
formal verification. Cadence's support sets it apart. And when
I say support, I don't mean tool support. What I mean is the
Jasper AE support is to help solve a formal problem."
Making Aart's VC Formal attack on Jasper was an overall "meh" right now.
Some users will take VC Formal as something thrown in with a package deal;
but if it comes down to an ABV benchmark, right now, JasperGold wins it.
---- ---- ---- ---- ---- ---- ----
BUG HUNTING GOES DEEPER: JasperGold FPV is a bounded model-checker, so
proving all assertions only proves the absence of bugs to that bound,
e.g. the first 20 cycles. In contrast, this new JasperGold Hunt option
does swarming strategies to get to deeper depths of 100's of cycles.
"JasperGold "Hunt" -- it runs the JasperGold engine L to go
deeper, so we can get more confidence on our bounded proofs.
We've used Hunt to go 200-300 cycles deep and have found failures."
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
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
It's the best formal ABV tool around today; and one of few tools
that still shows considerable improvement post-acquisition year
after year and version after version.
I primarily use its formal property verification (FPV) for block level
verification, and its sequential equivalence checking (SEC) for power
optimization and clock gating verification.
I use the tool throughout our entire design process -- from early RTL
development all the way through to final netlist. (I'm a formal
verification specialist.)
Our process
1. We set up JasperGold. To do this, we just need to know our RTL
and the JasperGold commands -- or use Cadence's setup examples
that ship with the tool.
This takes two days.
2. Since most of the regular designs we work with are large, we
usually shrink our design so that JasperGold can consume the RTL
and converge, in order for us to get sufficient proof of absence
of bugs.
For example, if our FIFO is 64 entries deep, we check to see if
we can make it only 8 deep (write in/read out).
To do this, we talk to the designers about the primary
functionality, and then try to weed out the parts of the logic
that are not core to the primary functionality. This enables
us to:
- Focus on verifying the primary and most relevant design
functionality, and
- Abstract away the irrelevant parts to make the setup
simpler and thereby better for the proof engines.
Most of the first steps of doing this involve shrinking some of
the structures to a size amenable to formal verification (for
e.g., FIFOs, counters, etc.)
Using this process, we've been able to reduce a design of a
substantial size (e.g. 100,000's of flops) down to something
that can be handled relatively well (about 10,000's of flops).
This takes us about one month.
3. We write the properties to capture the functionality that we want
to verify; which itself is arrived at after several discussions
with the architects and designers. Our properties contain:
- Assumptions. Some failures can occur simply because some
input combinations may not be legal. So, we make sure we
resolve these false failures by adding assumptions to the
input signals such that they allow all the legal behaviors
of the inputs.
- Assertions. We write assertions on the outputs to make sure
they are correct. In a sense, assertions are the
expressions that relate the output behavior to the inputs.
- Coverage. Make sure interesting points in design are
reachable.
4. We begin our formal testing.
Our iterations will initially uncover lots of failures primarily
due to the input not having a legal behavior. So, most of our
initial time is modeling the inputs to be legal and not
over-constrained. An example of over-constraining would be
saying that an input is always zero, which would mean that we are
verifying the design only for the scenarios where this particular
input is zero.
After writing the assertions, the more interesting and crucial
work starts - i.e. we start finding real counter-examples. We
bring up these waveforms and discuss them with the designer to
analyze the failure and the designer will go ahead and fix them.
We then iteratively run the assertions until they no longer fail.
Typically, for our designs we run the proofs for around 8-12
hours (i.e. not everything gets proven in 8 hours, but we see if
any bugs turn up by then.)
5. We also run random simulations to make sure our assumptions on
the inputs are reasonable and that we are not over-constraining
the behavior.
Going back to the previous example, if we had over-constrained
(assumed) an input signal to be zero, this would fail in
simulation (as one of the random simulation tests would inject a
one value to the signal) and would indicate that we need to fix
our assumption. We also review our assumptions with the
designers.
JasperGold Hunt for deep bug hunting
Proving all the assertions to a specific bound does not prove the
absence of bugs (beyond that bound) because JasperGold FPV is
primarily a bounded model-checker (i.e. for bug-hunting, rather
than an exhaustive proof tool). i.e., if an assertion is bounded
proven until 25 cycles, we can only be sure that there cannot be
a bug in the first 25 cycles and cannot be sure about the 26th cycle.
This is where we can use JasperGold "Hunt" -- it runs the
JasperGold engine L to go deeper, so we can get more confidence
on our bounded proofs. As it consumes lot of licenses, it can
take us about 30 days to run them on the most crucial properties
and to find and fix a corner case bugs.
The "hunt" command now has a relatively new "-auto" switch. It
runs state swarm and cycle swarm strategies alternately and
automatically, and a novice user no longer has to specify the
strategies and can leave it to the tool to figure it out.
We've used Hunt to go 200-300 cycles deep and have found failures.
CADENCE JASPERGOLD VS. SYNOPSYS VC FORMAL
1. For Formal Property Verification, JasperGold is clearly hands
down better than VC Formal.
JasperGold has:
- Better proof engines
- Better user control over what the tool does.
- 1 to 1.5X better speed/performance.
2. For sequential equivalence checking and clock gating verification
(power optimization), both tools were comparable.
3. Debug
- JasperGold has the best formal verification debug in
industry, due to its "Visualize" waveform viewer and various
features, such as:
Wave edit mode -- Once you have a failure waveform, you can
use the GUI to edit the values of the waveform signals,
toggle the signals you want, and replot.
Quiet trace -- If you have lots of toggles in your waveform,
you can minimize the number of toggles on a signal and still
give the same scenario, to make it easier to debug.
Add constraint & replot -- You can add constraints to
waveform on the fly to see if it can still produce the same
waveform.
- VC Formal - I do not believe Verdi has wave edit features.
Other points on JasperGold
- Learning Curve
The basic learning curve is fast; it only takes 2-3 weeks.
However, the learning curve is steep for the more advanced
features, such as finding corner case bugs to stress the tool
and choosing the right engines.
- JG-COV coverage analysis
Once you've written 100 assertions and you're not sure if they
are enough or if they are all on one part of the logic,
the Coverage app will tell you how much of the logic your
assertions cover and where you may want to write more.
The Coverage app is useful as it points out which parts of
logic are not exercised at all. For example, a designer
may write an If-Then statement where the "Else" is never
exercised.
Cadence's support has been awesome for years now.
I recommend it.
---- ---- ---- ---- ---- ---- ----
Cadence JasperGold
We begin using it on our designs as soon as our RTL is ready and stable.
Here's where we find running formal is superior to doing RTL simulation:
- X-propagation checking
- Sequential equivalency checking, where we must verify two
designs with different cycle delays
- Connectivity
- Corner cases that take a long time to simulate
Overall, we have used it for:
- Block-level verification (such as end-to-end checking,
x-propagation, coverage)
- Integration verification (connectivity)
- Equivalence checking in clock gate insertion or re-pipelining
for timing
- FSM liveness and deadlock checking
- Bug hunting to find hard to hit corner cases
JasperGold has a feature that allows convergence of multiple properties
in parallel. For the last few, which take the longest time to converge,
I've found it is usually more efficient to run them one-by-one.
Comparing Cadence JasperGold with Synopsys VC Formal, JasperGold is
easy to setup. From my experience, I also prefer JasperGold because it
has better support and a larger user community.
For block level and for SoC applications, JasperGold's larger capacity
and faster convergence are very important for me. The largest block
we've run it on had around 10,000 flops.
JasperGold's debugger has improved a lot, and I do not have any specific
issues with it. There is always more room to continue improve it.
Cadence claims it can hunt down bugs that are 100's or 1,000's of cycles
deep. I believe that would be super useful for complex design such as
CPU/GPU/NPU. However, I have not tried it.
We've used the following JasperGold formal apps
- JasperGold's Formal Property Verification app (FPV) is the
foundation of the rest. It proves any properties that are
either user-defined or auto-generated by other apps. Useful
anytime.
- The Sequential Equivalence Checking app proves two designs are
functionally equivalent, regardless of cycle throughputs.
Useful in ECO phase.
- Connectivity app - good for integration and block connections
checking.
- Cadence X-propagation app used to check the x state in a design to
prevent uncertainty. Running JasperGold's X-propagation checking
on the 10,000-flop design took us about 48 hours.
- Coverage Unreachability app used for coverage closure and for
checking the quality of your verification.
I would recommend JasperGold any time. It's apps are useful, including
it saving time to close coverage by finding unreachable code quickly.
I'd also say that JasperGold is tops ease-of-use. Plus, Cadence's
Jasper support is very good.
---- ---- ---- ---- ---- ---- ----
I've used Cadence JasperGold for 10+ years now. I use it for:
- Block level verification (end-to-end)
- Connectivity at integration level
- Automatic Formal or SuperLint for FSMs
- Sequential equivalence checking (SEC), where applicable
I run JasperGold during all my verification stages including late stage
and post silicon.
As my first step in doing formal verification for any design, I always
run the JasperGold Visualize debugger -- i.e. *before* I switch over to
formal property verification (FPV). Visualize helps get me more insight
into my design -- and I invariably find the 1st bug using it.
I use the JasperGold Coverage app for all my FPV efforts to help grade
my FPV and fill coverage holes. It gives me further insights into my
design, plus I use the information to help with waivers in the
simulation UCDB (universal coverage database) during coverage closure.
After 10 years of use, I'd recommend JasperGold for functional formal
verification. Cadence's support sets it apart. And when I say support,
I don't mean tool support.
What I mean is the Jasper AE support is to help solve a formal problem.
---- ---- ---- ---- ---- ---- ----
Cadence JasperGold
It has a nice GUI, lots of "apps", good performance, and excellent
support by Cadence. We use it for:
- Block verification; integration verification; equivalence
checking; security verification; sanity checks (e.g.
X-propagation), coverage closure; and deadlock verification.
- Some of these aspects are simply not doable with simulation.
For example, clock-gating, security, X-propagation and
deadlock.
- We use JasperGold for verification from the start to the end of
our project. We even use it to debug post-silicon bugs.
IT CAN BE SLOW: We've run JasperGold on full CPUs. It can converge
multiple properties in parallel. This was great, however, our design
sizes have grown faster than the tool's capabilities, so the results
are no longer as strong. Even so, we expect big Jasper improvements
here, perhaps using machine learning.
Some of JasperGold's strengths:
- An intuitive UI allowing beginners to quickly drive the tool.
The embedded expert system can help, too.
- Good bug hunting depth. It is possible for us to catch
bugs at 100's cycles on small designs, and at 10's cycles
in on medium/large ones.
- The GUI for Visualize and debugging are great.
We use these JasperGold formal apps.
1. Sequential Equivalence Checking app
We use this to compare two designs even if they have sequential
differences. It's extremely useful for different applications:
- Clock-gating verification
- Minor RTL changes to full rewrites that supposedly do not
change the functionality
- Advanced verification to check that some micro-arch level
events are not visible at the architectural level (e.g.
security)
- Design for verification checks: we add hidden features in
the design to help verification. We use SEC to ensure
these have no functional impact.
2. Coverage app
Good but not precise enough, because JasperGold's ProofCore
coverage approach is much too approximate/optimistic.
COI and stimuli coverage also good to find where the big holes
are, and where the over-constraints are. But we could not
target 100% coverage -- only look at the evolution and the big
holes. Cadence needs to do more work here.
3. X-propagation app
This app is useful because simulation is not able to catch X-prop
issues. However, in general, formal has poor performances here.
There are very few proofs,& no deep bounds for inconclusives.
4. Security app
This app has high potential but is currently difficult to master
and has poor performances. Cadence needs to do more work here.
JasperGold seems to now have serious competitors in OneSpin and
Synopsys VC Formal. They now have similar debug features and
sometimes even better performance.
But JasperGold still leads overall in terms of GUI and number of
features/controllability.
In the end, I recommend using JasperGold. And Cadence support
is very good, especially when we have direct contacts with the
expert AEs and/or R&D.
---- ---- ---- ---- ---- ---- ----
We're looking at Synopsys VC Formal right now.
---- ---- ---- ---- ---- ---- ----
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
|
|
