System Verilog Assertions (SVA) Language and Methodology Training Class

System Verilog Assertions (SVA) is a powerful subset of the IEEE 1800 System Verilog standard. Its hardware oriented concurrent semantics significantly reduce time to develop complex multi-clock domain checkers. Assertions also provide white box observability resulting in a drastic reduction of debug time, further reducing time to production. SVA allows a clean separation of design and verification logic and parameterization of properties resulting in a modular and reusable methodology.

Location: San Jose, CA
Date: 12/4/2008 - 12/4/2008
Organizer: DefineView Consulting

TRAINING AGENDA:

Introduction to Assertions
What’s an assertion? Why can’t I just use Verilog?
Advantages of Assertion Based Verification (ABV) .
Assertion Based Verification (ABV) Methodology components
System Verilog Assertions :: Syntax and Semantics (with applications)
Immediate assertions
Concurrent assertions - Basics
clocking basics; formal arguments; severity levels; threads
Sequence introduction
Property introduction (with/without an implication)
Vacuous pass?
Binding properties.
Threading (what are the performance implications?)
Sampled value functions (in property/sequence and procedural)
Functions that return boolean pass/fail: $rose, $fell, $stable
Function that return sampled value; $past (with/without gating expr.)
Sequence Operators
##m and ##[m:n] clock delay (SVA allows only fixed delays. So what if you want variable delays??)
[* ] and [*m:n] – Consecutive repetition operator
[= ] and [=m:n] – Non-consecutive repetition operator
[-> ] and [-> m:n] – Goto (non-consecutive) repetition operator
Pros/Cons of infinite ($) range
‘throughout’, ‘within’, ‘intersect’, 'first_match'
'and' and 'or' of sequences with/without delay range
‘intersect’ vs. ‘and’
Property operators
‘not’ operator
If … else
‘disable iff’
Recursive property
Mutually exclusive
0 delay infinite loop
Restrictions
System functions
$onehot, $onehot0, $isunknown, $countones
Multiple Clocks
Multiply clocked sequences and properties – legal and Illegal usage
Multiply clocked properties and ‘and’, ‘or’, ‘not’ operator
Multiply clocked properties – Clock resolutions
Local variables (one of the most powerful features...)
Basics and Visibility rules, legal and illegal usage
Pipelined behavior (threads)
Detecting and using endpoint of a sequence
.ended, .matched
The ‘expect’ statement, 'assume' statement
Embedding concurrent assertions in procedural code
Calling subroutines

LABs
LAB 1: Learn how to 'bind' property module with design module.
Understand vacuous pass and properties with/without implication
LAB 2: Enforces how pipelined threads of a property work.
LAB 3: FIFO
A simple FIFO design is presented. You will code different properties to meet various FIFO fail conditions.
FIFO assertions are some of the most useful assertions to code for any design. This lab teaches how to do that so that you can apply them directly to your design.
More Labs will be conducted, if time permits.

Event Link:http://defineview.com/