An implication a |-> b passes vacuously on every attempt where a is false. The consequent was never examined.
A stimulus that never raises a passes every time while verifying nothing. The usual causes are a typo in the antecedent, a tied-off enable, or a configuration that routes traffic elsewhere.
Assertion | Attempts | Real passes | Vacuous | Verdict |
|---|---|---|---|---|
ap_req_ack | 500000 | 4982 | 495018 | Healthy |
ap_retry_win | 500000 | 0 | 500000 | Red alert: retry never sampled high |
ap_err_resp | 500000 | 0 | 500000 | Red alert: never exercised |
Per-assertion real-pass counts come from metrics-enabled regressions, for example commercial assertion dashboards. Default pass or fail summaries do not separate real from vacuous passes, so a zero real-pass count is a red alert dressed in green.
Stimulus never generates the scenario, the antecedent is wrong such as a typo, or the scenario is configured off. The pass column alone cannot distinguish them.
The structural fix is a cover property on the antecedent of every implication. Cover hits turn “did this check ever try” into a regression number, and they double as scenario coverage.
The listing below is a fragment without a module, an illustration the course checks skip; Verilator 5.048 accepts it inside a module. The runnable testbench below it keeps the same idea with counters that sample at the clock edge.
// snippet
// The assert/cover pair - write them together, always
ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:4] ack);
cp_req: cover property (@(posedge clk) disable iff (!rst_n)
$rose(req)); // antecedent ever true?
cp_req_ack: cover property (@(posedge clk) disable iff (!rst_n)
$rose(req) ##[1:4] ack); // full success shape seen?
// Cover interesting variants, not just the minimum:
cp_b2b: cover property (@(posedge clk) disable iff (!rst_n)
$rose(req) ##[1:4] ack ##1 $rose(req)); // back-to-back transactions
cp_ack_min: cover property (@(posedge clk) disable iff (!rst_n)
$rose(req) ##1 ack); // shortest latency hit?
cp_ack_max: cover property (@(posedge clk) disable iff (!rst_n)
$rose(req) ##1 (!ack)[*3] ##1 ack); // first ack exactly at +4?Cover the antecedent of every implication; zero hits means the assert is decorative.
Cover the full success sequence for protocol-critical asserts, not just the trigger.
Cover window boundaries too; a ##[1:4] window that only ever hits ##1 has untested timing.
Cover properties never fail, they only count, at negligible cost next to their value.
Cover-first inverts the usual flow. Write the cover for the scenario first, run a smoke simulation, and confirm it hits.
If it never hits, fix the stimulus or the protocol understanding before writing the assert. A cover that never hits exposes a wrong mental model before a false assert pollutes the regression.
Write the cover property for the scenario first.
Run a quick smoke simulation and confirm the cover hits.
Convert to the assert, keeping the cover alive next to it.
In regression, monitor both: asserts catch violations, covers prove continued exercise.
Density review asks which protocol rules have no assertion at all. Walk the specification rule list against the assertion inventory, per interface and per state machine.
Every specification shall sentence should map to an assert, a cover, or a documented waiver. Typical finding: five assertions on the request channel and zero on the response channel.
Check the antecedent cover count. Then make it fail on purpose, for example by breaking the stimulus, to prove the check can fire. An assert nobody has seen fail or really pass is unproven in both directions.
One assert with cover counters that sample at the clock edge, the way a cover property does. Scenario 1 never raises retry, scenario 2 rises req during reset, scenario 3 violates the rule, scenario 4 grants in time.
module tb_vacuity;
timeunit 1ns; timeprecision 1ps;
logic clk = 1'b0;
always #5 clk = ~clk;
logic rst_n = 1'b0;
logic req = 1'b0;
logic retry = 1'b0;
logic gnt = 1'b0;
logic req_prev = 1'b0;
int unsigned ante_hits = 0; // cover: $rose(retry) sampled at the edge
int unsigned ok_hits = 0; // cover: $rose(retry) ##[1:8] gnt
int unsigned rose_post_reset = 0;
int unsigned fail_cnt = 0;
int unsigned bad = 0;
ap_retry_win: assert property (@(posedge clk) disable iff (!rst_n)
$rose(retry) |-> ##[1:8] gnt)
else begin
fail_cnt++;
$display("caught retry without grant at %0t", $time);
end
// Cover counters observe the signals at the clock edge, out of reset,
// like the cover properties above. They never touch the stimulus.
logic retry_q = 1'b0;
int win = 0; // cycles left in the open ##[1:8] window
always @(posedge clk) begin
if (!rst_n) win = 0;
else begin
if (gnt && win > 0) ok_hits++;
if (win > 0) win--;
if (retry && !retry_q) begin ante_hits++; win = 8; end
end
retry_q <= retry;
end
initial begin
@(negedge clk); @(negedge clk);
rst_n = 1'b1;
repeat (2) @(posedge clk);
// Scenario 1: ten request pulses, retry never raised; the assert is vacuous.
repeat (10) begin
@(negedge clk); req = 1'b1;
@(negedge clk); req = 1'b0;
end
if (ante_hits != 0) bad++;
// Scenario 2: req rises during reset and stays high past release.
@(negedge clk);
rst_n = 1'b0; req = 1'b1;
repeat (2) @(posedge clk);
@(negedge clk); rst_n = 1'b1;
req_prev = req; // req already high: settle tracker at 1
repeat (8) begin // eight quiet cycles, still no rise
@(posedge clk); #1;
if (req && !req_prev) rose_post_reset++;
req_prev = req;
end
if (rose_post_reset != 0) bad++;
// Fix the stimulus: drop req, then pulse it once after reset.
@(negedge clk); req = 1'b0;
@(posedge clk); #1; req_prev = req; // settle the tracker at 0
@(negedge clk); req = 1'b1;
@(posedge clk); #1;
if (req && !req_prev) rose_post_reset++;
req_prev = req;
@(negedge clk); req = 1'b0;
if (rose_post_reset != 1) bad++;
// Scenario 3: one retry with no grant inside eight cycles; the assert fires.
@(negedge clk); retry = 1'b1;
@(posedge clk);
@(negedge clk); retry = 1'b0;
repeat (8) @(posedge clk);
@(negedge clk); // let the fired action settle before counting
if (fail_cnt != 1) bad++;
// Scenario 4: retry followed by a grant two cycles later; no new failure.
@(negedge clk); retry = 1'b1;
@(posedge clk);
@(negedge clk); retry = 1'b0;
repeat (2) @(posedge clk);
@(negedge clk); gnt = 1'b1;
@(posedge clk); #1;
@(negedge clk); gnt = 1'b0;
repeat (8) @(posedge clk); // let the window close quietly
if (fail_cnt != 1) bad++; // still one: scenario 4 must not fire
if (ante_hits != 2) bad++;
if (ok_hits != 1) bad++;
if (bad == 0) $display("PASS: vacuous scenarios counted zero and the real violation was caught");
else $fatal(1, "FAIL: vacuity testbench");
$finish;
end
endmodulecaught retry without grant at 455000
PASS: vacuous scenarios counted zero and the real violation was caughtRun with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.