The Assertion Review Checklist

The six-point checklist

Everything from the previous four lessons compresses into six questions you ask of every assertion in review. Senior engineers run this list almost unconsciously; interviews for senior roles probe whether you have it at all. Memorize it as a list — then internalize it by applying it to the flawed module below.

1. COVER PAIRING — does every assert with an implication have a cover on its antecedent (and the success shape for critical rules)? Zero cover hits = vacuous = sign-off blocker.

2. ANTECEDENT PRECISION — does the attempt start exactly once per transaction ($rose of a qualifier), not every cycle of a level or unconditionally?

3. RESET GATING — disable iff with the correct polarity and the actual reset; does the property also behave when signals are mid-flight as reset asserts?

4. X-AWARENESS — would an X on a key signal pass unnoticed? (X !== 1 makes !sig comparisons truthy in surprising ways; consider $isunknown checks on qualifiers.)

5. LABEL & MESSAGE — unique, greppable label (ap_<block>_<rule>); action block printing $sampled values and $time so the failure is diagnosable from the log alone.

6. BOUNDED LIVENESS — every 'eventually' bounded with a spec-derived window for simulation; unbounded forms reserved for formal, behind a parameter.

REVIEW FLOW — applying the checklist

   for each assert property:
     1. cover pair exists?        ──no──► add cp_* / block sign-off
     2. antecedent fires per txn? ──no──► sharpen with $rose/qualifier
     3. disable iff right reset,
        right polarity?           ──no──► fix gating
     4. X on inputs detected?     ──no──► add $isunknown guard assert
     5. label unique + $sampled
        in action block?          ──no──► relabel, rewrite message
     6. liveness bounded?         ──no──► spec-derived ##[m:N] window
     ──all yes──► approve; record cover hit counts at next regression

The exercise: review this module

This checker compiles, runs, and its regression is green. Apply the checklist and find the six problems before reading the answer key.

module bus_checks (
  input logic clk, rst_n,
  input logic req, gnt, valid,
  input logic [31:0] data
);
  // R1: every request eventually granted
  a1: assert property (@(posedge clk)
        req |-> s_eventually gnt);

  // R2: data stable while valid high and not granted
  a2: assert property (@(posedge clk) disable iff (rst_n)
        valid && !gnt |=> $stable(data));

  // R3: grant only follows a request
  a3: assert property (@(posedge clk) disable iff (!rst_n)
        gnt |-> $past(req))
        else $error("orphan grant: req=%b gnt=%b", req, gnt);

  // R4: valid never unknown after reset
  a4: assert property (@(posedge clk) disable iff (!rst_n)
        valid |-> data inside {[0:32'hFFFF_FFFF]});
endmodule

Answer key — the six problems

1. a1 unbounded liveness in a sim checker: s_eventually leaks a live thread per lost grant and reports at end-of-sim. Fix: spec-derived bound, req |-> ##[1:MAX_GNT] gnt (checklist point 6).

2. a1 weak antecedent: level-sensitive req starts a NEW attempt every cycle req stays high — attempt explosion and multiple redundant threads per transaction. Fix: $rose(req), or req && !$past(req) (point 2).

3. a1 missing reset gating entirely: attempts started before reset asserts keep running through reset garbage. Fix: disable iff (!rst_n) (point 3).

4. a2 reset polarity inverted: disable iff (rst_n) disables the assertion during NORMAL operation and enables it in reset — it has never actually checked anything while the design ran. Fix: disable iff (!rst_n) (point 3 — and note the regression was green!).

5. a3 action block prints raw req/gnt: those are post-edge values that can contradict what the assertion sampled. Fix: $sampled(req), $sampled(gnt), add $time. Also $past(req) at the first post-reset edge reads a pre-reset value — guard with reset-aware antecedent (point 5, plus a point-3 subtlety).

6. a4 checks nothing: every 32-bit value is inside [0:FFFF_FFFF], and X data makes 'inside' evaluate unknown — the implication is not crisply violated, so corruption slides through. Fix: valid |-> !$isunknown(data) (point 4). And across the whole module: NOT ONE cover property — every one of these could be vacuous and no one would know (point 1).

// The repaired module
module bus_checks (
  input logic clk, rst_n,
  input logic req, gnt, valid,
  input logic [31:0] data
);
  localparam int MAX_GNT = 64;                  // from the spec

  a1_gnt_bounded: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:MAX_GNT] gnt)
    else $error("[%0t] grant timeout > %0d", $time, MAX_GNT);
  c1_req: cover property (@(posedge clk) disable iff (!rst_n) $rose(req));
  c1_ok:  cover property (@(posedge clk) disable iff (!rst_n)
    $rose(req) ##[1:MAX_GNT] gnt);

  a2_data_stable: assert property (@(posedge clk) disable iff (!rst_n)
    valid && !gnt |=> $stable(data))
    else $error("[%0t] data moved while stalled: %h -> %h",
                $time, $past($sampled(data)), $sampled(data));
  c2_stall: cover property (@(posedge clk) disable iff (!rst_n)
    valid && !gnt);

  a3_no_orphan: assert property (@(posedge clk) disable iff (!rst_n)
    gnt && $past(rst_n) |-> $past(req))
    else $error("[%0t] orphan grant req=%b gnt=%b",
                $time, $sampled(req), $sampled(gnt));
  c3_gnt: cover property (@(posedge clk) disable iff (!rst_n) $rose(gnt));

  a4_data_known: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> !$isunknown(data))
    else $error("[%0t] X/Z on data while valid", $time);
  c4_valid: cover property (@(posedge clk) disable iff (!rst_n) valid);
endmodule

Running the review at scale

• Make the checklist a code-review template: six checkbox lines in the PR description for any file adding assert property.

• Automate what you can: lint for assert-without-cover, for missing disable iff, for s_eventually outside formal-only files, for unlabeled assertions.

• Pull per-assertion vacuity statistics into the regression dashboard — checklist point 1 becomes a queryable number, reviewed at every milestone.

• Re-review after design changes, not just at creation: a renamed qualifier or repartitioned FSM can turn a precise antecedent vacuous overnight; the cover counts catch it.

• Keep an answer-key module like the one above in the team's onboarding material — it teaches the checklist faster than any document.

Interview angle

Senior interviews often hand you a flawed assertion module exactly like the exercise above and ask what is wrong with it. Work the checklist out loud in order — cover pairing, antecedent precision, reset gating (check the polarity character by character; the inverted disable iff is the most-planted bug), X-awareness, labels and $sampled messages, bounded liveness. Finding five of six silently is worth less than finding four while narrating a systematic method: the interviewer is hiring the process, not the bug count. Close by saying which problems a green regression would have hidden — the inverted reset polarity and the missing covers — because that distinction is the whole point of assertion methodology.

Key takeaways

• Six points: cover pairing, antecedent precision, reset gating, X-awareness, label/message quality, bounded liveness.

• A green regression proves nothing about an assertion suite until vacuity data and cover hits are reviewed.

• Inverted disable iff polarity is the classic planted bug — the assertion checks only during reset and never fails.

• X-awareness needs explicit $isunknown checks — range and equality comparisons quietly absorb X.

• Review is a repeatable process: checklist in the PR template, lint for the mechanical points, dashboards for vacuity.

Common pitfalls

• Reviewing assertions by eyeballing the property only — half the checklist (covers, vacuity, labels) lives outside the property text.

• Trusting disable iff polarity without tracing the actual reset signal and its sense — the most common silent killer.

• Treating range checks like inside {[0:MAX]} as X-protection — X makes the comparison unknown, not false.

• Skipping re-review after RTL changes — antecedent qualifiers go stale and assertions rot into vacuity.

• Demonstrating bug-finding without a method in interviews — narrate the checklist; the process is what is being hired.