Armed counts, not pass counts

An assertion whose antecedent never fires passes vacuously forever. A covergroup with lazy bins reports closure on scenarios nobody chose.

The review lens has two halves. For every property, what evidence exists that it ever armed. For every bin, who decided this bucket matters.

Worked review: a quiet covergroup file

The listing below is the file under review. It is a checker module with no testbench, so this course's checks do not run it.

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

// not-run: fragment: a checker module under review, with no testbench top
module bus_sva (input logic clk, rst_n, valid, ready, write,
                input logic [7:0] len);

  // P1: every request eventually gets ready
  property p_handshake;
    @(posedge clk) valid |-> ##[1:$] ready;
  endproperty
  assert property (p_handshake);

  // P2: legal burst length when accepted
  property p_len;
    @(posedge clk) (valid && ready && write && !write)
      |-> (len inside {[1:64]});
  endproperty
  assert property (p_len);

  covergroup cg @(posedge clk);
    cp_len:   coverpoint len;
    cp_write: coverpoint write {
      ignore_bins bad_w = {1'bx};      // "x is illegal"
    }
    x_wl: cross cp_write, cp_len;
  endgroup
  cg cg_i = new();
endmodule

1. BLOCK — no disable iff on either property. Every reset window fires on garbage. The noise teaches the team to ignore assertions, which is worse than having none.

2. BLOCK — P2's antecedent contradicts itself. write && !write can never be true, so the property passes vacuously on every cycle forever. An antecedent cover would have exposed this on day one.

3. BLOCK — P1 uses an unbounded ##[1:$]. The property cannot fail until the end of simulation, where tools report it as pending or unfinished. A real liveness requirement needs a spec-derived bound.

4. BLOCK — no cover property anywhere. There is no evidence any antecedent ever armed. Each assert ships with a cover of its antecedent at minimum.

5. BLOCK — cp_len is auto-binned with no intent. An 8-bit point with no bins yields up to 64 auto-bins by default: still intent-free and uncloseable. Bins must encode plan buckets by name.

6. NOTE — the X ignore_bin signals confusion. X and Z values are sampled but auto-dropped from value-bin counts unless explicit X bins exist, so ignore_bins {1'bx} on a 1-bit point is legal syntax with no meaning. It also suggests illegal and ignore were not distinguished: illegal means spec violation and must raise, ignore means legal but out of scope.

7. NOTE — the covergroup samples every clock. Idle cycles repeat the same len value and inflate closure. Sample once per accepted transaction from the monitor stream.

Bounded checks and honest bins

The monitor below is the procedural form of the bounded-liveness property both course tools can run. It flags a stall on the first waited cycle past the bound of 4, while the request is still waiting, so a hang is flagged too. Stalls that finish within the bound go into named bins.

Reset holds all counters at zero, so reset-window garbage can never pollute them. The testbench scripts stalls of 0, 2, 3, and 6 cycles, then a request that is still waiting, and proves each lands in the right place.

Watch valid against ready. The fifth sampled wait is past the bound of 4, and the checker flags it then, before ready arrives.

• Slot 0: idle, valid 0 and ready 0.

• Slot 1: valid rises while ready stays low: first waited cycle.

• Slots 2 to 4: still waiting: waited cycles 2, 3 and 4. Slot 4 reaches the bound.

• Slot 5: still waiting: the fifth waited cycle is past the bound, so the checker flags it here.

• Slot 6: ready rises at last: the late handshake completes, already flagged.

• Slot 7: both rest at 0.

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

module bound_mon (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        valid,
  input  logic        ready,
  output logic [31:0] bin0,    // accepted with no wait
  output logic [31:0] bin12,   // stalled 1-2 cycles
  output logic [31:0] bin34,   // stalled 3-4 cycles
  output logic [31:0] over     // stalled past OK_STALL
);
  localparam int OK_STALL = 4;
  int wait_cnt;
  bit active;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wait_cnt <= 0;   active <= 1'b0;
      bin0 <= 0;       bin12 <= 0;
      bin34 <= 0;      over <= 0;
    end else if (valid && ready && !active) begin
      bin0 <= bin0 + 1;                        // no wait at all
    end else if (valid && !ready && !active) begin
      active <= 1'b1;  wait_cnt <= 1;
    end else if (active && !ready) begin
      wait_cnt <= wait_cnt + 1;
      if (wait_cnt == OK_STALL) over <= over + 1;  // flag once, while still waiting
    end else if (active && ready) begin
      active <= 1'b0;
      if (wait_cnt <= 2)             bin12 <= bin12 + 1;
      else if (wait_cnt <= OK_STALL) bin34 <= bin34 + 1;
      // past OK_STALL: already flagged while waiting
    end
  end
endmodule

The corrected file below is a checker module with no testbench, so this course's checks do not run it.

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

// not-run: fragment: the corrected checker module, with no testbench top
module bus_cov (input logic clk, rst_n, valid, ready, write,
                input logic [7:0] len);

  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  property p_handshake;
    valid |-> ##[0:16] ready;        // spec 4.1: at most 16 stalled cycles,
                                     // counted from the valid cycle itself
  endproperty
  a_handshake:  assert property (p_handshake);
  c_handshake:  cover  property (valid);
  c_backpress:  cover  property (valid && !ready);

  property p_len;
    (valid && ready && write) |-> (len inside {[1:64]});
  endproperty
  a_len: assert property (p_len);
  c_len: cover  property (valid && ready && write);

  covergroup cg @(posedge clk iff (rst_n && valid && ready));
    cp_len: coverpoint len iff (write) {   // writes only, like a_len
      bins single = {1};
      bins small  = {[2:8]};
      bins large  = {[9:63]};
      bins max    = {64};
      illegal_bins bad = {0, [65:255]};    // spec violation: a hit must raise
    }
    cp_write: coverpoint write { bins rd = {0}; bins wr = {1}; }
  endgroup
  cg cg_i = new();
endmodule

The covergroup samples once per accepted transfer, gated off reset. cp_len counts writes only, matching a_len, so length 0 and lengths above 64 both fall in the illegal bin. The illegal bin marks spec violations that must raise, which is the opposite of ignoring out-of-scope traffic. The handshake bound counts from the valid cycle, so ##[0:16] also accepts a zero-wait handshake.

Common mistakes

• Accepting auto-bins on a multi-bit field as coverage. Up to 64 intent-free bins still say nothing about the plan.

• Sampling per clock instead of per transaction. Idle repetition inflates closure with junk.

• Accepting a promise of covers later. Later is after the bug escapes through the vacuous hole.

• Swapping illegal and ignore. One hides protocol violations, the other raises on legal traffic.

Related topics

• SVA fundamentals

• Covergroup basics

• SVA quickfire Q&A