Part 4 · Assertions (SVA) · Intermediate
SVA Anti-Patterns Review
The seven interviewer-bait mistakes: implication off-by-ones, retrigger storms, missing disable iff, weak liveness, [=N] misuse, missing first_match, ungated $past — broken code, failing trace, and fix for each.
Anti-pattern 1 — |-> vs |=> off-by-one
The single most-tested SVA fact: |-> checks the consequent in the SAME cycle the antecedent completes; |=> checks one cycle later. Every delay you stack shifts on top of that choice.
// SPEC: 'ack two cycles after req rise'
// BROKEN — checks cycle T+3:
a_bad: assert property (@(posedge clk) $rose(req) |=> ##2 ack);
// FIX — |-> ##2, or |=> ##1; pick ONE place to count from:
a_fix: assert property (@(posedge clk) $rose(req) |-> ##2 ack);cycle : 0 1 2 3 4
req : 0 1 0 0 0
ack : 0 0 0 1 0 ← correct DUT: ack at T+2 = cycle 3
a_bad checks cycle 1+1+2 = 4: ack low → FALSE FAILURE on a
correct design. Off-by-ones usually fail GOOD designs — that is
how you spot them in triage.Anti-pattern 2 — level antecedent retrigger storm
// SPEC: 'when req is asserted, ack within 4'
// BROKEN — one attempt per high cycle:
a_bad: assert property (
@(posedge clk) disable iff (!rst_n) req |-> ##[1:4] ack);
// FIX — arm once per request:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n) $rose(req) |-> ##[1:4] ack);cycle : 0 1 2 3 4 5 6
req : 0 1 1 1 1 0 0 ← req held until ack
ack : 0 0 0 0 1 0 0
a_bad attempts: @1 ✓(ack@4) @2 ✓ @3 ✓ @4 needs ack in 5..8 → ✗
The attempt from cycle 4 FAILS even though the handshake was
perfect. Storm signature: N-1 passes + spurious fail per txn,
and attempt counts in the tool exploding with traffic.Level antecedents are correct only when every high cycle genuinely restates the obligation (e.g. valid |-> !$isunknown(data)). For events, always edge-qualify.
Anti-pattern 3 — missing disable iff
// BROKEN — no reset clause on a functional check:
a_bad: assert property (
@(posedge clk) $rose(req) |-> ##[1:4] ack);
// FIX:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n) $rose(req) |-> ##[1:4] ack);cycle : 0 1 2 3 4 5 6
rst_n : 1 1 0 0 1 1 1 ← mid-sim reset
req : 0 1 0 0 0 0 0
ack : 0 0 0 0 0 0 0 ← reset wiped the txn — legal!
a_bad: attempt from cycle 1 survives INTO reset, window 2..5
empty → FAILS at 5 on a perfectly legal abort. Multiply by every
transaction in flight at every reset event = noise that buries
real failures. FIX kills in-flight attempts the moment rst_n drops.
Remember the inversion: functional checks NEED disable iff;
reset-value checks must NOT have it (Reset Drill 1).Anti-pattern 4 — unbounded liveness in simulation
// SPEC: 'every request is eventually acknowledged'
// BROKEN in sim — weak, can never fail at finite time:
a_bad: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:$] ack);
// FIX for sim — protocol-derived bound:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:64] ack);
// (true unbounded liveness: s_eventually ack — formal only)cycle : 0 1 2 ........ 999999 (end of sim)
req : 0 1 0 ........ 0
ack : 0 0 0 ........ 0 ← NEVER acknowledged
a_bad: ##[1:$] keeps hoping; at end-of-sim the attempt is merely
'pending' — most tools report it as a pass or a benign note.
A dead handshake sails through regression. a_fix fails crisply
at cycle 65. If you cannot justify a bound, the property belongs
in formal, not in the sim regression.Anti-pattern 5 — [=N] where [->N] is needed
// SPEC: 'done comes EXACTLY one cycle after the 4th beat'
// BROKEN — [=4] lets idle cycles drift in before done:
a_bad: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(go) |=> beat[=4] ##1 done);
// FIX — [->4] ends ON the 4th beat, anchoring done:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(go) |=> beat[->4] ##1 done);BUGGY DUT: done is 3 cycles late
cycle : 0 1 2 3 4 5 6 7 8
go : 0 1 0 0 0 0 0 0 0
beat : 0 0 1 1 1 1 0 0 0 ← 4th beat at cycle 5
done : 0 0 0 0 0 0 0 0 1 ← should be at 6, is at 8
a_bad: beat[=4] happily absorbs idle cycles 6..7 into its match,
##1 done lands at 8 → PASSES. Timing bug invisible.
a_fix: [->4] pins the match end to cycle 5; done demanded at 6,
absent → FAILS at 6. Direction matters: [=N] is for 'closing
event may trail', [->N] is for 'Nth occurrence anchors what follows'.Anti-pattern 6 — missing first_match on a ranged antecedent
// SPEC: 'when start is followed by ready (1..5 later), data
// must be valid in that same cycle... checking from the
// FIRST ready'
// BROKEN — EVERY match of the ranged antecedent must satisfy
// the consequent; later ready cycles spawn obligations too:
a_bad: assert property (
@(posedge clk) disable iff (!rst_n)
(start ##[1:5] ready) |-> data_ok);
// FIX — collapse to the earliest match:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n)
first_match(start ##[1:5] ready) |-> data_ok);cycle : 0 1 2 3 4 5
start : 0 1 0 0 0 0
ready : 0 0 0 1 1 0 ← ready high cycles 3 AND 4
data_ok : 0 0 0 1 0 0 ← DUT presents data with FIRST ready
a_bad: antecedent matches at 3 (✓ data_ok) AND at 4 (✗ data_ok=0)
→ FALSE FAILURE at 4 on a spec-compliant DUT.
a_fix: first_match keeps only the cycle-3 thread → PASS.
Nuance to volunteer: with a ranged antecedent, |-> needs EVERY
match's consequent to hold. Sometimes that IS the spec ('data_ok
whenever ready in the window') — first_match is for when the spec
says 'the first'. Quote the spec, then choose.Anti-pattern 7 — $past without a gate
// SPEC: 'when out_vld, dout equals din from the prior vld beat'
// BROKEN — $past samples the previous CYCLE, vld or not,
// and reads garbage/X in the first cycles after reset:
a_bad: assert property (
@(posedge clk) disable iff (!rst_n)
out_vld |-> (dout == $past(din)));
// FIX — gate $past with the qualifying enable:
a_fix: assert property (
@(posedge clk) disable iff (!rst_n)
out_vld |-> (dout == $past(din, 1, , in_vld)));cycle : 0 1 2 3 4
in_vld : 0 1 0 0 0
din : -- A ZZ ZZ ZZ ← bus floats between beats
out_vld: 0 0 0 1 0
dout : -- -- -- A --
a_bad @3: compares dout(A) with $past(din) = din@2 = ZZ
→ FALSE FAILURE (or X-vacuous nonsense) on a correct DUT.
a_fix @3: $past(...,in_vld) returns din at the last in_vld
beat = A → PASS. Also gate the first evaluation after reset:
$past has no history at cycle 0 — pair with a warm-up term
when reset is short.Triage cheat-sheet — symptom to anti-pattern
Fails a known-good design at txn end ± 1 cycle → implication off-by-one (AP1).
N-1 passes then one fail per transaction, attempt counts explode → level retrigger (AP2).
Failures clustered at reset events → missing disable iff (AP3).
Dead handshake but regression green → weak unbounded liveness (AP4).
Late event accepted silently → [=N] absorbing the slack (AP5).
False fail when the trigger window has multiple matches → missing first_match (AP6).
False fail right after reset or between beats → ungated $past (AP7).
Key takeaways
Most anti-patterns fail GOOD designs (off-by-one, retrigger, no disable, no first_match, ungated $past) — false failures are the symptom to learn.
The other two pass BAD designs (weak liveness, [=N] slack) — these are the dangerous ones, invisible in regression.
Interviewers plant these seven deliberately; naming the anti-pattern by symptom is worth more than a first-try-perfect property.
Common pitfalls
Fixing an off-by-one by trial and error in the tool instead of counting cycles on a drawn trace.
Adding first_match reflexively to every sequence — when the spec demands ALL matches comply, first_match hides bugs.
Bounding liveness with an arbitrary huge number instead of a protocol-derived limit — 'within 100000' checks nothing useful.
Treating a quiet assertion as a correct one — pair every assert with a cover to prove it ever triggered non-vacuously.