Part 4 · Assertions (SVA) · Intermediate
Evaluation Attempts & Threads
A new attempt starts every clock tick; nondeterministic sequences spawn threads; each attempt passes or fails independently — and why this drives vacuity and performance.
An attempt every tick
A concurrent assertion is not a single watcher that arms once. At every clock tick , a brand-new evaluation attempt of the property begins, completely independent of attempts started at earlier ticks. Attempts overlap freely: while the attempt from T1 is still waiting for its ack, the attempts from T2, T3, T4 are each running their own evaluation. Each attempt individually ends in pass (possibly vacuous) or fail. This is what makes assertions catch back-to-back protocol traffic that a single hand-coded watcher would miss while busy.
OVERLAPPING ATTEMPTS — ap: assert property (@(posedge clk) req |-> ##2 ack)
clk : T0 T1 T2 T3 T4 T5 T6
req : 0 1 1 0 0 0 0
ack : 0 0 0 1 1 0 0
attempt@T0: req=0 → vacuous pass ✓ (antecedent false, done instantly)
attempt@T1: req=1 → wait ##2 ──────► T3: ack=1 → PASS ✓
attempt@T2: req=1 → wait ##2 ────────────► T4: ack=1 → PASS ✓
attempt@T3: req=0 → vacuous pass ✓
attempt@T4: req=0 → vacuous pass ✓
...
Two requests in flight simultaneously, each tracked by its own
attempt. A single hand-rolled "wait for ack" watcher would have
missed the second req entirely.Why this design? Because protocol rules are universally quantified over time : "EVERY request gets an ack in 2" — not "the first one does". Starting an attempt at every tick is the executable form of "every". It also explains assertion cost: an always-true antecedent on a 2 GHz-of-sim-cycles regression means millions of live attempts.
Threads within an attempt
Inside one attempt, nondeterministic sequence constructs spawn multiple evaluation threads . A windowed delay ##[1:3] ack effectively forks three threads — ack at +1, at +2, at +3. Repetition ranges, or, and goto/nonconsecutive repetition do the same. For an assert directive, the attempt PASSES if at least one thread completes the match (and FAILS only when every thread has died without matching). Threads are bookkeeping inside the attempt — but they are real memory and real simulation work.
THREAD SPAWNING — one attempt of: req |-> ##[1:3] ack
attempt@T1 (req sampled 1):
┌─ thread A: expect ack @ T2 ✗ dies (ack=0)
fork ──────┼─ thread B: expect ack @ T3 ✓ MATCH → attempt PASSES
└─ thread C: expect ack @ T4 (cancelled — already passed)
clk : T1 T2 T3 T4
ack : 0 0 1 -
FAIL case (ack never comes):
┌─ thread A: @T2 ✗
fork ──────┼─ thread B: @T3 ✗
└─ thread C: @T4 ✗ ← LAST thread dies → attempt FAILS,
reported at T4 (not T1!)
Failure is reported when the LAST hope dies — windowed assertions
report at the END of the window, not where the cause was.// Constructs that spawn threads inside an attempt:
ap_win : assert property (@(posedge clk) req |-> ##[1:3] ack); // 3 threads
ap_unbnd : assert property (@(posedge clk) req |-> ##[1:$] ack); // unbounded!
ap_or : assert property (@(posedge clk) start |-> (fast_done or
##[2:5] slow_done));
ap_rep : assert property (@(posedge clk) go |-> busy [*2:4] ##1 done);Pass, fail, and vacuity per attempt
Every attempt terminates in exactly one of three ways: non-vacuous pass (antecedent matched and consequent held), vacuous pass (antecedent never matched — the implication is trivially true and nothing was actually checked), or fail . Simulators count these separately. The vacuous bucket is the dangerous one: an assertion with a never-true antecedent reports 100% passing attempts while checking nothing — full treatment in the Implication topic, but the attempt model is where the concept lives.
ATTEMPT OUTCOME ACCOUNTING — typical simulator report
ap_req_ack: attempts: 100000
real passes: 142 ← antecedent fired, consequent held
vacuous passes: 99858 ← antecedent false; NOTHING checked
failures: 0
Healthy: real passes > 0 (the check actually engaged)
Red flag: real passes == 0 → assertion is dead weight; antecedent
unreachable, signals miswired, or stimulus never exercises it.
This is why "assertion passed" alone proves nothing — always check
the non-vacuous count (or pair every assert with a cover).// Standard hygiene: pair the assert with a cover of the antecedent
ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
req |-> ##[1:3] ack) else $error("ack window missed");
// If this cover never hits, ap_req_ack only ever passed vacuously
cp_req_seen: cover property (@(posedge clk) disable iff (!rst_n) req);Performance: why attempt count is your simulation bill
Total cost ≈ (attempts per tick) × (average threads per attempt) × (average attempt lifetime in cycles).
Unbounded windows (##[1:$], s_eventually) keep threads alive until match or end of sim — the classic assertion memory leak; prefer bounded windows from the spec.
A specific antecedent (req && !busy rather than 1'b1) kills most attempts at birth as cheap vacuous passes — antecedent specificity is the main performance lever.
first_match() and goto repetition ([->1]) prune redundant threads in long windows.
If a regression slows dramatically after adding assertions, profile attempts: one unbounded property on a hot clock usually dominates.
ATTEMPT LIFETIME PICTURE — bounded vs unbounded
bounded req |-> ##[1:3] ack unbounded req |-> ##[1:$] ack
attempt lives ≤ 4 ticks attempt lives until ack... or forever
tick: T1 T2 T3 T4 T5 ... tick: T1 T2 T3 T4 T5 ... T1000000
A@T1 ●──────● A@T1 ●────────────────────────►
A@T2 ●──────● A@T2 ●─────────────────────►
A@T3 ●──────● A@T3 ●──────────────────►
(bounded cleanup) (threads accumulate if ack stalls)Interview angle
"How often does a concurrent assertion evaluate?" — the expected answer is the attempt model: a new independent attempt every clock tick, overlapping attempts for pipelined traffic, threads forked by nondeterministic windows, pass/fail decided per attempt. Drawing the overlapping-attempts diagram on a whiteboard is a strong move; it shows you think in the semantics, not the syntax.
Trap question: "req at T1 and T2, ack only at T3 — does req |-> ##2 ack pass?" — attempt@T1 needs ack at T3 (pass), attempt@T2 needs ack at T4 (fail unless ack repeats). Tests whether you know attempts are independent.
Trap question: "Where is the failure of req |-> ##[1:10] ack reported?" — at the end of the window (when the last thread dies), 10 cycles after the req that caused it. Knowing this saves real debug time.
Follow-up: "Your assertion never failed in a year of regressions — is the design proven?" — check non-vacuous pass count; if zero, the assertion never engaged.
Performance follow-up: "An assertion slowed the regression 3x — first suspects?" — unbounded windows and weak antecedents creating long-lived threads on every tick.
Key takeaways
A new attempt starts at every clock tick — "every request" is implemented as "an attempt per tick".
Attempts are independent and overlap; windowed/or/repetition constructs fork threads within an attempt.
An assert attempt passes if any thread matches; it fails only when the last thread dies — failures report at window end.
Vacuous passes check nothing; track non-vacuous counts or pair asserts with covers.
Attempt count × thread count × lifetime = assertion cost; bound your windows and sharpen your antecedents.
Common pitfalls
Mentally modeling an assertion as one watcher that re-arms after each match — misses overlapped traffic semantics entirely.
Hunting for the bug at the failure-report time of a windowed assertion — the cause is at the attempt START, up to a full window earlier.
##[1:$] everywhere "to be safe" — unbounded threads, memory growth, and failures that never report until end of sim.
Reading "0 failures" as "checked and correct" without confirming non-vacuous passes exist.
Antecedent of 1'b1 (or omitting implication) on hot clocks — every tick runs the full consequent machinery.