Vacuous Success

What vacuous success means

An implication attempt where the antecedent never matches is declared a vacuous pass : the obligation never activated, so nothing was violated — logically true, verification-empty. The danger is statistical: an assertion can report thousands of passes, all vacuous, while the consequent logic has never been examined once . A green assertion column proves nothing unless you separately prove the antecedents fired. This is the single most common assertion-quality failure in real projects: the checker was present, enabled, passing — and asleep.

WAVEFORM — vacuity: req never rises

clk :  1    2    3    4    5    6    7    8
req :  0    0    0    0    0    0    0    0
gnt :  0    0    0    0    0    0    0    0
       v    v    v    v    v    v    v    v
req |-> ##2 gnt
Every tick starts an attempt; req=0 at each → antecedent
no-match → 8 VACUOUS passes. Tool log: "assertion passed: 8".
gnt logic was never checked. The log looks identical to a
healthy run unless vacuous passes are reported separately.

The assert + cover pairing discipline

Vacuity has a standard antidote: for every implication, cover the antecedent (or the full sequence). The assert proves "never violated"; the cover proves "actually exercised". Sign-off requires both: assertion pass count green AND its paired cover hit at least once (in the merged regression, not per seed). Many teams codify this as a lint rule — an assert property of an implication without a sibling cover property fails review.

// The checker
property p_gnt_in2;
  @(posedge clk) disable iff (!rst_n) $rose(req) |-> ##[1:2] gnt;
endproperty
a_gnt: assert property (p_gnt_in2);

// The paired vacuity guard — antecedent really fires:
c_gnt_ante: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req));

// Even better — cover the full success path end to end:
c_gnt_full: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req) ##[1:2] gnt);
// Note the cover uses a SEQUENCE (no implication): covering
// "ante |-> cons" would be satisfied by a vacuous pass too!

SIGN-OFF MATRIX — assert and cover are answering different questions

                        cover HIT          cover NOT hit
  assert PASSES     │ checked & clean   │ VACUOUS — stimulus gap,
                    │ (real sign-off)   │ fix the test, not the RTL
  ──────────────────┼───────────────────┼─────────────────────────
  assert FAILS      │ real bug (or bad  │ (impossible: a non-vacuous
                    │ assertion) — debug│  fail implies ante fired)

Vendor vacuity reporting

Simulators distinguish real and vacuous passes internally; the reporting just defaults to quiet. Questa exposes vacuity via vsim -assertdebug with assertion report columns separating vacuous counts; VCS tags them under -assert vacuouspass+report style options; Xcelium reports them in assertion summary tables. Formal tools go further: a property that can only pass vacuously (antecedent unreachable) is flagged as a vacuity/trigger failure outright. Whatever the tool, the regression flow should publish three numbers per assertion: real passes, vacuous passes, failures — and a vacuous-only assertion should block sign-off exactly like a failure.

// Make vacuity visible in any simulator: action-block counting
int real_pass, vac_hint;
a_gnt2: assert property (@(posedge clk) $rose(req) |-> ##[1:2] gnt)
  real_pass++;             // pass action runs on REAL passes only? NO —
                           // it runs on vacuous passes too in most tools.
// The portable discipline is therefore the cover pairing:
c_fired: cover property (@(posedge clk) $rose(req));
final begin
  if (real_pass > 0 && !$past(1)) ; // illustrative only
  // Sign-off rule implemented in the regression script:
  //   FAIL the run if a_gnt2 passes > 0 times but c_fired hits == 0
end

Interview angle and review

Interview angle

• "An assertion passed 10,000 times — is the design verified?" — the expected answer: not unless the antecedent fired; all 10,000 may be vacuous. Then describe the assert+cover pairing.

• "Why cover the antecedent sequence rather than the implication property?" — covering the implication is satisfied by vacuous passes; you must cover the sequence so only real activation counts.

• "How does formal treat vacuity differently?" — formal can prove the antecedent unreachable and flags the property, while simulation just silently never exercises it.

• "Where does vacuity hide in practice?" — over-precise antecedents (wrong polarity, missed qualifier, gated-off enable), reset gating that never releases, tied-off config bits in the test.

Key takeaways

• Vacuous pass = antecedent never matched; the consequent was never checked at all.

• Pass counts are meaningless without evidence the antecedent fired — pair every assert with a cover of the antecedent.

• Cover the SEQUENCE (antecedent or full success path), never the implication property itself.

• Publish real/vacuous/fail counts in regression; vacuous-only assertions block sign-off like failures.

Common pitfalls

• Equating green assertion columns with verified behavior — the classic silent-checker failure.

• cover property (a |-> b) as the vacuity guard — vacuous attempts satisfy it; cover the sequence instead.

• Checking covers per seed instead of on the merged regression — rare antecedents legitimately need many seeds.

• Antecedents conjoined with an enable that the testbench never turns on — structurally vacuous forever.

• Relying on pass-action blocks to count real passes — many tools execute them on vacuous passes too.