1 day training agenda

SystemVerilog Assertions Language and Methodology Training Agenda

(1 Day Class with 6 LABs)

Course Highlights

• Each operator/feature is explained in detail using comprehensive examples, timing diagrams and simulation logs.
• Real life applications are discussed to put it all in perspective.
• A reference grade handout book is provided to the class. It has comprehensive detail on each page that can serve as excellent reference material for future.
• Labs are geared to solidify understanding of key concepts using application oriented designs.

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’

System functions

• $onehot, $onehot0, $isunknown, $countones

Multiple Clocks / Multiply clocked properties and sequences

– Local variables (one of the most powerful features…)

• Pipelined behavior (multiple threads)

– Detecting and using endpoint of a sequence

• .ended, .matched, .triggered

‘expect’, ‘assume’ (for formal verification)

Asynchronous Assertions

2012 features:

• Strong and Weak sequences, ‘followed by’, ‘always’, ‘eventually’, ‘until’, ‘until_with’, ‘nexttime’, ‘case’, inferred clock and disable, ‘accept_on’, ‘reject_on’

‘let’ declaration

‘checker’

SVA 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: Synchronous FIFO

• A synchronous FIFO design is presented. You will write assertions to check for various FIFO fail conditions.
• FIFO assertions are some of the most useful assertions to write for any design. The assertions developed in this LAB will be directly applicable to your design.

LAB 4: Up/Down Counter

• A simple UP/DOWN COUNTER design is presented. Counter assertions deployed directly at the source can greatly reduce the time to debug since these assertions will point to the exact cause of a Counter error without the need for extensive back-tracing debug when design fails.

LAB 5: Generic Bus Interface Protocol

• A simple bus interface is presented. Assertions are written to find bugs on burst mode data and other protocol violations

LAB 6: PCI Read Protocol

• A simple system with a PCI Master and PCI Target modules designed to do a simple basic PCI Read operation. The LAB shows how to derive and write simple but effective assertions for a PCI type bus.