Assertion Based Verification
(ABV)
1
The Design and Verification Gap
The number of transistors on a chip increases approximately 58% per year,
according to Moore's Law.
The design productivity, facilitated by EDA tool improvements, grows only 21% per
year.
These numbers have held constant for the last two decades.
Assertion Based Verification
2
What is the hardest challenge in design flow?
The main problem in the design flow is to clean on the functional bugs.
Functional Logic Error grow to be 72% at 2002, and 75% at 2004.
Top causes are:
– 12.7% - Goofs (for example, typos)
– 11.4% - Miscommunication.
– 9.3% - Micro Architecture bugs.
– 9.3% - Logic and micro changes.
Assertion Based Verification
3
Agenda
What is verification and coverage driven?
ABV – Assertion Based Verification
– What is assertion
– Examples
Questions
Backup – SystemVerilog assertions
– SystemVerilog overview
– Advantages of SystemVerilog assertions
– Examples
Assertion Based Verification
4
Coverage Driven Verification
How to verify that the design meets the verification goals?
Define all the verification goals up front in terms of "functional coverage points.“
– Each bit of functionality required to be tested in the design is described in terms of
events, values and combinations.
Functional coverage points are coded into the HVL (Hardware Verification
Language) environment (e.g., Specman ‘e’).
– The simulation runs can be measured for the coverage they accomplish.
Focus on tests that will accomplishing the coverage ("coverage driven testing“).
– By Fixing bugs, releasing constraints, and improving the test environment.
– In a coverage-driven project, each verification engineer is focused on achieving the
tangible results for his features.
Assertion Based Verification
5
Common testing schemes
Traditional simulation-based functional verification is good at
validating baseline functionality
Disadvantages :
The specification may not be complete
– usually describes only the normal operating behavior
Hard to set up all specified operations strictly from the chip inputs
Hard to check all specified behavior strictly from the chip outputs
Hard to locate the sources of bugs exhibited at the chip outputs
Certain types of bug behaviors may not propagate all the way to
the chip outputs
Certain types of implementation errors are difficult to detect using
functional tests
Assertion Based Verification
6
Hardware Languages for Design and Verification
Assertion Based Verification
7
Assertions
Assertions capture knowledge about how a design should operate
Assertions are vital to increasing both the observability and the
controllability of a design
Each assertion specifies both legal and illegal behavior of a circuit
structure (which can be an RTL element, an interface, a controller,
etc.) inside the design
Assertion in English:
- The fifo should not overflow
(i.e., when it is full, write should not happen) or
- TDO signal should be less then…
Will be used in coverage-driven verification techniques.
Assertion Based Verification
8
Assertion Based Verification
9
Assertion Based Verification
10
Assertion Based Verification
11
Complete ABV Flow
RTL Design Automatic
RTL Checks
Assertions Assertion
Library Assertion
Compiler
Standard Verilog Coverage
Testbench
Simulation Simulator Reports
Formal Model
Compiler
Formal
Verification
Formal
Static Formal Dynamic Formal Metrics
Verification Verification
Assertion Based Verification
12
Performance of the ABV Flow
% Functional Coverage $/Bug Saving Reduced Risk
Signoff Coverage
Traditional Verification
X Improvement in Verification Closure
bug
(Reduction in total simulation)
Project Timeline (Increasing $/Bug)
Assertion based verification flow provides
– Find bugs faster with assertions
– Find more bugs with verification hot spots
– Reduce simulation cycles
– Adopt the AVB/CDV methodology incrementally
Assertion Based Verification
13
Conclusion
Assertion-based verification is a shift in verification methodology
Traditional functional verification tries to stimulate the design and observe the
responses from the outside
observability and controllability are so low that pseudo-random simulation can
no longer exercise the internals of the device sufficiently
ABV technologies and methodologies are developed to :
– Zero in to the structure of the design
– Responsibility of verification is also shifting from over-the-wall verification team to
involve designers as well
– Design knowledge becomes a critical criterion for successful functional verification
– With assertions, we can detect bugs sooner
– With formal verification, we have more direct control of the verification effort
Assertion Based Verification
14
Thank you for listening !
Assertion Based Verification
15
Backup
SystemVerilog Assertions ( SVA )
16
Four Pillars of ABV
Assertions capture the design intent by embedding them in a
design and having them monitor design activities
Pillar 1: Automatic Assertion Check
Pillar 2: Static Formal Verification
Pillar 3: Simulation with Assertions
Pillar 4: Dynamic Formal Verification
Assertion Based Verification
17
SystemVerilog – assertions overview
Key benefits of SVA can be summarized as follows:
Familiar language and syntax
Less assertion code
Simple hookup between assertions and the test
No special interfaces
Customized messaging and error severity levels
Ability to interact with Verilog and C functions
No mismatch results between simulation and formal tools
Assertion Based Verification
18
SystemVerilog – assertions overview
SystemVerilog provides two types of assertions:
– Immediate
– Concurrent
Both intended to convey the intent of the design and
identify the source of a problem as quickly and directly .
Immediate assertions
Assertion Based Verification
19
Concurrent vs. immediate
Two important differences:
- Concurrent assertions allow the specification of a temporal behavior to
be checked vs. combinational condition of immediate.
- Concurrent assertions can also be instantiated declaratively as a
module-level statement (similar to a continuous assignment).
Concurrent types:
- Boolean expressions
- Sequential expressions
- Property Declarations
- Assertion Directives
Assertion Based Verification
20
Boolean expressions
The Boolean expressions layer is the basic layer.
Boolean expressions specifies the values of elements at a
particular point in time
Syntax :
Assertion Based Verification
21
Sequential expressions
Sequences of Boolean expressions with clear temporal
relationships between them
Basic sequential expression :
"a followed by b on the next clock"
which is represented in SystemVerilog as
a ##1 b
##1 indicates one clock delay
Assertion Based Verification
22
Important to understand that in SystemVerilog each element
of a sequence may be either a
Boolean expression or another sequence.
Thus, the expression
s1 ##1 s2
means that sequence s2 begins on the clock after
sequence s1 ends.
Assertion Based Verification
23
The optional list of arguments allows for specification of sequences
as a generic temporal relationship .
- Some operations on sequences :
Assertion Based Verification
24
Property declarations
More general behaviors to be specified.
Properties allow you to invert the sense of a sequence
- As when the sequence should not happen.
Disable the sequence evaluation.
Specify that a sequence be implied by some other occurrence.
Syntax :
"as long as the test signal is low,
check that the abort_seq sequence does not occur."
Assertion Based Verification
25
Assertions directives ( Procedural )
System implication - "when this happens, then that will happen“
thus require the writer to specify the trigger assertion.
Declarative assertions, require additional work by the designer to use
them effectively.
Consider a finite state machine design.
Assertion
"when in state ACK, if foo is high, then req should be held low for 5 clocks."
Assertion Based Verification
26
State machine cont’
This assertion could be coded declaratively as:
The fact that the assertions are syntactically part of the language
allows them to be embedded procedurally in the RTL code
and automatically infer this information, as in:
Assertion Based Verification
27
Assertion example
Two blocks A,B exchange data via a common bus :
• A and/or B sends ‘Req’ to the Arbiter.
• Arbiter sends ‘Gnt’ back to A or B, making it Master.
• Arbiter sets ‘Busy’ while A or B is Master.
• Master sets ‘DRdy’ when Data is on the bus.
• Master sets ‘Done’ in the last cycle of a grant.
Assertion Based Verification
28
Some Assertions to Check :
A Grant never occurs without a Request.
– Assert never GntA && !ReqA
If A (B) receives a Grant, then B (A) does not.
– Assert always GntA -> !GntB
A (B) never receives a Grant in two successive cycles.
– Assert never GntA && nextGntA
A Request is eventually followed by a Grant
– Assert always ReqA -> eventually GntA
Assertion Based Verification
29
Tool Support
Assertion Based Verification
30
Assertion Debug Environment
Assertion Based Verification
31
Conclusion
SystemVerilog is a unified language that contains design and
verification constructs
Assertions communicate to the test bench and vice-versa.
Customize messaging resulting from the assertions
Create calls to Verilog and C functions dependent on the success
or failure of the assertions
Minimize assertion code by inferring design control structures
Furthermore, SystemVerilog assertions will eliminate the
debugging of mismatches between simulation and formal tools
Assertion Based Verification
32
