You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Status of every lesson and a roadmap of what still needs to be written.
Lessons are keyed by slug (matches src/lessons/index.js). Reference material
from https://github.com/karimmahmoud22/SystemVerilog-For-Verification (KM repo)
and SystemVerilog Assertions and Functional Coverage by Ashok B. Mehta,
3rd ed. (Springer, 2020) — cited as Mehta §N throughout — are noted
where they are directly usable as a basis for a lesson.
Scores are out of 27 (9 dimensions × 3 max). See RUBRIC.md for the rubric.
Flag numbers identify the weak dimension(s): 1=Concept Focus, 2=Starter Calibration,
3=Description Quality, 4=Progression, 5=Dual Coding, 6=Solution Idiom,
7=Concept Importance, 8=Lesson Novelty, 9=Visual Novelty.
assign, bit/reduction/ternary operators, signed arithmetic, overflow
Cover reduction operators (|req), ternary, signed arithmetic,
overflow — sets up concepts used in SVA and UVM lessons.
Ref: TipsAndTricks/ExpressionWidth.sv, TipsAndTricks/Casting.sv
throughout, signal stability constraint over sequence duration
sva/sequence-ops
Sequence Composition: intersect, within, and, or
✅
24/27 ⚠️4,5
sva/throughout
intersect, within, and, or — sequence algebra
sva/seq-args
Sequence Formal Arguments
✅
25/27 ⚠️5
sva/sequence-ops
typed formal arguments in named sequences, reusable parameterised patterns
Chapter: Sampled Value Functions
Slug
Title
Status
Score
Prereqs
Teaches
sva/stable-past
$stable and $past
✅
22/27 ⚠️3,4,5,9
sva/concurrent-sim
$stable(), $past(n), sampled-value semantics
sva/changed
$changed and $sampled
✅
22/27 ⚠️3,4,5,9
sva/stable-past
$changed(), $sampled()
Chapter: Protocols & Coverage
Slug
Title
Status
Score
Prereqs
Teaches
sva/disable-iff
disable iff — Reset Handling
✅
22/27 ⚠️2,4,5,9
sva/implication
disable iff, async reset gating of properties
sva/abort
Aborting Properties: reject_on and accept_on
✅
23/27 ⚠️4,5,9
sva/disable-iff
reject_on, accept_on, mid-sequence abort
sva/cover-property
cover property
✅
23/27 ⚠️4,5,9
sva/sequence-basics
cover property, reachability vs correctness, cover vs assert intent
Chapter: Advanced Properties
Slug
Title
Status
Score
Prereqs
Teaches
sva/local-vars
Local Variables in Sequences
✅
24/27 ⚠️5,9
sva/clock-delay
local var, data capture across sequence steps
sva/onehot
$onehot, $onehot0, $countones
✅
24/27 ⚠️5,9
sva/concurrent-sim
$onehot(), $onehot0(), $countones() — bit-count system functions
sva/triggered
.triggered — Sequence Endpoint Detection
✅
23/27 ⚠️5,7,9
sva/sequence-basics
.triggered, detecting sequence completion at a named endpoint
sva/checker
The checker Construct
✅
23/27 ⚠️5,6,7
sva/implication, sva/disable-iff
checker construct, encapsulating assertions into reusable modules
sva/recursive
Recursive Properties
✅
23/27 ⚠️5,6,7
sva/implication
recursive property, inductive-style reasoning
sva/bind
bind — Non-Invasive Assertion Attachment
📝
—
sva/checker
bind statement, attaching checkers without modifying RTL source
sva/let
let Declarations
💡
—
sva/sequence-basics
let declaration, scoped parameterisable macro alternative to `define
sva/bind (Mehta §6.12-6.14, p. 79-82)
bind target_module checker_or_module inst_name (port_connections);
attaches assertion logic to any module without touching its source.
Exercise: bind a property checker to the existing counter module
from Part 1.
sva/let (Mehta §21, p. 325-333)
let name [(ports)] = expression; — scoped, parameterisable macro
alternative to `define without text-substitution pitfalls.
Chapter: Formal Verification
Slug
Title
Status
Score
Prereqs
Teaches
sva/formal-assume
assume property
✅
25/27 ⚠️4,9
sva/formal-intro
assume property, constraining formal input space
sva/always-eventually
always and s_eventually
✅
22/27 ⚠️4,5,7,9
sva/formal-assume
always/s_eventually, liveness vs safety properties
seq #-# prop and seq #=# prop fail if the antecedent doesn't
match — unlike |-> / |=> which pass vacuously.
Exercise: compare the two forms on a burst read; observe the #=#
failure when the burst never occurs vs the |=> silent pass.
Requires circt-bmc for the formal comparison half.