Q&A: SVA Quick-Fire

How to use this page

The SVA rapid-fire round: each question expects a one-breath answer plus a one-line property. Sequence/property depth, local variables, and assertion architecture live in the dedicated Part 4 SVA modules — this page is the day-before-interview sweep.

Q: |-> versus |=> — what exactly is the difference?

|-> is overlapping : the consequent starts evaluating in the same cycle the antecedent completes. |=> is non-overlapping : the consequent starts one cycle later — exactly equivalent to |-> ##1.

// grant must be high IN THE SAME CYCLE req completes
a_same:  assert property (@(posedge clk) req |-> gnt);

// grant must be high THE CYCLE AFTER req
a_next:  assert property (@(posedge clk) req |=> gnt);
// identical:            req |-> ##1 gnt

Follow-up: "Which fits a registered (flopped) response?" — |=>, because a flopped output cannot respond in the same cycle as its cause. Using |-> on registered logic produces a failure on correct RTL.

Junior vs senior: juniors know same-cycle vs next-cycle. Seniors map the choice onto combinational vs registered DUT paths.

Q: What is a vacuous pass, and why is it dangerous?

An implication passes vacuously whenever the antecedent never matches — the consequent is never even checked. A property guarding behavior after req is 100% green in a test where req never fires. The assertion reports pass; it verified nothing.

a_gnt: assert property (@(posedge clk) req |-> ##[1:3] gnt);
// test never asserts req → a_gnt passes every cycle, vacuously

// defense 1: cover the antecedent — proves it actually happened
c_req: cover property (@(posedge clk) req);

// defense 2: simulator vacuity reporting (e.g. report non-vacuous pass counts)

Follow-up: "How do you systematically find vacuous assertions in a regression?" — Pair every assert with a cover on its antecedent and review zero-hit covers at closure; most simulators can also report assertions that only ever passed vacuously.

Junior vs senior: juniors define vacuity. Seniors ship the defense: cover-the-antecedent as a standing rule, audited during coverage closure.

Q: [->N] versus [=N] — goto versus non-consecutive repetition?

b [->3] (goto) matches at the cycle of the 3rd occurrence of b — the match point lands exactly on the last b. b [=3] (non-consecutive) matches 3 occurrences possibly followed by more non-b cycles — the match point can float after the 3rd b. Consequence: use goto when the next operator must align to the last occurrence.

// "after the 3rd beat, done next cycle" — alignment matters → goto
a_burst: assert property (@(posedge clk)
  start |-> (beat [->3]) ##1 done);

// b[=3] would allow:  beat,beat,beat, idle, idle, THEN ##1 done
// (the ##1 anchors to a floating endpoint — almost never what you meant)

Follow-up: "And b[*3]?" — Consecutive repetition: exactly 3 b's in 3 back-to-back cycles, no gaps. The trio: [*] consecutive, [->] last-occurrence-anchored with gaps allowed, [=] occurrences-counted with a floating tail.

Junior vs senior: juniors recite definitions. Seniors answer with where the match point lands — the only thing that matters when you chain ##1 after it.

Q: What does $past do, and what are its gotchas?

$past(sig, N) returns the sampled value of sig from N clock ticks earlier (default 1), using the assertion's own clock. Gotchas: in the first N cycles of simulation it returns the type's default (X for logic) — gate with a startup condition or disable iff; and an optional gating expression makes it count only enabled ticks.

// data must hold while valid && !ready (a stability check)
a_stable: assert property (@(posedge clk) disable iff (!rst_n)
  (valid && !ready) ##1 valid |-> data == $past(data));

// gated form: value 2 ENABLED ticks ago
// $past(data, 2, en)  — only ticks where en==1 count

Follow-up: "Why might data == $past(data) fail at time zero even on good RTL?" — $past has no history yet and returns X; X == anything is not 1'b1, so the check fails. The disable iff (!rst_n) covering the start typically absorbs it — otherwise add a first-cycles guard.

Junior vs senior: juniors know it reads the past. Seniors volunteer the no-history X behavior and the gated third argument.

Q: What does disable iff do — and what does it NOT do?

disable iff (expr) — typically disable iff (!rst_n) — aborts any in-flight evaluation attempt and suppresses new failures while the expression is true: reset-time protocol violations stop generating noise. What it does not do: it is asynchronous (evaluated on the fly, not sampled), it discards attempts rather than passing them, and it must not be abused to mute real failure windows — disabling on a busy flag, say, hides bugs.

property p_handshake;
  @(posedge clk) disable iff (!rst_n)
    req |-> ##[1:4] ack;
endproperty
a_hs: assert property (p_handshake);
// reset mid-evaluation → attempt silently discarded (not failed, not passed)

Follow-up: "Difference between disable iff (!rst_n) and adding rst_n to the antecedent?" — The antecedent guard checks reset only at the start of an attempt; an attempt already running when reset lands still completes (and fails falsely). disable iff kills in-flight attempts asynchronously.

Junior vs senior: juniors use it as boilerplate. Seniors articulate aborts-in-flight vs guards-at-start, and the it-discards-not-passes subtlety.

Q: When exactly do concurrent assertions sample their signals?

In the Preponed region — the values signals held just before the clock edge, the same values a flip-flop would capture. This is why an assertion can fail on a cycle where waveform cursors show the "correct" post-edge value: the waveform displays the updated value, but the assertion sampled the pre-edge one.

ASSERTION SAMPLING vs WAVEFORM CONFUSION

  time step N:    Preponed ──► Active/NBA ──► ... ──► Postponed
                     │              │
                     │              └─ clocked logic updates sig 0→1
                     └─ assertion samples sig = 0  (pre-edge value)

  waveform at the edge shows: 1   (post-update)
  assertion evaluated with:   0   (Preponed sample)
  → "the assertion is wrong!" ... no, it sampled like a flop does

  same rule as clocking block input #1step — pre-edge by design

Follow-up: "A signal changed by blocking assignment at the edge — what does the assertion see?" — Still the Preponed value. No same-step update, blocking or nonblocking, is visible to that step's assertion evaluation.

Junior vs senior: juniors say "on the clock edge." Seniors say Preponed, explain the waveform-vs-assertion mismatch it causes, and connect it to #1step sampling.

Key takeaways

• |-> same cycle, |=> next cycle (≡ |-> ##1); registered responses want |=>.

• Vacuous passes verify nothing — cover every antecedent as a standing rule.

• [*] consecutive, [->] anchored to the last occurrence, [=] floating tail — answer in match points.

• $past returns X before history exists; disable iff aborts in-flight attempts asynchronously.

• Assertions sample in Preponed — pre-edge values, exactly like a flop.

Common pitfalls

• |-> on flopped responses — fails correct RTL by demanding same-cycle reaction.

• Green assertion dashboards full of vacuous passes — audit non-vacuous counts.

• ##1 chained after [=N] — anchors to a floating endpoint, almost never intended.

• Debugging assertion failures from post-edge waveform values — check Preponed samples.