Reviewing Assertions & Coverage

The assertions & coverage checklist

Assertions and covergroups are the checking machinery's checking machinery — and they fail silently in a specific way: an assertion whose antecedent never fires passes vacuously forever , and a covergroup with lazy bins reports closure on scenarios nobody chose. The review lens: for every property, what evidence exists that it ever ARMED? For every bin, who decided this bucket matters?

• Assert/cover pairing: every nontrivial assertion ships with a cover of its antecedent (or the interesting sub-sequence). Zero cover hits in regression = the assertion verified nothing.

• Vacuity audit: implications whose antecedent is contradictory, mis-clocked, or tied to a never-asserted mode pass 100% of the time — ask for the cover counts, not the pass counts.

• Reset gating: every concurrent assertion needs disable iff (with the RIGHT polarity and the right reset); missing gating produces a wall of bogus reset-time failures that teach people to ignore assertions.

• Clock and sampling: assertions on the correct clock domain, no @(posedge clk) properties sampling signals from another domain without synchronization.

• Bin intent: every bin name should answer 'which plan feature is this?' — auto-bins on multi-bit fields are bin explosion plus zero intent.

• illegal_bins vs ignore_bins: illegal = spec violation (a hit is a BUG and must error); ignore = legal but out of scope (shrinks the denominator). Swapping them either hides protocol violations or errors on legal traffic.

• Sampling event: covergroup sampled once per completed transaction from the monitor stream — per-cycle or driver-side sampling inflates closure with junk.

Worked review: a flawed SVA + covergroup file

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

Review findings

1. BLOCK — no disable iff (!rst_n) on either property: every reset window will fire p_handshake spuriously (valid X/garbage during reset), burying real failures in noise.

2. BLOCK — P2's antecedent contains write && !write — a contradiction; the antecedent can never be true, so the assertion passes vacuously on every cycle forever. This is exactly what an antecedent cover would have exposed on day one.

3. BLOCK — P1 uses ##[1:$] with no bound: the property cannot fail until end of simulation, where it reports as 'unfinished' at best. A real liveness requirement needs a spec-derived bound (##[1:MAX_READY]) or an explicit documented decision to use s_eventually with end-of-test semantics.

4. BLOCK — no cover property anywhere in the file: there is no evidence any antecedent ever armed. Pair each assert with cover property (valid && ready) at minimum.

5. BLOCK — cp_len is auto-binned: 256 bins, no intent, uncloseable and meaningless. Bins must encode plan buckets (single, small, max, illegal-adjacent).

6. NOTE — ignore_bins on 1'bx does nothing useful (covergroups do not sample X into value bins this way) and signals confusion between illegal_bins (spec violation → error) and ignore_bins (out of scope); also cg samples every clock rather than per accepted transaction — closure will be inflated by idle cycles repeating the same len value.

Corrected version

module bus_sva (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 |-> ##[1:16] ready;        // spec 4.1: max 16-cycle stall
  endproperty
  a_handshake: assert property (p_handshake);
  c_handshake: cover  property (valid);            // antecedent armed?
  c_backpress: cover  property (valid && !ready);  // stall path seen?

  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 (valid && ready));  // per accepted txn
    cp_len: coverpoint len {
      bins single = {1};
      bins small  = {[2:8]};
      bins large  = {[9:63]};
      bins max    = {64};
      illegal_bins over = {[65:255]};   // spec violation → error on hit
    }
    cp_write: coverpoint write { bins rd = {0}; bins wr = {1}; }
    x_wl: cross cp_write, cp_len;
  endgroup
  cg cg_i = new();
endmodule

Key takeaways

• Demand the antecedent cover counts in review — pass counts prove nothing; armed counts prove the assertion lives.

• Every property gets disable iff with the correct reset; unbounded ##[1:$] needs a spec-cited bound or an explicit liveness decision.

• Bins encode plan intent by name; auto-bins on multi-bit fields are a blocking finding, not a style nit.

• illegal_bins = spec violation that must error; ignore_bins = legal but out of scope — swapping them corrupts both checking and closure.

Common pitfalls

• Reviewing assertion PASS counts and feeling reassured — vacuous passes look identical to real ones.

• Contradictory or mode-gated antecedents that can never arm — undetectable without cover pairing.

• Covergroups sampled per clock instead of per transaction — closure inflated by idle repetition.

• Accepting 'we will add covers later' — later is after the bug escapes through the vacuous hole.