( ESNUG 514 Item 2 ) -------------------------------------------- [11/16/12]
Subject: Hey! That NextOp guy didn't cover Avery's PropSYN bughunter tool!!
> 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.
>
> - Yunshan Zhu of NextOp/Atrenta
> http://www.deepchip.com/items/0513-01.html
From: [ Chris Browy of Avery Design ]
Hi John,
That Atrenta Nextop guy forgot to mention Avery's PropSYN tool for assertion
and coverage property synthesis.
We're different from Nextop BugScope on a couple of key fronts even though
we both automatically generate properties used primarily in logic simulation
to detect design bugs -- or to find coverage holes in testbenches.
Our PropSYN operates only on your Verilog/VHDL RTL code and extracts the HW
architecture of the block or chip as a set of interacting hardware functions
and their attributes. It's formal symbolic matching algorithms infer how
your Verilog/VHDL RTL maps to distinct hardware elements like:
- FSM (state register, control inputs and outputs, #states)
- Counter (register, load conditions, load value sources)
- Arbiter (request, grant)
- Simple 2 FSM (request/grant handshake)
- FIFO (push and pop conditions, fifo memory)
- Memory (memory, read and write conditions, size, #words)
- Register (register, load conditions, clock, clockedge)
- Sequential UDPs (UDP output, load conditions)
- Arithmetic operators (+, -, *, /)
- Clocks (internal/external clock sources, clock domain crossing paths)
- Tristate (drive enables, sources)
- IOs (inputs, outputs)
The initial report PropSyn generates is the mircoarchitecture summary of your
block or chip:
#-----------------------------------
# Micro-architecture Summary Report
# Top-level Modules: i_dut
# Generated on: June 18 19:59 2012
#-----------------------------------
# Feature #
# ---------------------- --------
# FSM 8
# counter 149
# arbiter 0
# FIFO 0
# memory 84
# large fanouts 0
# -----------------------------------
# Coerce FIFOs 30
# Coerce Arbiters 2
# Custom Instances 30
# -----------------------------------
Next we generate correct-by-construction properties and covergroups for
single or multiple interacting hardware functions based on the user's
preference of what assertions and coverage they want generated.
For example PropSYN supports several types of FIFOs:
- Simple FIFO (wr_ptr, rd_ptr increment by 1)
- Relaxed FIFO (wr_ptr, rd_ptr increment by variable amount)
- Multi-output shift FIFO
- Priority encoded FIFO
and handles complex Verilog/VHDL RTL modeling styles including the use of
hierarchy, nested "if" and "case" statements. Non-standard FIFOs might be
recognized initially as just memories, but can be coerced by the user into
being handled as one of the FIFO types.
Each HW function has a set of built-in assertions and coverage monitors
that it supports. For example, FIFO supports:
Assertions:
- Overflow
- Underflow
- Simultaneous push/pop
- FIFO output X
- FIFO data leak check where FIFO is popped but data is
not clocked into downstream register
Coverage:
- Fullness histogram covergroup
- Almost Full and Empty cover properties
- # passthroughs covergroup
- # of cycles between push/pop operations covergroup
Other examples of interesting assertions include:
- CDC source data hold time check (supports dynamic
clock frequencies and clock muxing)
Some examples of covergroups include:
- Covergroup for the exclusive write enable conditions
to a memory
- Arbiter request/grant time histogram
- Decomposed FSM state transition condition covergroup
- Expanded read/write conditions covergroup for all
on-set combinations
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.
We also like using covergroups because they present a very concise view of
the design operation and can be read into the verification manager tools for
Synopsys VCS, Cadence NC-Sim, and Mentor Questa which can alert you of low
coverage during simulation.
Verification managers have told us that improving coverage metrics for their
design is extremely important to assessing verification quality.
---- ---- ---- ---- ---- ---- ----
We can also be compared to code coverage tools -- but instead of presenting
generic line, condition, and FSM transition coverage, we derive intuitive
coverage metrics on the hardware elements (microarchitecture abstraction)
and their control functions. (After all isn't this how engineers think
about their design in the first place?)
---- ---- ---- ---- ---- ---- ----
We also differ from BugScope because we support manual/guided flows allowing
users to apply their own property and covergroup templates to our built-in
property generation -- or create their own Tcl script-based design queries
to create their own customized properties. Examples are:
- the user can query the read condition of a FIFO, the transition
condition of a FSM, combine them, and generate a property or
covergroup.
- the user can get the sequential fanin/fanout of any pin or variable.
- the user can query FSM control output variables and put a covergroup
on ones with large fanout. For example, the Tcl script for this:
# Get FSM objects
set fsms [insight_get_objects -type fsm]
# Loop over FSMs...
foreach fsm $fsms {
# Get the FSM control sequential fanout to identify
# all control registers
set fsm_outputs [insight_psyn_get_fanout $fsm -control -seq]
# Loop over control registers to get high fanout ones
foreach fsm_output $fsm_outputs {
set fsm_output_l [insight_psyn_get_fanout $fsm_output -seq]
if {[llength $fsm_output_l] > $fanout_threshold} {
# add a variable covergroup to variable using parameter
# or enumerated values for cover bins
insight_psyn_property_gen $fsm_output -var_covergroup
}
}
}
Other Avery PropSYN features that Atrenta NextOp BugScope does not support:
- I/O connectivity property generation and formal proof. (Yes,
PropSYN also does the proving because it has a formal engine.)
- Ranks control constructs in your Verilog/VHDL RTL for how
easy or hard they are to hit.
- Finds hard-to-cover logic BEFORE you start developing your tests.
So to sum it up:
1) Using Avery PropSYN is more straightforward and the ROI is clear
since manual effort is small and the tool's output provides
positive value (without needing you to filter out "don't care"
conditions like in NextOp BugScope.)
2) PropSYN QOR is good since we base properties and covergroups
on extracted hardware architecture, not a NextOp style waveform
snapshot of how the design was exercised.
3) PropSYN incremental properties and covergroups are highlighted
from run to run to figure out quickly what's new or removed.
4) PropSYN automates generating the properties and covergroups
best suited to designers to write; but who typically don't.
Either way the payback would be to inevitably find more
design bugs and coverage holes.
Avery PropSYN is a tool used in current HW design and verification. And it
has paying customers.
- Chris Browy
Avery Design Andover, MA
Join
Index
Next->Item
|
|
