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 |
|---|---|---|---|
5 | Sampled values, attempts, layers, reset gating and directives: the base every SVA check stands on. | 40 min | |
4 | Sequences are patterns over clock ticks; delays, repetition, and composition build them on match threads. | 30 min | |
5 | How SVA implication, vacuity, property operators, temporal strength, and antecedent design work. | 40 min | |
4 | Snapshots drive every SVA check: edges, past values, one-hot classes, and data-integrity patterns. | 30 min | |
5 | Complete SVA rulesets for handshakes, FIFOs, FSMs and pipelines, with checkers and testbenches. | 40 min | |
4 | Local variables, multiclock checks, expect, checkers and assertion control. | 30 min | |
5 | Debug methods for SystemVerilog assertions: failures, vacuity, performance, placement, and review. | 40 min | |
8 | Write-the-assertion drills graded on a real simulator, and Q&A revision with runnable proof. | 65 min |
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.