Designing Good Antecedents

The antecedent is the specification

The consequent states the obligation, but the antecedent decides WHEN it applies — and both failure modes of a bad assertion live there. Too narrow (wrong polarity, over-qualified, gated by something the test never enables) and the assertion is vacuous — green and useless. Too loose (level instead of edge, missing qualifier) and it fires obligations the spec never imposed — false failures that erode trust until someone disables the assertion. Precision in the antecedent is what makes an assertion simultaneously meaningful and quiet.

ANTECEDENT FAILURE MODES

  too NARROW                          too LOOSE
  ───────────                         ─────────
  $rose(req && en && !dbg_mode)       req   (level, held 10 cycles)
  └ test never sets en                └ 10 attempts, 10 obligations
    → never matches                     → duplicate/false failures
    → vacuous forever                   → assertion gets waived/off
    "green but asleep"                  "noisy then silenced"

  the target: matches EXACTLY when the spec imposes the obligation

$rose vs level: the retrigger problem

A level antecedent re-matches at every tick it stays true . If req is held high while waiting for gnt — the normal handshake posture — then req |-> ##[1:4] gnt launches a fresh attempt each cycle, each with its own 4-cycle window. The early attempts' windows expire before the legitimately-late grant arrives: false failure, even though the protocol was honored from the REQUEST. $rose(req) anchors the obligation to the request EVENT, giving exactly one attempt per transaction.

WAVEFORM — level retrigger: req held, gnt at tick 6

clk :  1    2    3    4    5    6    7
req :  0    1    1    1    1    1    0
gnt :  0    0    0    0    0    1    0

req |-> ##[1:2] gnt        (LEVEL antecedent)
  attempt@2: window ticks 3-4 → no gnt → FAIL @4   ✗ false fail
  attempt@3: window ticks 4-5 → no gnt → FAIL @5   ✗ false fail
  attempt@4: window ticks 5-6 → gnt @6 → pass
  attempt@5: window ticks 6-7 → gnt @6 → pass
  attempt@6: window ticks 7-8 → ...
  → 5 attempts from ONE transaction, 2 spurious failures

$rose(req) |-> ##[1:5] gnt  (EDGE antecedent)
  attempt@2 only: window ticks 3-7 → gnt @6 → PASS  ✓
  one transaction, one attempt, correct verdict

// WRONG for held-request protocols: level antecedent
a_bad:  assert property (@(posedge clk) disable iff (!rst_n)
          req |-> ##[1:4] gnt);

// RIGHT: edge-anchored, window sized from the request event
a_good: assert property (@(posedge clk) disable iff (!rst_n)
          $rose(req) |-> ##[1:4] gnt);

// When level IS right: a per-cycle invariant, consequent same cycle
a_inv:  assert property (@(posedge clk) disable iff (!rst_n)
          fifo_full |-> !wr_en);   // every full cycle must block writes

Gating with enable/valid and qualifying data checks

Antecedents should encode every qualifier the spec attaches to the obligation — and nothing more. Data-path checks especially: a rule about wdata only applies when wvalid qualifies it, so the qualifier belongs in the antecedent, not AND-ed into the consequent where its absence becomes a failure instead of a non-obligation. Same for enables, modes, and reset: gate where the spec gates.

// Qualifier in the WRONG place — consequent:
a_w1: assert property (@(posedge clk)
        wr_cmd |-> (wvalid && (wdata inside {[0:MAX]})));
// If wvalid is legitimately low, this FAILS — but no data rule
// was violated; there was simply no qualified data.

// Qualifier in the RIGHT place — antecedent:
a_w2: assert property (@(posedge clk)
        (wr_cmd && wvalid) |-> (wdata inside {[0:MAX]}));
// No qualified data → vacuous (correct: no obligation existed).

// Enable-gated protocol rule, edge-anchored:
a_en: assert property (@(posedge clk) disable iff (!rst_n)
        $rose(start) && chan_en |-> ##[1:8] done);

Attempt explosion: the performance angle

Every antecedent match spawns consequent evaluation threads; a loose antecedent multiplied by a ranged consequent is the standard recipe for assertion-dominated simulation. A level antecedent true for L cycles in front of ##[1:N] holds roughly L×N threads live; nest another range and it multiplies again. Symptoms: simulation slows when assertions are enabled, profilers show assertion engine time, memory creeps in long tests. Fixes, in order of preference: edge-anchor the antecedent, shrink ranges to spec-derived bounds, first_match nondeterministic consequents whose extra matches carry no meaning, and only then consider disabling assertions in performance runs.

THREAD COST — level antecedent x ranged consequent

  busy |-> ##[1:16] done       busy high for 100 cycles
  ────────────────────────     ──────────────────────────
  attempts:        100         (one per busy tick)
  threads/attempt:  16         (consequent range)
  peak live:     ~1600 threads ... PER ASSERTION INSTANCE
  x 50 instances (bind to every channel) = ~80,000 threads

  $rose(busy) |-> ##[1:16] done
  attempts: 1 per busy episode → ~16 threads peak. Same check intent.

Interview angle and review checklist

Interview angle

• "req stays high for 5 cycles and gnt comes at cycle 4 — what does req |-> ##[1:2] gnt report?" — multiple attempts, early ones fail: the level-retrigger waveform IS the question. Answer with the attempt table, then fix with $rose.

• "Where do you put the wvalid qualifier in a wdata check?" — antecedent; in the consequent its absence becomes a false failure instead of a non-obligation.

• "An assertion slows simulation 3x — first three things you check?" — level antecedents that retrigger, wide ##[M:N]/[*M:N] ranges, missing first_match on multi-match consequents.

• "Can an antecedent be too precise?" — yes: over-qualified antecedents go vacuous; this is why every antecedent ships with a paired cover.

Antecedent review checklist

1. Event or invariant? Transaction-triggered obligations get $rose/edge anchors; per-cycle invariants may use levels with same-cycle consequents.

2. Every spec qualifier present (valid, enable, mode) — in the antecedent, not the consequent?

3. No qualifier the spec does NOT impose (over-precision → vacuity)?

4. Paired cover written for the antecedent sequence, tracked in the merged regression?

5. Window bounds derived from the spec, not guessed generously?

6. Retrigger behavior considered: what happens if the trigger holds for N cycles?

7. Thread estimate acceptable: attempts × consequent threads × instances?

Key takeaways

• The antecedent encodes WHEN the obligation applies — most assertion bugs are antecedent bugs, in both directions.

• Level antecedents re-match every cycle they hold: false failures on held-request handshakes; $rose anchors one attempt per transaction.

• Qualifiers (valid/enable/mode) belong in the antecedent; in the consequent their absence becomes a false failure.

• Attempts × range = live threads; edge-anchoring and tight windows are the first performance fixes.

• Every antecedent needs a paired cover — precision without coverage proof is just well-organized vacuity.

Common pitfalls

• req |-> ##[1:N] gnt on a held-req protocol — spurious failures from expired early-attempt windows.

• Blanket $rose on genuinely per-cycle invariants — misses violations on cycles after the first.

• wvalid AND-ed into the consequent of a data check — protocol-legal idle cycles reported as failures.

• Generously widened windows "to be safe" — masks real latency regressions and multiplies threads.

• Tightening a noisy antecedent until it never fires, without a cover to notice — the assertion dies silently.