( DAC'20 Item 04b ) ----------------------------------------------- [03/09/21]
Subject: Users say Jasper's 200K register block signoff is Best of 2020 #4b
FORMAL BLOCK SIGN-OFF: A *major* change in this year's report is that it's
the first time engineers have commented about using JasperGold alone for
SoC block-signoff -- and with NO dynamic simulation whatsoever! Whoa!
And this "block sign-off with only formal" feedback came from 3 unrelated
users:
"Further, in the past year we have also been able to use JasperGold
to signoff some blocks with formal only."
"FPV for block-level verification (end to end). The biggest improvements
here are Visualize, over constraint debugging, and being able to
formally sign-off a block using only formal coverage."
"Block verification. This is so complete that we can use JasperGold
to signoff our digital blocks -- i.e., we do signoff using
formal verification and eliminate RTL simulation."
"We can completely verify the block without developing a dynamic test
bench (UVM), thanks to the availability of the JasperGold formal
apps we use, including: FPV (Formal Property Verification), Superlint,
CSR (Control & Status Register), CDC, and COV (coverage)."
Keep in mind that block-level signoff used to only be done by a dedicated
verification engineer writing enough end-to-end properties for the Jasper
FPV app to fully verify block functionality. They still do that now, but
block sign-off can also now be done by an RTL designer using a mix of
apps with built-in assertions and writing additional assertions using FPV.
I immediately called the Cadence R&D guys for hard numbers on capacity and
runtime on their ability to do "full sign-off using on Jasper formal and
absolutely NO Verilog / System Verilog / VHDL simulations at all".
After a *lot* of abusive Cooley Q&A on them, their final summary was:
"For FULL block sign-off,
- max block size ~200K registers; this could be up to 5-10M gates
without black boxing.
- It's state space that matters for formal, so # of registers is
a better gauge than gate size.
- Design style also matters -- e.g. degree of parallelism;
parallel protocols are better than long serial protocols
- For the above, Jasper users get results in under 24 hours
- Formal is particularly good because you get all combinations
of stimulus for free. It's the key reason Jasper is used for
processor verification. Any IP targeting unknown data input
can lend itself to formal -- especially where good testbenches
are typically more difficult to capture in simulation.
Outside of this scope, Jasper can compile large SoC sized designs;
(we regularly test with designs up to 600M gates.)"
- Cadence JasperGold R&D email to Cooley (02/24/2021)
---- ---- ---- ---- ---- ---- ----
ML-TRAINED PROOFS: The 2nd new thing this year is the users have started to
cite is Cadence's "smart" machine learning to speed up its proof engines.
Anirudh discussed this directly at my 2019 Troublemaker Panel.
"Right now, you run verification for 6 months and you still don't know
whether you are finished with verification or not. So, overall
verification closure is a great area for machine learning."
- Anirudh Devgan, CEO of Cadence (ESNUG 588 #2)
The user comments on ML driving JasperGold proof engine choices:
"What is most important for my group is that Cadence has improved the
automation of the proof process, adding multiple features. The tool
uses machine learning to do it automatically, and the results are
on par with a careful selection by a human. This saves us engineering
resources; our engineers no longer spend time selecting engines or
a proof strategy."
"JasperGold uses "Smart Proof Technology," which is CDNS marketing-speak
for machine-learning algorithms used to automatically pick which exact
proof engine to use on subsequent runs. (No human intervention needed!)
We turn it on and get a big speed-up on our formal regression tests."
---- ---- ---- ---- ---- ---- ----
APPS, APPS, APPS: CDNS R&D stepped up improvements on their JasperGold formal
apps this year. There's users here discussing 11 of them: FPV, SEC, X-Prop,
Coverage, Security, Control and Status Register, Unreachability, Superlint,
Connectivity & Reverse Connectivity, CDC, and C-to-RTL.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen in 2020? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
Cadence has improved JasperGold this past year by increasing the proof
engine performances and adding new engines.
What is most important for my group is that Cadence has improved the
automation of the proof process, adding multiple features.
- The tool uses Machine Learning to do it automatically, and the
results are on par with a careful selection by a human.
- That saves us engineering resources; our engineers no longer
spend time selecting engines or a proof strategy.
We continue to use JasperGold for block verification, integration,
equivalence checking, security verification, coverage closure, checks
such as X-propagation, and deadlock verification. Formal verification
still gives us an advantage over simulation for those areas.
Further, in the past year we have also been able to use JasperGold
to signoff some blocks with formal only.
We've also used Cadence's 'deep bug hunting' to find bug 100's cycles
deep in small designs. The UI is intuitive.
Formal Apps
- We have increased our usage of the SEC app. It is now mainstream
for us to use in areas such as minor RTL changes, full RTL
rewrites, clock gating, design for verification checking, etc.
- The X-propagation app has good potential as simulation is not
able to catch X-prop issues. Cadence is investigating our
test cases to understand why performances are not better.
- Cadence has done a full rework of the Security app this past
year and incorporated a lot of our inputs. We need to do an
in-depth evaluation, but the first results on our designs
show an improvement in runtimes. The speed-ups came with
the tradeoff of losing some features, but they will be added
back in future versions.
Cadence's AE & R&D support and expertise continues to be very good.
---- ---- ---- ---- ---- ---- ----
We use JasperGold for:
- Block verification. This is so complete that we can use
JasperGold to signoff our digital blocks -- i.e., we do signoff
using formal verification and eliminate RTL simulation.
We can completely verify the block without developing a
dynamic test bench (UVM), thanks to the availability of the
JasperGold Formal Apps we use, including: FPV (Formal Property
Verification), Superlint, CSR (Control & Status Register),
CDC (clock domain crossing), and COV (coverage).
- Integration level. At the integration level, we use both UVM
and a formal flow. Here, we use the UNR formal app to remove
unreachable code and the Connectivity app for connections to
GPIOs and analog macros.
When we use formal along with dynamic simulation for verification, but
we run formal first in our flow.
Smart Proof Technology & Machine-Learning
JasperGold uses "Smart Proof Technology," which is CDNS marketing-speak
for machine-learning algorithms used to automatically pick which exact
proof engine to use on subsequent runs. (No human intervention needed!)
We turn it on and get a big speed-up our formal regression tests.
Visualize Debug
Visualize is one powerful debugger! It makes it easy to analyze
failures and reach their root cause. Debug with counter-examples is
one of the most important features I need in a formal tool.
Learning Curve/UI
JasperGold's user interface is quite intuitive. In our team, the
rookie designers are able to start using JasperGold in only a few days.
They get a 4-hour introduction training on the basic concepts of
formal and this can be enough to get them started.
ProofCore tags are what is covered by the set of properties. It's
important to understand the different levels of formal coverage, as
formal coverage, by itself, is not equivalent to dynamic simulation.
Engineers understand the different RTL coverage levels in 1 hour.
JasperGold Apps
Cadence's support is strong - they help us continue to improve how we
use Formal Apps by providing us with tips, examples, and dedicated
training. Below are some of the apps that we use.
1. FPV. We use FPV to develop and prove our custom assertions.
It has a ton of features and settings to reach convergence,
and is the most used app in our flow.
2. Coverage (COV). Used for signing off digital blocks. The
app settings are very easy for our designers.
3. CSR (Control & Status Register). For our digital blocks,
we now always verify the registers with CSR, and no longer
with UVM. So, we use this app widely.
4. UNR (Unreachability) is very useful to clean the coverage
from dead/unreachable code. We use this widely also.
5. Connectivity and "reverse connectivity". We use Connectivity
to check the GPIO connections, as well as the analog macro
connection. We sometimes used the "reverse connectivity"
function, but it needs automatization for completeness.
6. Sequential Equivalence Checking. We use this occasionally,
mainly to verify a change/improvement on an FSM, or when we
introduce a new feature and want to check that the original
features have been maintained.
7. Superlint. We use this app widely as first step of Formal
Flow. With Superlint we can clean the early-version RTL
code from dead/live locks, dead code and other possible
bugs that sometimes appear in the first versions of code.
Moreover, it helped debug the DFT issues in our blocks.
I strongly recommend JasperGold for anyone who wants to use formal to
verify their design. It's a complete environment for IP signoff.
---- ---- ---- ---- ---- ---- ----
We use JasperGold a lot. Mostly for pre-silicon, but we also have a
few projects where we use it for post-silicon debug.
Our formal verification (FV) teams use it for blocks/unit signoff, and
our designers sometimes use it for design-exploration (though less
frequently). The importance and benefit of FV over simulation is well
accepted by our management.
- We have teams that use JasperGold on an SoC, but the capacity
to do that depends on the checks done. E.g., our SoC level
testing is usually only connectivity checks.
- At the block/IP-level, it's used for signoff in some cases
and bounded proofs in others. (Depends on the block size.)
JasperGold has engines that will solve the properties one by one, and
others that will solve multiple properties at once. We often use the
multi-property engines, because we've seen them prove properties.
The main drawbacks of doing formal verification are:
1) the acute shortage of experienced FV people
2) the uncertainty whether FV will eventually converge
3) and while most managers understand simulation well,
they still see FV as "magic".
DEBUG
I started my FV work with JasperGold. Engineers that used to work with
other FV tools say debugging was much harder with the other tools.
Today, we give our RTL designers a session on JasperGold -- or the Tcl
commands to run it -- and they can easily understand what's wrong with
their designs from all the JasperGold features, such as:
- "why" <-- the reason that a signal got this value at this
cycle. This is a great debug feature.
- "what-if" <-- changing the value of some signals at specific
cycles to see the impact
Cadence suggests a few bug-hunting techniques and is open for other
implementation ideas for their "hunt" command. The techniques,
especially deep-bug-hunting, do require some effort, as the engineer
must supply some interesting cover points which JasperGold looks for.
If there are 100s or 1,000s of cycles, then the tool continues to
search around the location to potentially find a bug.
"Visualize" is good and continues to progress. Engineers familiar
with Verdi, often ask for features like Verdi has. Cadence is open to
listening to our requests, and if the request is legitimate, they add
it to Visualize.
The "Quiet trace" feature cuts down on signal activity and is very
useful for someone who's less familiar with the design and can be
confused by irrelevant signals. The "wave-edit" (what-if) feature is
useful, but not well-known to our team.
Problem: There are issues with taking a design snapshot and then
continuing the debug without re-initiating the formal engines from
the beginning. There are some solutions for this, but they require
additional work.
GUI
If someone is familiar with FV, JasperGold's learning curve should be
quick. For new users, the mass of options (that other users asked for
and Cadence added) can cause some disruptions due to the complexity.
FORMAL COVERAGE
JasperGold's way to avoid over-constraining is fairly straight-forward
and has no convergence issues. It's the one we use the most.
Problem: The proof-core analysis sometimes does not converge on part
of the properties. Plus, there are a few questions as to which level
(e.g., "high_precision") will get adequate results and convergence.
Bounded-proof analysis gives useful data and usually doesn't require
much effort from the formal engine.
JASPERGOLD'S APPS
- Formal Property Verification App (FPV) -- is the main tool and
therefore the most used one. Engineers usually write their
own properties or instantiate some home-made libraries. The
assertion-based VIP is used less often, partly because the
interfaces are not standard.
- Superlint -- We use this for creating properties, primarily
for dead code checks.
- Sequential Equivalence Checking (SEC) -- is gaining more use.
Main use cases are clock-gating and design changes. Cadence
sees it as one of their best apps.
- Connectivity -- is widely used by our teams.
- Reverse connectivity -- we've used this for cases where we
wanted to know which bit of an input bus went to which cell
(i.e. fuses per memory), and it was very useful. However,
have not tried it on more complicated reverse-connectivity
cases.
CONCLUSION
We've been using Jasper for nearly a decade, after doing a detailed
evaluation.
We get great support from Cadence. I've worked with other EDA vendors
on non-FV tools -- the access we get with Cadence RnD is exceptional.
We keep getting new stories on bugs that were found only by FV, and on
the process of "shifting left" to get a cleaner design following design
team handoff.
We keep getting new stories on 1) bugs that were found only by formal,
and 2) using formal to get a cleaner design following our design team
handing off the RTL, as part of our "shift left".
If you have the budget, JasperGold it the formal tool you are likely to
buy.
---- ---- ---- ---- ---- ---- ----
I've used Cadence JasperGold for 7 years now; it is our cockpit for
running a lot of formal verification (FV) tasks on a design. I start
using JasperGold as soon as the RTL code starts to become available
and I have a specification to verify. I must make sure RTL behavior
matches the design intent.
JasperGold Formal vs. Dynamic Simulation
A big advantage for JasperGold over simulation is that it's exhaustive;
this means you don't miss bugs that require multiple events happening
at the same time.
For example, with our complex CPUs, I like to verify our lower-level
modules first with JasperGold, then I hand over the design to the
top-level verification guys, where they use simulation.
Jasper is more productive for verification at lower levels, such as
instruction-fetch and instruction-decode. (A unit level check might be
at the outputs of the DUT.) And because formal technology is orthogonal
to simulation, it complements simulation nicely.
With both simulation and emulation, we must apply stimulus/vectors.
JasperGold doesn't require stimulus. And because FV is so exhaustive,
we can find bugs even for corner cases.
Performance/Capacity
JasperGold can work on multiple properties in parallel; this is a very
useful function that has been there for many years.
In terms of capacity, we find JasperGold is effective in finding bugs
for designs with fewer than 100,000 flipflops and under 2 million gates.
Above that, JasperGold ABV starts to lose its advantage.
We ran a 2 million gate design on JasperGold, and it compiled in less
than 3 minutes. Then ran full proofs on less than half of our checks.
The others didn't converge, but we don't need 100% convergence -- we
can decide how long to let JasperGold run.
- If the RTL is continuously changing, we can typically find a
bug in 1 hour.
- If the RTL is stable, then it can take 24 hours to find a
bug, or even 60 hours (we let it run over a weekend).
JasperGold will check every combination up to a certain sequential
depth. We learned how to use bug hunting techniques along with
abstraction to find deeper bugs; we might find them at a depth of 20,
then find a bug at 29 deep, but miss a bug that is 25 deep -- meaning
it takes expertise to run JasperGold ASB correctly.
New Machine Learning Speedup
Cadence has added machine learning to JasperGold to speed up the proofs
and regressions, although I haven't used it yet. I am curious how ML
will increase the regression efficiency with our runs.
Set Up: Simulation vs. Formal
With simulation, you must set up your testbench. Then spend time
applying vectors and hitting corner cases in the simulation run.
In formal, the tool honors all the constraints by default. So, the
engineer must spend time ensuring constraints are correct and that they
are not applying illegal stimulus. If the formal tool is not properly
constrained, it will try all possible combination of inputs, and
unexpected failures can occur. It requires expertise!
Once the initial work is done with the constraints, the next step is
trying to make the formal tool go sequentially deeper. So, we set
over-constraints, or code targeted checks (using case splitting for
example) to do exhaustive verification on deeper cycles.
Both formal verification tools and simulators require checkers. At the
heart of a formal checker, there is always an SVA. To keep them
efficient for formal, your JasperGold checks need to be coded quite
differently from your simulation checks.
Our primary reasons for using JasperGold over simulation (at the unit
level) whenever it is feasible are:
1. JasperGold is orthogonal to simulation; it's a complementary
verification technique at a lower level, and then we can use
simulation at a higher level.
2. If a particular portion of our design is seeing a lot of
change, and either a simulator testbench or formal testbench
must be done from scratch -- then the formal bench is usually
faster to bring up. This is because you don't need stimulus
or templates to configure the design properly. (JasperGold
will apply all possible combinations.)
Note: this second reason doesn't apply if you already have a simulation
testbench. Then only reason one applies.
JasperGold Debug
We've used JasperGold to go 100 cycles deep, but that is rare. Our
average depth is between 20 to 30 cycles -- because we find most of
our bugs are at less than 25 cycles.
JasperGold's Visualize debugger is my bread and butter for debugging
and "root causing" a failure. Cadence continuously improves it.
- First, JasperGold gives us a failure to debug.
- Then, if the failure is 25 cycles deep, we can use Visualizer
to take the existing wave, freeze what it did for first "20"
cycles, and then apply constraints differently for the next 5
cycles and generate a new wave. So, we can get there quicker.
It's like an interactive debug, with new stimulus and new wave with
quicker turnaround time.
I'd like Cadence to add this feature: If I did a run last week, and had
design and testbench changes this week, I'd like to be able to compare
my new JasperGold run to last week's run. This could be in or outside
of vManager, but it needs to be fairly lightweight to use. This would
be useful to keep track of what are the new failures, or which failures
disappeared, etc.
Cadence has ProofCore coverage, and stimulus coverage analysis for code
coverage. The stimulus coverage can be used to look for dead code. The
proof core can be used to analyze holes in your checking.
Some engineers use JasperGold for higher coverage. I like using it to
give me a mental map of where our verification holes might be, and if
they are okay. We are not trying to verify *every* feature in coverage,
but rather specific features. JasperGold helps identify areas where
additional effort is needed (i.e. it's not an official coverage checking
tool.)
The UI is good.
JasperGold Formal Apps
Formal Property Verification App. FPV is really the core functionality
of JasperGold. We write assertions for this one, some are simple, and
some are complex.
These other apps are for special cases that our everyday designers use;
CDNS R&D added syntactic sugar around each for each specific use model.
Maybe the engine is tuned also.
- SEC
- XProp
- CDC apps
- Security
- C-to- RTL <-- we are evaluating this now.
Training & Support
I'd recommend JasperGold for companies doing formal verification.
Cadence has lots of training material, including videos to help users
get stated. They have two days of training for design engineers and
for verification engineers. (The formal engineers must be able to
write Verilog assertions efficiently.)
Cadence also has excellent support. We get smart and capable AEs, who
are able to help us directly for a lot of our problems.
---- ---- ---- ---- ---- ---- ----
We think that JasperGold is the best-in-class formal tool with great
proof performance and a good user interface. We use it throughout
our design and verification process for block and mini-cluster level
verification, register verification, CDC verification, and sequential
equivalence checking. We usually use FPV at block level for designs
up to 100K flops.
We generally use JasperGold formal apps like FPV, SEC, CONN, CSR, CDC,
COV, XPROP -- instead of simulation. Specific formal apps like CONN
can be applied at the SOC level. We are also trying to bring CSR to
the SoC-level; it is still a work-in-progress.
What we like about JasperGold:
1. If you have enough licenses, JasperGold has killer multi-threading
capability which improves performance by at least 3X.
2. The debug is very good. It has nice GUI features that greatly
help, such as the "why" analysis, quiet trace, and it evaluates
other properties. Cadence could improve debuggability for their
newer formal apps like CDC. E.g., a better/easier root-cause
analysis tool for debugging metastability-related counter-examples.
In general, we don't rely much on bug hunting for our block-level
design. Instead, we try to use other techniques to get full proof
or bounded proofs with sufficient bounds. We use the bug hunting
algorithms for coverage trace search. As we take more larger
designs into formal, we plan to rely more on bug hunting techniques.
3. The user interface is easy to use; but there is a non-trivial
learning curve for people to get used to the JasperGold GUI due
to its complexity. Some of our engineers complain about using
Tcl scripts to code complex algorithms; they would prefer more
up-to-date language like Python.
4. In general, JasperGold provides comprehensive coverage analysis
tools to help analyze formal results.
5. WARNING: The methodology requires a learning curve for new users
to understand.
Cadence's support has always been great in terms of supporting normal
use as well as helping us develope new methodologies.
Formal Apps
Some more input on the JasperGold formal apps we use:
- Formal Property Verification App (FPV). This is best in class
in terms of engine capability. SystemVerilog language support
is in general good.
- Sequential Equivalence Checking. Cadence has the best SEC tool
with some unique capabilities that other tools don't offer.
- Connectivity and "Reverse Connectivity". We use reverse
connectivity often to sanity check our RTL and the manually
created connectivity map. It is useful. Another nice
feature is the toggle check, which helps to check unexpected
design constants such as tie-down.
- X-Propagation. We use the XPROP app as part of our formal
signoff flow. In general, it is very easy to use. We'd
like Cadence to provide more visualized coverage to help
our engineers understand what has been verified.
I would definitely recommend JasperGold -- it makes our formal
verification engineers' lives easier and happier.
Formal has become a critical piece in our verification strategy, and we
use it to replace simulation wherever we can. JasperGold's great tool
capability and customer support play a very important role in helping
us adopt formal verification.
JasperGold's also has "Smart Proof" technology which uses machine
learning that we plan to use, but we haven't use it in production yet.
---- ---- ---- ---- ---- ---- ----
Cadence has made a number of JasperGold improvements in the past year.
I've definitely experienced faster proof convergence on successive
runs. Cadence added machine learning for this ("Smart Proof"), and
has done so in a way that it is transparent to the user.
JasperGold's apps improvements this past year:
- FPV for block-level verification (end to end). The biggest
improvements here are Visualize, over constraint debugging,
and being able to formally sign-off a block using only
formal coverage.
- SuperLint for FSMs. Cadence has improved FSM deadlock, FSM
livelock verification and the ease of use.
- SEC (Sequential Equivalence Checking). Better ease of use.
We are extremely happy with Cadence's AE support. What's new is their
AE support is seamless. That is, I get the same level of good support
(or more) no matter who my AE is.
I recommend JasperGold 100%. It's a great product that is well
supported by great AEs. One cannot do one without the other.
---- ---- ---- ---- ---- ---- ----
We like JasperGold and my designers use its apps every day
---- ---- ---- ---- ---- ---- ----
I feel I should nominate JasperGold to be a "Best of 2020".
---- ---- ---- ---- ---- ---- ----
Our purchasing department says Synopsys VC Formal is good enough.
I'd rather we used JasperGold. It'd look better on my resume.
---- ---- ---- ---- ---- ---- ----
We were going to do JasperGold and Conformal LEC until our SNPS sales
guy dropped his pants and gave us VC Formal and Formality for a song.
---- ---- ---- ---- ---- ---- ----
Related Articles
OneSpin's "going where Cadence isn't" approach is Best of 2020 #4a
Users say Jasper's 200K register block signoff is Best of 2020 #4b
OneSpin extensible ABV plus formal linting is the Best of 2020 #4c
Join
Index
Next->Item
|
|
