( DAC'16 Item 1d ) ---------------------------------------------- [12/09/16]
Subject: And how JasperGold compares to OneSpin in the Formal Apps biz
JASPER KICKS ASS IN APPS: I gotta give credit to Kathryn Kranen when she
realized that her JasperGold tool was a nightmare for design engineers to
use -- so she copied RealIntent's "formal apps" concept way back in 2007.
And then she forcefully drove her AEs and R&D for multiple years to make
JasperGold apps actually work. (Keep in mind that she had a customer base
at the time who were used to being "Formal Wizards" whose work reputations
were built on their intimate knowledge of the secret incantations that makes
formal ABV work or not work. Creating apps was like saying: "Look! We're
creating SW so easy to use that it makes you an obsolete engineer!")
Formal apps took years to create and 1,000's of man-hours to shake out, but
she did it. And I have to tip my hat to Kathryn for pioneering this.
---- ---- ---- ---- ---- ---- ----
As I said earlier in this survey, this was a weird year. Once I realized
that Formal ABV and their apps were big this year, I made it a point to do
follow-up questions to the users on their specific formal app experience.
JASPER MIX-AND-MATCH: While at present Cadence JasperGold has 13 available
formal apps, the typical customer only uses 3 to 5 of them in his daily job;
with the exception of the Formal Property Verification (FPV) app which
everyone uses. Beyond that there's linting, X-propagation, unreachable
code, clock gating, sequential EC, reverse connectivity apps -- plus 7 more
flavors that I'm not listing here. There's even a datapath security app
that got a lot of DeepChip reader interest in 2013 in ESNUG 524 #3.
Your average Jasper customer is used to mixing-and-matching formal apps.
ONESPIN PACKAGE DEAL: On the other hand, when I asked the OneSpin users what
their favorite OneSpin apps were, they were perplexed at first. Because
Raik sells them in a everything-in-one-big-package deal, the DV-Verify users
tend to see them as knobs and switches inside DV-Verify. What's unique for
OneSpin is they have a Safety Fault app, a SystemC Algorithmic app, and an
odd type of Coverage app -- that JasperGold doesn't have.
ONE IS ALLOWED: Ironically, while you must own a JasperGold license to run
any Jasper formal app, OneSpin will sell you formal app that run standalone
*without* needing any additional DV-Verify licence. (That is, the company
known for *bundling* formal apps also specializes in single serving apps.)
PRICING: depending on who you ask and exactly what you're doing, there's
no always cheaper combo of Jasper + Apps vs. OneSpin + Big Package of Apps
pricing model. Both companies, and their users, say their way costs less.
P.S. For more, see Jim Hogan's Guide to 16 Types of Apps in ESNUG 558 #4.
"Knowing is not enough; we must apply.
Willing is not enough; we must do."
- Johann Wolfgang Goethe, German writer & philosopher (1749 - 1832)
QUESTION ASKED OF JASPER USERS:
Q: "What do you think about the JasperGold apps?
Which JasperGold apps does your project use?"
---- ---- ---- ---- ---- ---- ----
The 5 main JasperGold apps that we use:
FPV app - is Jasper's main formal function, and we use it for most of
our verification environments.
Sequential Equivalence Check app - we use this in 5 different ways:
- For RTL-to-RTL, we use it to check for functional equivalency when
we make a design change, e.g. to improve timing or speed after
we've already verified our design with RTL simulation.
- Structurally, it helps if the designs are similar, though you can
get around it manually.
- Jasper has built-in automation to insert single-sided and
double-sided cut points. It also does internal proofs.
- Formal tools inherently place random values in all flops (as a
two-state sim). So if you have non-reset flops, you can get
indeterminate values and false failures. These will have to be
manually worked around.
- We are starting to use Jasper for clock gating verification when
we have two copies of same design. It works very well.
Automatic Formal Linting (AFL) app - analyzes your design and generates
automatic checks. We not using this yet, as it still generates a fair
amount of noise (with false failures).
X-Prop app - verifies if your unknown X states were handled properly, so
that you don't get unexpected results. It will find out quickly if
there are bugs. It's hard for us to get conclusive proof results
without a lot of effort. We use this app on all our blocks.
Coverage Unreachability app - We use this to save time on simulation
coverage closure.
- This approach is tied to a particular simulator database; we
recently started using it with Incisive NC-Sim.
- When a condition is not covered, we take our NC-Sim RTL simulation
results and feed them to Jasper. Jasper determines if the holes in
in the results are reachable or impossible to hit. Then you go
back and close the hole.
---- ---- ---- ---- ---- ---- ----
Jasper FPV app is the majority of our usage.
- We write our own properties, and define our own verification
strategies, and write our own VIP.
- The tool has very good debug capabilities, waveform debug, source
code tracing.
- The debug tool has additional features like quiet trace that
simplifies signal toggles in a trace down to the basic and
necessary toggle to see the problem, or trace to IO, value change
on the fly.
- Jasper has 23 engines, counting 2 additional ones from Cadence's
latest release. Getting deeper into the design is getting faster.
Sequential Equivalence Checking app.
- We use SEQ, but it's lacking when dealing with cycle schedule
changes. Our workaround is to add fake pipe registers to make
sure that both the reference and target design are equivalent in
depth.
---- ---- ---- ---- ---- ---- ----
JasperGold has a very useful "reverse connectivity" app that generates
the connectivity spec (CSV table) from your known good design, to use
on derivative design. We have large designs SOC's that have a number
of blocks so the connectivity tool is great for IDing the connectivity.
Since this Jasper app extracts the connectivity through the hierarchy,
it provides useful information to our block designers.
---- ---- ---- ---- ---- ---- ----
JasperGold
FPV app
- Mature and feature rich.
- Thumbs up for its flexibility in the setup with the TCL commands
and also for ease of use of the property debugger.
- Cadence could improve the integration of Jasper FPV into the
overall verification platform at Cadence -- still a work in
progress it seems.
Reverse Connectivity app
- Is helpful because generating the connectivity spec from scratch
was a sometimes a big challenge.
Coverage app
- Formal coverage tools have two main uses:
1) providing formal signoff metrics
2) assisting with simulation coverage closure.
The Jasper coverage app is good for formal verification signoff.
- "Proof core" coverage provides a metric of how complete the formal
test environment is. It answers the question: Am I missing to
check any of the design structures with my properties? This is
something that is unique to formal -- simulation cannot directly
report this type of coverage metric about the simulation testbench
checkers.
- The coverage app also provides a metric to gauge the efficacy of a
bounded proof. Another important formal signoff criteria.
- However, when it comes to assisting with simulation coverage
closure, code coverage semantics are inconsistent between tools,
so you can't mix and match. For example, the Jasper coverage app
is cumbersome to use with VCS for simulation coverage closure.
X-Prop app
- A must-have. Finds bugs.
- Could be smarter in the way that it presents the results to the
user. For example, in addition to reporting the multitude of
different places that an X could propagate, it would make things
more efficient if the tool reported the list of unique places where
X originates from to cause all the xprop failures -- which is
typically a much smaller list.
These 13 JasperGold formal apps are nothing more than a pre-packed way
of applying formal to a job that it is really good at. Using formal
in these tasks was being done by early adopters of formal long before
the apps were available and the value of each of the 18 approaches is
well known and accepted.
---- ---- ---- ---- ---- ---- ----
JasperGold Formal Property Verification app.
- We had tried using Cadence IEV (Incisive Enterprise Verifier) in
the past, and it would run for 10+ hours and never prove/disprove
our assertions. Using the same setup with Jasper, on our first
day we were able to identify an issue in just 3 hours. We then
used Jasper to validate the fix and it was able prove the
assertions to pass in 10 hours.
JasperGold Register app.
We have caught many issues in multiple projects using this app.
Pros:
- Jasper supports almost all the register types that we could
possibly verify through UVM simulations.
- Required assertions can be automatically extracted from IPXACT
specification of registers
- Assertions based VIPs can be quickly hooked up to impose the
protocol constraints.
- Able to exhaustively verify the register checks and address
aliasing issues.
Cons:
- No support for serial interfaces.
---- ---- ---- ---- ---- ---- ----
Feedback on a couple JasperGold formal apps:
- Formal Property Verification (FPV) app.
We wrote our own assertion-based VIP properties, plus bought some
of Cadence/Jasper VIP. We then used Jasper to prove the properties,
give counter examples, or give a bounded proof after a certain number
of cycles.
We use this app a lot, and have found and fixed interesting bugs
with it. It's complementary to doing it in simulation and gives better
quality results.
- X-PROP app.
We used it. However we did not find any bugs on our design. This
is likely because we had already run simulation also.
We run XPROP as a final check -- it's complementary to simulation
but does not replace it.
---- ---- ---- ---- ---- ---- ----
I use some of the Cadence JasperGold formal apps.
The JasperGold FPV app is the key app for using FV as verification
strategy. It's for formal verification of design features, and is very
useful in catching bugs early and provides a quick turnaround time.
It also has the ability to find complex corner cases. The debug and
analysis hooks with this app are also very useful.
The Connectivity app is key for areas not covered well by simulation.
It provides a quick check of connectivity as compared with costly
methods employed in simulation.
Coverage Unreachability app detects unreachable code, and is useful app
to flush out early bugs. It is also quite useful to identify
unreachable code for coverage exclusions.
The apps provide significant time savings and help improve overall chip
quality. Strongly recommend.
---- ---- ---- ---- ---- ---- ----
JasperGold's "apps" add features, and cost. :-(
They let untrained engineers use formal verification for more than
just ABV: X-propagation check, super-lint, security verification, etc.
Some are just a different wrapping of the tool (X-propagation), but
others provide a high added value. For example, sequential equivalence
checking app is a real step forward.
---- ---- ---- ---- ---- ---- ----
We use JasperGold's formal property verification (FPV) app, both with
hand-written properties as with auto-generated properties (by our
generators and by VIPs).
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED OF ONESPIN USERS:
Q: "What do you think about the OneSpin DV-Verify apps?
Which OneSpin DV-Verify apps does your project use?"
---- ---- ---- ---- ---- ---- ----
Even beginners to formal can concentrate initially on OneSpin's formal
apps and build expertise over time to create assertions and run proofs.
- OneSpin has static code tests, such as code reachability that are
very useful - everyone should use them.
- We are not yet using their X-propagation app, but may do so in
the future.
- Register checking is a useful app for AMBA-based protocol -- it's
almost push-button.
The automated apps are useful for both verification engineers and
someone with a design background. I'm on verification side, but have
design experience as well. I've met designers who gladly write
assertions and use formal, but not that many go that far -- mostly
they do automated or semi-automated formal, while the verification
engineers take on writing assertions.
---- ---- ---- ---- ---- ---- ----
OneSpin's DV-Verify formal apps are well thought out and useful.
- Safety Analysis app was excellent
- X-Propagation app was also good
---- ---- ---- ---- ---- ---- ----
OneSpin includes formal apps inside the core DV-Verify package. Some
examples of the apps are:
1. Formal linting.
2. Formal checking for X propagation with some tool automation, such
as looking for proper initialization of signals after reset.
3. Flagging arithmetic overflow
4. Identifying state machines in the design and finding unreachable
or deadlock states.
5. Checking for code coverage formally (is a portion of the code
reachable from reset). Flagging signals that do not change value.
The apps may use the OneSpin formal engines under the hood, but the user
doesn't have to write properties manually. The DV-Verify tool automates
creation of properties for these.
---- ---- ---- ---- ---- ---- ----
OneSpin has a set of "design activation" apps for dead code detection,
FSM analysis, toggle coverage, etc.
For example, when we ran it on some designs in progress, we
quickly discovered redundant saturation logic in our datapath logic.
These are typically expensive operations in terms of gate count,
so we'd rather not spend the silicon on them when not required.
Automated SystemC code apps
- We haven't yet used OneSpin for SystemC code.
- We would like to also assess the Mentor SLEC and OneSpin SLEC
solution to compare fixed point C/C++ code for our datapaths
against hand crafted RTL.
Safety critical verification
- OneSpin offers safety critical verification using formal fault
injection to test on chip safety function.
- It's on our roadmap, but we have no direct experience with it yet.
---- ---- ---- ---- ---- ---- ----
I saw OneSpin's DAC demo for its DV-Verify app for SystemC.
It looked impressive. It has the ability to point out problems and
present that information nicely to users.
We are getting more involved with SystemC -- using OneSpin's formal
could save us time and help turn out better products.
---- ---- ---- ---- ---- ---- ----
Related Articles
How engineers feel about Formal verification vs. RTL simulation
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
|
|
