The six-point checklist

Everything in this topic compresses into six questions for every assertion in review. Memorize the list, then internalize it on the flawed module below.

1. COVER PAIRING: does every implication have a cover on its antecedent, and the success shape for critical rules? Zero cover hits is a sign-off blocker.

2. ANTECEDENT PRECISION: does the attempt start once per transaction, on an edge qualifier, not every cycle of a level?

3. RESET GATING: is disable iff the correct polarity on the actual reset, including mid-flight attempts as reset asserts?

4. X-AWARENESS: are X checks explicit? Range and inside checks catch X only by accident (X counts as false in an assertion) and catch nothing on two-state engines; write !$isunknown.

5. LABEL AND MESSAGE: is the label unique and greppable, with $sampled values and time in the action block?

6. BOUNDED LIVENESS: is every eventually bounded with a spec-derived window for simulation?

The exercise: review this module

This checker hides seven problems. It is not run in this course's checks because Verilator 5.048 does not support s_eventually. Find the seven before reading the key.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// not-run: Verilator 5.048 does not support s_eventually; also a review exercise
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 and repaired module

Seven problems: three in a1 (unbounded liveness, a level antecedent and a missing reset gate), inverted reset polarity in a2, raw-signal printing in a3 with labels a1 to a4 that nobody can grep, an obscure range check in a4 that states no X intent, and zero covers across the module.

The repaired module bounds the grant window, hardens the antecedents, fixes the polarity, checks $isunknown explicitly, and prints sampled values. Its seen mask is harness-only. The testbench confirms that three injected faults fire (timeout, moved data, orphan grant), that the mid-flight reset and the held request stay silent, and that the unknown-data injection holds without firing on two-state checks.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

module bus_checks_fixed (
  input logic clk, rst_n,
  input logic req, gnt, valid,
  input logic [31:0] data,
  output logic [3:0] seen    // harness-only: bit i latches when check i fires
);
  localparam int MAX_GNT = 8;               // from the spec
  initial seen = 4'b0;

  a1_gnt_bounded: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:8] gnt)   // literal 8 == MAX_GNT; Verilator needs a numeric range
    else begin
      seen[0] <= 1'b1;
      $display("caught grant timeout at %0t", $time);
    end

  a2_data_stable: assert property (@(posedge clk) disable iff (!rst_n)
    valid && !gnt |=> $stable(data))
    else begin
      seen[1] <= 1'b1;
      $display("caught moved data at %0t: %h -> %h (sampled)", $time, $past(data), $sampled(data));
    end

  a3_no_orphan: assert property (@(posedge clk) disable iff (!rst_n)
    gnt && $past(rst_n) |-> $past(req))
    else begin
      seen[2] <= 1'b1;
      $display("caught orphan grant at %0t: sampled req=%b gnt=%b", $time, $sampled(req), $sampled(gnt));
    end

  a4_data_known: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> !$isunknown(data))
    else begin
      seen[3] <= 1'b1;
      $display("caught unknown data at %0t while valid", $time);
    end
endmodule

caught grant timeout at 235000
caught moved data at 465000: 00000000 -> 00000001 (sampled)
caught moved data at 475000: 00000001 -> 00000002 (sampled)
caught moved data at 485000: 00000002 -> 00000003 (sampled)
caught moved data at 495000: 00000003 -> 00000004 (sampled)
caught moved data at 515000: 00000004 -> 00000000 (sampled)
caught orphan grant at 535000: sampled req=0 gnt=1
PASS: three faults fired as reviewed, reset and held-request cases stayed silent, X held on two-state, covers hit

Running the review at scale

Make the checklist a code-review template: six checkbox lines in the pull-request description for any file adding assert property. Automate the mechanical points with lint.

Lint for assert-without-cover, missing disable iff, s_eventually outside formal-only files, and unlabeled assertions. Pull per-assertion vacuity statistics into the regression dashboard, and re-review after design changes, not just at creation.

Related topics

• Where Assertions Live