Passing without checking

An attempt whose antecedent never matches is a vacuous pass. The obligation never activated, so nothing was violated and nothing was checked.

The risk is statistical. Thousands of passes can pile up while the consequent logic is never examined once.

• Slot 0: req 0. Attempt starts, antecedent misses, vacuous pass.

• Slot 1: req 0. Same outcome, second vacuous pass.

• Slot 2: req 0. Same outcome, third vacuous pass.

• Slot 3: req 0. Same outcome, fourth vacuous pass.

• Slot 4: req 0. Same outcome, fifth vacuous pass.

• Slot 5: req 0. Same outcome, sixth vacuous pass.

Six attempts, six vacuous passes, zero examinations of gnt. The tool log looks identical to a healthy run.

Cover the antecedent

Every implication ships with a cover of its antecedent sequence. The assert proves never violated, and the cover proves actually exercised.

Cover the sequence, never the implication. Covering ante |-> cons is itself satisfied by vacuous passes.

1
2
3
4
5
6
7

// snippet
a_gnt: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:2] gnt);
c_ante: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req));
c_full: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req) ##[1:2] gnt);

Making vacuity visible

Simulators separate real and vacuous passes in assertion reports. Consult the vendor docs for the exact options, since flag names differ across tools.

Keep the sign-off rule in the regression script. Fail the run when an assertion passes but its paired cover has zero hits across the merged regression.

Testbench

A never-firing antecedent plus the paired cover that proves the passes are vacuous. The bench reads a procedural mirror of the cover count, then fires two real requests to show the assertion is live: one granted, one not.

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
38
39
40
41
42
43

module tb_impl_vac;
  timeunit 1ns; timeprecision 1ps;
  logic clk = 0;
  always #5 clk = ~clk;
  logic rst_n = 0;
  logic req = 0;
  logic gnt = 0;
  logic req_q = 0;
  int ante_hits = 0;
  int fails = 0;

  a_vac: assert property (@(posedge clk) disable iff (!rst_n) req |-> gnt)
    else fails++;
  c_ante: cover property (@(posedge clk) disable iff (!rst_n) $rose(req));

  // Procedural mirror of c_ante, so the bench can read the hit count.
  always @(posedge clk) begin
    req_q <= req;
    if (rst_n && req && !req_q) ante_hits <= ante_hits + 1;
  end

  initial begin
    int vac_hits, vac_fails;
    repeat (2) @(negedge clk);
    rst_n = 1;
    repeat (6) @(negedge clk);       // phase 1: req never rises
    vac_hits = ante_hits;
    vac_fails = fails;
    req = 1; gnt = 1;                // phase 2: a granted request
    @(negedge clk);
    req = 0; gnt = 0;
    @(negedge clk);
    req = 1;                         // phase 3: a request with no grant
    @(negedge clk);
    req = 0;
    repeat (2) @(negedge clk);
    if (vac_hits == 0 && vac_fails == 0 && ante_hits == 2 && fails == 1)
      $display("PASS: 6 vacuous cycles: 0 cover hits, 0 failures; then 2 real requests: 2 hits, 1 failure");
    else
      $fatal(1, "FAIL: vac_hits=%0d vac_fails=%0d ante_hits=%0d fails=%0d", vac_hits, vac_fails, ante_hits, fails);
    $finish;
  end
endmodule

PASS: 6 vacuous cycles: 0 cover hits, 0 failures; then 2 real requests: 2 hits, 1 failure

Related topics

• Designing Good Antecedents

• Assertion Debug