( DAC'16 Item 1a ) ---------------------------------------------- [12/09/16]
Subject: How engineers feel about Formal verification vs. RTL simulation
AND IN CAME THE FLOOD: I should have seen it coming. With Jim Hogan's big
big 5 part guide to Formal EDA tools appearing on DeepChip (ESNUG 558 #5)
earlier this year -- plus its high reader pageviews -- and vendor reaction
letters Jim's guide garnered, I should have predicted it. But I hadn't.
This year my annual "What's The Best Tools of 2016?" survey question got me
flooded out -- 6,000 words of initial flood actually -- from the EDA users
themselves gushing about either the JasperGold or OneSpin formal tools.
Curious, I did separate a follow-up question to the Jasper and OneSpin users
to see how Formal compared to the old school RTL simulation way of verifying
designs. That created an additional 2,000 words.
P.S. Notice how the users do NOT see Formal as replacing RTL simulation, but
instead see both as a "soup and sandwich" combo that works well together.
P.P.S. As a consequence all this gushing, instead of one email blast with
the DeepChip Top 5 of 2016, I'm publishing all these formal user comments
as the #1 tool category of 2016 -- and will later publish #2 through #5
tools of 2016 in a separate email blast.
First, here's the OneSpin users on DV-Verify vs. RTL simulation:
FOLLOW-UP QUESTION ASKED TO ONESPIN USERS:
Q: "What are your thoughts about using OneSpin
formal vs. RTL simulation on your project?"
---- ---- ---- ---- ---- ---- ----
I highly recommend any formal tools (such as OneSpin) as an addition
to RTL simulation. Your workflow then becomes:
1) First, attempt initial verification with formal tool. When the
properties are proven, they are exhaustively proven.
2) For property verification, or code coverage, or X-propagation,
formal tools are much easier to setup than writing simulation
testbenches
3) For properties that cannot easily be verified with formal, then
follow through with your RTL simulation.
The learning curve for getting started with a formal tool like OneSpin
is small -- even smaller than setting up RTL simulation testbenches.
---- ---- ---- ---- ---- ---- ----
We've found that OneSpin formal and VCS/Incisive RTL-simulation are
complementary -- rather than one versus the other.
OneSpin is exceptionally useful for the block-level verification of
control-flow structures and finding scenarios you haven't thought of.
---- ---- ---- ---- ---- ---- ----
Formal and Verilog/VHDL RTL simulation are so different.
To run simulation, you have to build a testbench and hand write all
of your test cases.
With OneSpin formal, and I suppose with any formal verification tool in
general, you can start sanitizing your design with just a few clicks of
a button. At DAC some OneSpin user described how some verification
groups at his compaby were abandoning "block-level and verify" at the
subsystem level and up -- and using formal to fill in the gap in the
unit level.
Some say verification engineers are the ones who do formal work, but I
have also heard of designers being more involved, and probably rightly
so, as it requires in-depth knowledge of design implementation.
Formal is not free though. Only limited runs can be done without doing
extra work. To go further, you have to start writing SVA -- which means
decide which exact SVA needs to be written -- and which engines to run,
etc. This requires technical expertise that most verifiers/designers
don't already have.
---- ---- ---- ---- ---- ---- ----
The problem with simulation-based verification is that it has become too
difficult. Let me explain.
We used to have just Verilog testbenches with some directed RTL tests.
- Everybody understands that concept because it's embedded in our
education. Cause and effect.
- For logic verification this works as long as you can cover all the
possible relationships between inputs and state on one hand and
expected outputs on the other hand.
- Unfortunately, this quickly becomes an enormous space as we have
2^(# of inputs + # of states) to cover.
Humans generally lack the brains (and time) to describe this search
space in sufficient detail through directed RTL testing -- so we went
from directed testing in simulation to constrained randomized testing
in an attempt to better cover our search space.
In essence we'd like to cover the complete space to be 100% sure no bugs
are lurking below the surface. With constrained randomized plus early
assertions, we went from a 100 page Verilog syntax book that covers the
language -- to a 1000 page SystemVerilog book plus a few books on UVM.
Suddenly verification has moved from procedural programming and golden
reference files to OO design patterns and a completely different way of
thinking about stimuli with distributions, sequences, layered sequences,
etc...
So, imagine now a junior engineer entering the team. In the old days
he/she would be a reasonably good design and verification guy after
about 2 years on projects. Everybody on the project would have the
same level of understanding more or less and things were good.
NOW, these days with UVM et al:
- We get juniors going by doing *some* directed stuff at first, and
then we expect that they gradually move to more complex features
such as randomized.
- What we see however is that after 2-3 years a lot of them are still
doing directed stuff.
- So now we have this high overhead of setting up UVM and we're still
basically doing directed -- because that what people understand.
This becomes even worse when we have to staff bigger teams with
external consultants, etc.
- The verification environment tends to be *dumbed down* to the common
level because we need to get this thing done with too few people
having very diverse backgrounds (often due to a very limited amount
of engineers available) in too little time, so it's important that
every day *some* progress is made.
- At some point later it becomes clear that we don't have sustainably
succeeded in doing better verification.
BUT, with formal tools like OneSpin (or JasperGold) we kind of bypass
the mantra that it's hard to imagine all possible combinations.
- The formal tool constructs *all* combinations based on what we say
should or should not happen.
- The "should not happen" bit is often more interesting. It also
goes against the education of cause and effect reasoning, but it
seems much less of an issue to explain to people and to implement
as compared to doing constrained randomized testing.
- With formal we're forced to actually think about the *design* rather
than sequences and scoreboards. The design/chip is what brings in
the money, not some fancy testbench.
Let's not fool ourselves either: full verification using only formal is
no joke -- and for most designs it's totally impractical.
What we do gain, by *adding* formal, is that we can put it in the hands
of the designers, early in the project. As a result, we spend much less
time later doing top-level verification based on good old UVM simulation
hoping to find bugs in the submodules.
---- ---- ---- ---- ---- ---- ----
I see formal and simulation as complementary.
OneSpin has great formal technology and tools.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
And now here's the Cadence users on JasperGold vs. RTL simulation:
FOLLOW-UP QUESTION ASKED TO JASPER USERS:
Q: "What are your thoughts about using Jasper
formal vs. RTL simulation on your project?"
---- ---- ---- ---- ---- ---- ----
We can reach corner cases in RTL much faster with JasperGold than by
a random behavioral simulation.
---- ---- ---- ---- ---- ---- ----
For us, JasperGold has been key deploying formal verification; formal
now competes against simulation and emulation, and is gaining more
and more importance.
---- ---- ---- ---- ---- ---- ----
The JasperGold formal tool is the best way we've found to quickly
verify functionality at the block and sub-block level. It is
complimentary to RTL simulation. We're seeing cases where simulation
is not keeping up with the complexity. Resourcing traditional
testbenches for each block is not feasible anymore.
Also, the assertions we developed for Jasper are fully reusable in
simulation. I see these assertions as a handoff point between formal
and simulation.
---- ---- ---- ---- ---- ---- ----
We see JasperGold as a as complement to simulation, not a replacement
for simulation. The strengths of one approach covers the weaknesses
of the other.
Once I had finally learned the fundamentals of formal (not easy to do),
it was fairly effortless to use on designs developed by other engineers
in our group -- designs which I was not too familiar with.
For folks who are from a traditional RTL verification background, there
is some pain initially -- but it always helps if one has a design in
mind that they want to push through formal.
---- ---- ---- ---- ---- ---- ----
JasperGold formal gave us a huge time savings by improving efficiency
of verification for some tasks. I don't know if the other formal tools
would have done this because we only use Jasper,
Rather than formal vs. simulation, I prefer to think about it as formal
plus simulation. Use the right tool for the job.
---- ---- ---- ---- ---- ---- ----
Jasper's bug hunting engines can go 1000's of cycles deep into a design.
So you can do a "cover" property to get to an interesting state, then
search for bugs from that state.
It doesn't go as deep as you can with VCS/Incisive/Questa simulation,
but the state space can still explode, so Jasper needs to reduce it.
JasperGold's time savings comes from quick debug turnaround. If you
deploy formal on an appropriate block, it can find bugs much quicker
than simulation. You can potentially build environments more quickly
this way than with some complex UVM testbenches.
---- ---- ---- ---- ---- ---- ----
Formal verification is completely different from simulation-based
verification. In order to write effective properties for formal
verification, your engineers have to change their way of thinking;
thus intensive support is very important.
The Cadence Jasper technical support is extremely good. The Cadence
AE visits us once a week and takes care of our engineers who are
just starting to use Jasper. That support made all the difference
to our projects.
---- ---- ---- ---- ---- ---- ----
It is always more efficient to use formal tools versus simulation to
verify configuration registers and connectivity. In both cases,
exhaustive verification cannot be done just using simulations, so
formal is the way to go!
WARNING: Formal may not be ideal for datapaths verification, but is
a very good option for control logic verification.
We tried JasperGold on a previously verified designs which used the
traditional simulation-based techniques. With minimal assertions
and effort, it identified 2 corner case bugs that had not been found
on these designs despite years of simulations having been run.
Because of that, we are working to incorporate JasperGold as a bug
hunting engine earlier in our design process. It's been immensely
valuable. We have seen failures exposed with trace depths of 80 to
100 cycles and once the design was fixed, Jasper was able to prove
assertions that required over 400 cycles to close. (!)
We have found that formal verification, when targeted at appropriately
at control logic, significantly outperforms simulation and emulation.
It cannot replace simulation for all tasks, but its increased capacity
lets formal take on more of the tedious simulation-based tasks.
If your previous experiences with formal left you with the notion that
it requires high effort and is difficult to master, you should take
another look. Formal tool capacity has increased significantly and new
ease-of-use features make anyone with basic SVA and DUT knowledge will
be productive.
---- ---- ---- ---- ---- ---- ----
Right now, Jasper is more about getting better design quality than in
saving time. Our current approach is:
- Run Jasper Gold early before we have our testbenches; great for
finding bugs early.
- Do mid-project RTL simulation; still our biggest focus for
uncovering lot of bugs.
- JasperGold formal comes in again at the end to improve quality
as we head toward tape out.
We use formal with simulation; not instead of simulation.
---- ---- ---- ---- ---- ---- ----
Before trying Jasper, we had experience with multiple formal tools
which we used for doing "traditional" formal verification (O-in/Questa,
CDNS IFV, Magellan) with manually written assertions. All these
other formal tools we used previously suffered from capacity problems
with anything other than small blocks.
When we first tried Jasper, surprisingly, it could exhaustively prove
end-to-end assertions for large blocks and sub-systems, that we had
never considered running formal on before.
Case in point, we used Jasper for debugging 4 post-silicon issues and
validating the 4 fixes (both silicon and software fixes) before then
recommending them to the customers. Standard RTL simulations were
very unproductive in IDing the problems -- as the test cases would
run for hours on a board. For Jasper, by writing a minimal set of
required end-to-end assertions after brainstorming with designers,
we were able to use Jasper to hunt identify the issues and try out
the fixes.
---- ---- ---- ---- ---- ---- ----
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
|
|
