( ESNUG 519 Item 2 ) -------------------------------------------- [02/14/13]
Subject: NextOp says dynamic analysis is what makes assertion synthesis work
> AVERY PROPSYN VS. ATRENTA NEXTOP BUGSCOPE:
>
> NextOp BugScope relies on data mining waveforms to extract the interesting
> invariant properties which can be initially rather incomplete based on the
> range of tests available to run regressions with. QOR seems hard to claim
> during early stages of design. Users have to manually classify properties
> as assertions, coverage holes, or "don't cares".
>
> Avery PropSYN coverage metrics are generated and used very early in the
> design flow to ensure the quality of the regression tests that are still
> being developed.
>
> We also focus more than BugScope on the coverage of the implied hardware
> functions of the design to give greater visibility to the control logic
> corner cases.
>
> - Chris Browy of Avery Design
> http://www.deepchip.com/items/0514-02.html
From: [ Yunshan Zhu of Atrenta/NextOp ]
Hi, John,
As that NextOp guy, I'd like to clarify my comments.
Chris went on to describe how his PropSYN uses static methods to analyze RTL
and generate assertion and coverage property based on design templates.
From what I've seen in our customers, the most useful functional assertions
typically do not fit in any static design templates. Dynamic analysis of
simulation is what makes assertion synthesis work.
Here's 3 examples of synthesized assertions and coverage properties. All of
them have found real bugs. I don't think it is feasible to generate them
effectively without dynamic analysis.
Example 1:
module mctrl(rdy_i, addr_i, data_i, rdy_o, addr_o, data_o);
rdy_i -> !isunknown(addr_i);
This assertion captures a key design assumption that when rdy_i is asserted,
addr_i does not contain any X values.
rdy_i and addr_i are both inputs to mctrl, and mctrl does not contain any
logic defining rdy_i and addr_i. It is not possible to generate this
assertion solely by analyzing the RTL of mctrl.
Example 2:
EOS -> state == IDLE;
This assertion says that at the end of simulation (EOS), the state must
return to IDLE after all data have been processed. It ensures that the
design does not retain any data by mistake.
RTL analysis can identify FSMs, but the above functional assertion combines
state machine variables (state == IDLE) with additional control conditions
(EOS). Identifying such combinations is not possible without the help of
dynamic analysis.
Example 3:
if (c1)
if (c2)
...
if (c5)
mode = value;
... other ctrl logic here
!(c1 && c2 ... && c5 && mode == 1)
This property captures an important functional coverage hole that is missed
by other code coverage tools. To generate functional properties like this,
a tool with RTL analysis-only will have to enumerate all combinations.
Such a tool will create many, many properties and have very few designer
friends as a result.
Many other types of high quality assertions can be generated by BugScope.
And dynamic analysis in combination with static and formal analysis is the
key to Quality of Results (QoR).
There are other ways (such as PropSYN) to analyze a design based on the RTL
without simulation. They are, in essence, extensions of lint tools and not
assertion synthesis.
- Yunshan Zhu
Atrenta/NextOp San Jose, CA
Join
Index
Next->Item
|
|
