Vacuity and covers

A vacuous pass is an implication attempt whose antecedent never matched: the consequent was never tested, and the attempt counts as a pass. Per-attempt vacuity is healthy; idle cycles should pass. Whole-regression vacuity is a silent hole: every attempt vacuous, nothing checked, dashboard green.

Three usual causes cover most cases: the stimulus never produced the scenario, a typo made the antecedent unsatisfiable, or reset and enable gating swallowed it. Encoding spec exceptions in the antecedent is the legitimate use: the write-readback drill routes overwritten cases into vacuity on purpose.

Detection has four layers. Tool vacuity reporting separates pass-vacuous from pass-non-vacuous counts per assertion: demand non-vacuous above zero at signoff. Paired covers on the triggering scenario turn “did it ever check” into a metric. Mutation and fault injection break the RTL deliberately and confirm the assertion fires. In formal, prove the antecedent reachable: an unreachable cover exposes over-constraint or dead logic.

Assert and cover answer orthogonal questions: was the rule ever violated, and was it ever exercised. The dangerous quadrant is assert-pass with cover-missed: invisible on any dashboard that shows only pass and fail. Pair every assert with covers on its antecedent and on its boundary constants: the fastest legal ack and the slowest, the minimum pulse and the maximum.

Strong, weak, and bounded

The difference is the verdict for unfinished attempts. A weak sequence or property still in progress at end of simulation is not a failure: the pending attempt is discharged without failing. A strong form, strong(seq), s_until, or s_eventually, demands completion and fails attempts that cannot complete.

The listing below is not run in this course's checks: Verilator 5.048 does not support strong or s_eventually.

1
2
3
4
5
6
7
8
9

// not-run: Verilator 5.048 does not support strong or s_eventually
a_weak: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:$] ack);

a_strong: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> strong(##[1:$] ack));

a_live: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> s_eventually ack);

Marking everything strong in simulation drowns the run in end-of-test noise: every legitimately in-flight transaction fails. The standing policy is bounded windows in simulation and strong forms in formal, generated as twins from one spec rule.

A bounded proof guarantees no counterexample within K cycles of the initial state, and nothing beyond. Report it as clean to depth K with K stated next to the design's natural depths: FIFO depths, counter periods, timeout values. Failed induction means the property is not inductive, not that it is false: add strengthening invariants about reachable state until it closes, or accept a documented deep bound.

Debug and assume discipline

Triage before diving. Read the assertion as a spec sentence and locate the attempt start time: for a multi-cycle property the failure time is the end of the story, and the attempt began earlier by the property depth. Examine sampled values over that window in the assertion-debug view, never raw cursor reads.

A never-failing assertion earns trust through a four-step audit: non-vacuous counts above zero, boundary covers hit, firing on an injected bug, and a history of catching something in bring-up. Silence without that audit is unverified, not working.

Simulation evaluates one finite stimulated trace: failures are real but coverage equals stimulus quality, weak pending attempts dissolve at the end, and X flows as 4-state values. Formal evaluates all reachable traces under the assumes: a pass is a proof, liveness is fully meaningful, and free inputs take every value at once. When formal fails what sim never failed, check the counterexample stimulus for legality first: a missing assume masquerades as a bug nine times out of ten.

Each assume restricts the trace universe to behaviors satisfying it. Over-constraint removes the behavior containing the bug and the assert proves over the remainder: a false negative wearing a green checkmark. Contradictory assumes prove everything vacuously. Keep assumes honest with a cover sanity set that must stay reachable, a contradiction check every session, and one spec citation per assume.

Count is a vanity metric for assertion suites. Report plan-trace ratio of spec rules mapped to properties, non-vacuity ratio across merged regression, and mutation kill rate on a sampled set. Density per line of code serves only as a smell test for blocks at zero.

Testbench

The bench runs the vacuity audit for real: four requests that never use mode 3, where the assert stays green and its cover reads zero, then two mode-3 requests, one acked late. A bounded-liveness check and its cover run beside them.

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

module tb_qa_vacuity;
  logic clk = 0, rst_n = 0, req = 0, ack = 0;
  logic [1:0] grant_mode = 0;
  always #5 clk = ~clk;
  int fails = 0, ante_hits = 0, done_hits = 0;
  localparam int MAX = 8;

  // The assert and its paired cover on the antecedent: write them together.
  a_mode3: assert property (@(posedge clk) disable iff (!rst_n)
    (req && grant_mode == 3) |-> ##2 ack) else fails++;
  c_mode3: cover property (@(posedge clk) disable iff (!rst_n)
    req && grant_mode == 3) ante_hits++;
  // Bounded liveness: the simulation form of "every request eventually acked".
  a_bounded: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:MAX] ack) else fails++;
  c_done: cover property (@(posedge clk) disable iff (!rst_n)
    $rose(req) ##[1:MAX] ack) done_hits++;

  task automatic request(logic [1:0] mode, int lat);
    @(negedge clk) req = 1; grant_mode = mode;
    @(negedge clk) req = 0;
    repeat (lat - 1) @(negedge clk);
    ack = 1; @(negedge clk) ack = 0;
    repeat (3) @(negedge clk);
  endtask

  initial begin
    repeat (2) @(negedge clk);
    rst_n = 1;
    repeat (4) request(1, 2);                    // mode 3 never used
    $display("4 requests in mode 1: a_mode3 %0d failures, its antecedent cover %0d hits (vacuous)", fails, ante_hits);
    if (fails != 0 || ante_hits != 0) $fatal(1, "FAIL: vacuous phase");
    request(3, 2);                               // mode 3, acked on time
    request(3, 3);                               // planted: mode 3, acked a cycle late
    $display("2 requests in mode 3: a_mode3 %0d failure, cover %0d hits; bounded liveness covered %0d requests", fails, ante_hits, done_hits);
    if (fails != 1 || ante_hits != 2 || done_hits != 6) $fatal(1, "FAIL: %0d %0d %0d", fails, ante_hits, done_hits);
    $display("PASS: the cover exposed the vacuous phase, and the assert caught the late ack once mode 3 was used");
    $finish;
  end
endmodule

4 requests in mode 1: a_mode3 0 failures, its antecedent cover 0 hits (vacuous)
2 requests in mode 3: a_mode3 1 failure, cover 2 hits; bounded liveness covered 6 requests
PASS: the cover exposed the vacuous phase, and the assert caught the late ack once mode 3 was used

Related topics

• Data & Reset Drills

• Q&A: Operators & Semantics