CHAPTER 1 Introduction to SystemVerilog and Assertions
What Is an Assertion?
Benefits of Assertions
Overview of Assertions
How Are Assertions Used?
Assertions in Simulation
Assertions in Formal Tools
Assertions in HDLs
Temporal Languages
Selecting the Right Assertion Language
Evolution of Verilog
Overview: SystemVerilog Assertion Language (SVA)
Immediate Assertions
Concurrent Assertions
Boolean Layer in Concurrent Assertions
Sequences
Properties
Directives
SystemVerilog Scheduling
Scheduling Details
Assertion Evaluation in SystemVerilog
SVA and PSL: A Comparison
Summary
CHAPTER 2 Boolean Expressions & Sequences
Boolean Expressions
Restrictions in Boolean Expressions
Examples of Boolean Expressions
Sampling of Variables in Concurrent Assertions
Sampled Value Functions
$sampled Function
$rose Function
$fell Function
$stable Function
$past Function
Other Useful System Functions
$onehot Function
$onehot0 Function
$isunknown Function
$countones Function
$isunbounded Function
Sequences
Overview
Defining a Sequence
Defining Temporal Expressions
Examples of Sequence Declaration
Sequences: Attempts and Matches
Sequences as Concatenations of Boolean Expressions
Non-Branching (Simple) Concatenation
Overlapping Concatenation
Branching Sequences
Concatenation with Unbounded Ranges
Extending Sequences
Sequences as Concatenations of Sequences
Simple Sequence Concatenation
Overlapping Sequence Concatenation
Concatenation Using Range Delays
Concatenating Branching Sequences
Unbounded Sequence Concatenation
Formal Arguments in Sequences
Substitution of Identifiers
Substitution of Event Control Expressions
Substitution of Upper Values of a Range with “$”
Local Variables in Sequences
Declaring Local Variables
Assigning Values to Local Variables
Substitution of Local Variables
Scope
Local Variables in Non-Branching Sequences
Local Variables in Branching Sequences
Repetitions
Consecutive Repetition
Repetitions with Gaps between Iterations
Empty Repetitions with Gaps between Iterations
Repetition of Bounded Ranges
Repetition of Unbounded Ranges
Using Repetitions to Express an Until Condition
Summary
CHAPTER 3 Sequence Operations
Sequences
Sequence Operations
Operator Precedence
The or Operator
An “or” of Non-Branching Sequences
An “or” of Branching Sequences
An “or” Operation Concatenated with a Sequence
An “or” of Boolean Expressions
The and Operator
An “and” of Non-Branching Sequences
An “and” of Branching Sequences
An “and” Operation Concatenated with a Sequence
An “and” of Boolean Expressions
The intersect Operator
An intersect of Non-Branching Sequences
An intersect of Branching Sequences
The within Operator
The intersect Form of within
The within Operation Using Non-Branching Sequences
within Operations Using Branching Sequences
Empty Sequences in within Operations
The throughout Operator
The intersect Form of throughout
The throughout Operation with a Non-Branching Sequence
The throughout Operation With a Branching Sequence
The first_match Operator
Multiple Matches at the Same Cycle
Passing Local Variables
Built-In Sequence Methods
The .ended Method
The .triggered Method
The .matched Function
Flow of Local Variables
Local Variable Flow with .ended
Flow of Local Variables in Sequences Using “or”, “an
and “intersect”
Local Variable Flow in “and” and “intersect” Operations
Summary: Sequence Operations
Summary of Rules for an “or” Operation
Summary of Rules for an “and” Operation
Summary of Rules for an “intersect” Operation
Summary of Rules for a “within” Operation
Summary of Rules for a “throughout” Operation
Summary of Rules for “first_match” Operation
Summary of Rules for the .ended Method
Summary of Rules for the .triggered Method
Summary of Rules for Local Variables
CHAPTER 4 Properties
Declaration of Properties
Behavior of Properties
Property Matches: Implicit First Match
Property Failures
Property Operators and Constructs
Negation Operator “not”
Disjunction Operator “or”
Conjunction Operator “and”
Implications and Implication Operators
The “disable iff” Construct
Operator Precedence
Mixing Sequences and Properties
Definitions of Sequence and Property Expressions
Rules for Mixing Sequence and Property Expressions
Example: Legal Property Declaration
Examples: Illegal Property Declaration
Multiclocked Sequences and Properties
Sequence Delay and Concatenation Operator ##1
Implication Operators |=>, |–>, and if..else
Logical Property Operators “and” and “or”
Sequence End Detection
Recursive Properties
Examples of Recursive Properties
Recursion Limitations
Properties vsSequences
Summary
CHAPTER 5 Assertion Directives
assert property Directive: Concurrent Assertion
Syntax
Examples of Concurrent Assertions
Action Block Utility Functions
Execution Rules
assert Directive: Immediate Assertion
Syntax
Examples of Immediate Assertions
Execution of Immediate Assertions
cover property Directive: Concurrent Coverage Collection
Syntax
Cover Examples
Coverage Binning
Using Coverage Data
assume property Directive: Concurrent Assumption
Usage Overview
Syntax
Assume Examples
Assumed Distributions
Clock Flow and Clock Inference
Clock Flow
Clock Inference
Enabling Condition Inference
Summary
CHAPTER 6 Common Assertion Problems and Examples
Applying SVA to Common Assertion Problems
Intersignal Dependencies
Infinite Pattern after Reset
No Consecutive Transaction IDs
Bounding an Unbounded Property
Signal Assertion Length
Signal Assertion Windows
Applying SVA to Design Examples
Counter Example
FIFO Example
Summary
Common Problems
Counter: Immediate Assertions
Counter: Concurrent Assertions
Counter: Coverage
FIFO: Immediate Assertions
FIFO: Concurrent Assertions
FIFO: Coverage
CHAPTER 7 Assertions: Practice and Methodology
General Assertion Practices
Where to Add Assertions
Who Writes Assertions?
Verifying and Debugging Assertions
Enabling & Disabling Assertions
The Performance Impact of Assertions
Re-use of Assertions
Re-use between Simulation and Formal Verification
Re-use of Checkers for Common Design Behaviors
Re-use of Sequences and Properties
Tracking Coverage with Assertions
Where to Add Coverage Assertions
Determining the Sufficient Number of Assertions
Summary
SVA Implementation Guidelines
General Assertion Guidelines
General SVA Guidelines
Naming Conventions
SVA Coding Guidelines
Using SVA with Other Languages
Using SVA with Verilog 2001 and SystemVerilog
SVA Interface to Vera
FIFO Testbench Example
Conclusion
CHAPTER 8 Assertion-Based Verification of an OCP Cache
OCP Cache Overview
Supported Transactions
Limitations
OCP Overview
OCP Data Transfers
The Idle Phase
The Request Phase
The Response Phase
The Write Data Phase
OCP Cache Implementation
Transaction Flow
Block Descriptions
Identifying Assertions
Interface Assertions
Interface Coverage Assertions
Implementation Assertions
Implementation Coverage Assertions
Assertion Code
Interface Assertions
Interface Coverage Assertions
Implementation-Specific Assertions
Summary
CHAPTER 9 A Model Checking Primer
Overview
Constraints
Exhaustivity of Formal Proof
Model Checking versus Equivalence Checking
Searching the State Space
Ideal versus Realistic Results—The State Space Explosion Problem
Formal Verification Uses
Coexistence with Simulation
Usage
Assertions
Constraints
Models
Model Checking Engines
State Space Reduction Techniques
SVA Coding Guidelines
Examples
The FIFO DUT
Assertions for the FIFO
Summary
