SystemVerilog Assertions check protocol rules on every clock edge, at the exact signal that breaks. This part builds from sampling and the four assertion layers to sequences, properties, protocol checkers, and debug.
Topic | Lessons | What it covers | Time | Path |
|---|---|---|---|---|
5 | Sampled values, attempts, layers, reset gating and directives: the base every SVA check stands on. | 40 min | Required | |
4 | Sequences are patterns over clock ticks; delays, repetition, and composition build them on match threads. | 30 min | Required | |
5 | How SVA implication, vacuity, property operators, temporal strength, and antecedent design work. | 40 min | Required | |
4 | Snapshots drive every SVA check: edges, past values, one-hot classes, and data-integrity patterns. | 30 min | Recommended | |
6 | Complete SVA rulesets for handshakes, FIFOs, FSMs and pipelines, plus the PacketFIFO checker, with benches. | 50 min | Recommended | |
4 | Local variables, multiclock checks, expect, checkers and assertion control. | 30 min | Recommended | |
5 | Debug methods for SystemVerilog assertions: failures, vacuity, performance, placement, and review. | 40 min | Recommended | |
8 | Revision: write-the-assertion drills graded on a real simulator, and Q&A with runnable proof. | 65 min | Optional |
Required lessons are the core first pass for writing working assertions. Recommended lessons are worth reading for most learners once the first pass works. Optional lessons are reference, specialist material or revision, and you can come back to them when a project needs them.
Topics marked Recommended still hold Required lessons: Sampled Value Functions for $rose and $stable, Protocol Assertion Cookbook for the valid/ready handshake, and Assertion Debug for reading failures. The path below lists them.
These ten lessons give you a working assertion writer: you can state a protocol rule as a clocked property, predict what it samples, avoid vacuous passes and read a failure report. Read them in this order, then pick the rest by need.
Immediate vs Concurrent Assertions: when a check needs a clock.
Clocks and the Sampling Model: which value an edge sees, and disable iff.
Evaluation Attempts and Threads: one attempt per tick, and what one failure means.
Cycle Delays: ##N and ##[M:N].
Repetition: [*N], [->N] and [=N].
|-> vs |=>: where the consequent starts.
Vacuous Success: pair every assert with a cover.
$rose, $fell, $stable, $changed: edge triggers and hold checks.
Valid/Ready Handshake: your first complete ruleset.
Debugging Assertion Failures: attempt start versus failure time.
Learn now
Sampling, attempts, reset gating and assert with cover.
## delays and repetition, then |-> and |=>.
$rose and $stable for edges and holds.
One protocol checker, and how to read its failure report.
Return to later
Composition (and, or, intersect), first_match and the temporal operators nexttime, always, s_eventually: Verilator 5.048 supports few of them, so the lessons pair them with a bounded form.
$past, counting functions and data-integrity patterns when a design needs them.
FSM and pipeline rulesets, local variables, multiclock, expect and procedural assertions: each lesson names its prerequisites.
Performance, placement and the review checklist before sign-off, and the drills for interview revision.
Every lesson ends with a bench that runs real assertions on Verilator 5.048 (with --assert, and --coverage for covers) and plants a bug the assertion must report. Icarus 13 has no concurrent assertions. Verilator gets single-thread properties right, misses some failures in multi-step sequences, and stops at the first $error, so the benches count failures in action blocks and show the compact form's count beside a form that works. What the Open Simulators Run lists every case.
req |-> ##[1:3] ack pass on a run where ack never pulses?Overlapped implication succeeds vacuously on every cycle where req is low, so a run with no requests passes without checking anything. The Implication and Property Operators topic covers vacuity and how to close the hole.
No. The assertion used the value from just before the edge, so at that edge it saw the old, low value. Sampling is taught in Clocks and the Sampling Model.
req |-> ##[1:3] ack and req |=> ##[1:3] ack differ by one cycle. How, and where is each consequent window?With |-> the window [1:3] counts from the request tick; with |=> it counts from the next tick, so the ack may come one cycle later. |-> vs |=> draws both.
Whether each antecedent ever matched, using a cover paired with each assert. Vacuous Success teaches the pairing.
ready is low.(valid && !ready) |-> ##1 valid and (valid && !ready) |-> ##1 $stable(data), gated by disable iff (!rst_n). The first is in Valid/Ready Handshake and $stable is in $rose, $fell, $stable, $changed.
At the attempt start, the tick where the antecedent matched, not the failure tick. Debugging Assertion Failures explains the two times in every report.