( ESNUG 513 Item 1 ) -------------------------------------------- [11/01/12]
Subject: NextOp and JasperGold Apps on the usefulness of assertion synthesis
> My management wants the pros/cons of using assertion synthesis in our
> ABV suite. NextOp, Jasper, Zocalo, 0-in claim to do it.
>
> - from http://www.deepchip.com/items/0509-07.html
From: [ Yunshan Zhu of NextOp/Atrenta ]
Hi, John,
I'd like to set the record straight.
My company, NextOp invented assertion synthesis. It is supported for
simulation, formal verification and emulation in our BugScope tool.
Jasper announced a similar tool last year. I'm not sure if they have any
production users yet. It may be just a frontend to their formal tool.
Zocalo does not do assertion synthesis. They have a GUI to manually input
assertions.
Mentor 0-in is a formal model checking tool. As far as I know it doesn't
automatically generate functional assertions nor coverage properties based
on simulation.
> We noticed three things about assertion (or property) synthesis:
>
> 1.) The input for assertion synthesis is STABLE simulation info.
>
> 2.) But stable simulation verification info is not available
> until WAY late in the verification stage.
>
> 3.) Also, when our verification suite changes (which it does
> often) we'll need to rerun the assertion synthesis again.
> That means all of our older assertions are now useless.
>
> So how useful is assertion synthesis really? It seems to be just another
> add-on task involving pricey add-on tools when you can only generate your
> assertions very late after most of your verification is done.
>
> Is this assertion synthesis overhead, at a late stage, really productive?
>
> What's the quality of synthesized assertions? Will the time we "saved"
> by synthesis be lost manually checking and rechecking the tool output?
Just like RTL synthesis, good Quality-of-Results is needed for assertion
synthesis to be useful. QoR has two aspects:
1) Whether the generated assertions and coverage properties
are useful to detect bugs or coverage holes; and
2) Whether the assertions have low overhead in simulation
regression and emulation runs.
For item 1 and 3 above, we have 11 large production chip users have seen on
average 70%+ of the generated assertion and coverage properties being marked
as "useful". Thousands of assertions and coverage properties have been
checked in many customer simulation environments. Engineers who think all
these corner cases could have been manually found are crazy.
For item 2 above, we have seen on average of less than 5% simulation
overhead when binding BugScope assertions in the customer's simulation
regression, with on average 100+ gates-per-assertion when using them
in emulation.
All three of these questions are related to the applicability of assertion
synthesis at different verification stages. Assertion synthesis generates
properties that are guaranteed to hold true for ALL simulation runs. If a
property holds true universally, then it is an assertion. If a property is
generated as an artifact of the limited set of simulation tests, then the
negation of the property is a functional coverage hole that has been missed
by simulation.
In early stages of simulation, simulation tests are limited, so assertion
synthesis will generate mostly coverage properties. At around the 30%-40%
verification stage, where basic feature tests have been completed, most
assertions for the block would be generated as well. This is a good time to
check-in the assertions. The assertions will reduce debug turnaround time
as more tests are added.
During the late verification stage, verification engineers should focus on
patching the functional coverage holes identified by assertion synthesis.
At the IP signoff stage, BugScope generates assertions based on the IP tests
and these are shipped to the SoC team for IP integration.
Throughout the verification cycle, the properties generated are tracked by
our Progressive App. This tracking is useful for verification managers to
monitor the process of simulation test development. When the tests or
RTL changes, assertion synthesis is re-run, but the process is incremental.
BugScope automatically tracks the newly generated properties.
> Is it worth the price of 10's of thousands of dollars for a tool to do it?
Assertion synthesis find bugs that escaped your checkers, identifies
coverage holes missed by simulation and allows management to track
verification progress. If the design has complex control, then assertion
synthesis adds sufficient value.
> Is it worth the price of 100 man-hours learning and maintaining the tool?
Assertion synthesis is about automation. On average, it takes about 1-2
minutes to create an assertion using BugScope. Compare this with the fact
that human efforts that can take hours-or-days per assertion.
> Which assertion synthesis tool is the best? Which is the worst?
BugScope is the best, by far. But that is just one man's opinion. :-)
- Yunshan Zhu
Atrenta/NextOp San Jose, CA
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
From: [ Asa Ben-Tzur of Jasper DA ]
Hi John,
I believe this user's main claim refers to his project timeline. While one
may write a property before any design/verification content is available,
all automated tools require that your property is implemented in RTL and
exercised to some extent by a test for that property to be synthesized.
To reap a property value (i.e. find a bug using simulation) you would need
the RTL implementation and test content anyway.
---- ---- ---- ---- ---- ---- ----
Yes, it's true you can use formal tools to benefit from ABV (assertion
based verification) properties without any test content. For instance, with
our JasperGold, you can use ABV assertions as soon as they are available in
your design. The JasperGold SPS App lets you synthesize properties from
your RTL design before any test environment is available -- and you can use
other Jasper Apps during your project lifecycle, letting your verification
content increase as your design and verification environment matures.
---- ---- ---- ---- ---- ---- ----
Concerning your question about stability, our property synthesis App for
ABV does not require a "mature and stable" verification environment. True
assertions and constraints can be generated from early test content and
can be refined as test content matures. Your property synthesis results
are updated as your design evolves -- much like human written properties
that need to be maintained -- but with automation support.
JasperGold's property synthesis App supports "black-box" property synthesis;
namely synthesizing properties at design interfaces. Interfaces tend to
stabilize sooner in the project lifecycle and maintain stability across
projects, bringing higher value to property synthesis and/or
specification investment.
---- ---- ---- ---- ---- ---- ----
Regarding this concern about the value of your old assertions when you tweak
your verification suite, JasperGold's property synthesis App supports design
evolution by refining synthesis results and highlighting changes between
design and verification milestones. Your investment in stable properties is
preserved, while properties that have changed are highlighted.
Once you embed selected properties in your design, JasperGold will recognize
these embedded properties and will not present similar properties for you
to review. Our functional filtering and property ranking reduce your review
effort by presenting synthesized properties in priority order.
WORD OF WARNING:
A property can only provide value once it has been developed and maintained.
I would encourage you to apply ABV broadly across the entire design, whether
manually or automated. Real-life experience has shown us that that ABV
deployment is sometimes limited due to the effort involved in developing and
maintaining properties.
Property Synthesis offers a BIG productivity gain in ABV deployment if it's
done right. It's value is not limited to an ABV methodology. You can use
property synthesis for other purposes like:
- finding coverage holes,
- bug hunting,
- design reviews and
- various flows sharing content between simulation and formal
environments.
JasperGold Apps do property verification and property synthesis for formal
environment bring-up and getting convergence on complex proofs.
- Asa Ben-Tzur
Jasper DA Haifa, Israel
Join
Index
Next->Item
|
|
