When Passing Is the Bug: Vacuity & Coverage

Green is not the same as checked

An implication a |-> b passes vacuously on every attempt where a is false — the consequent was never examined. A testbench that never raises a makes the assertion pass 100% of the time while verifying exactly nothing. This failure mode is silent, common (a typo in the antecedent, a tied-off enable, a config that routes traffic elsewhere), and invisible in a pass/fail summary. The cure is data: tools count real passes vs vacuous passes per assertion , and a real-pass count of zero is a red alert dressed in green.

THE VACUITY TRAP — assertion report worth reading

  assertion        attempts   real_pass   vacuous     fail
  ─────────────────────────────────────────────────────────
  ap_req_ack        500000        4982     495018        0   ← healthy
  ap_retry_win      500000           0     500000        0   ← RED ALERT
  ap_err_resp       500000           0     500000        0   ← RED ALERT
  ─────────────────────────────────────────────────────────
  ap_retry_win: retry |-> ##[1:8] gnt
  → retry was NEVER sampled high in any test.
    Either stimulus never generates retries (test gap),
    or the antecedent is wrong (e.g. retry vs retry_q typo),
    or retries are configured off (intentional? document it).
  The pass/fail column alone cannot distinguish these.

Cover properties on antecedents and key sequences

The structural fix: for every assert with an implication, write a cover property on the antecedent (and on the full success path for the important ones). Cover hit counts turn "did this check ever try?" into a regression-queryable number, and they double as scenario coverage for the protocol.

// 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_max: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req) ##4 $fell(ack) or $rose(req) ##4 ack); // latency boundary hit?

• Cover the antecedent of every implication — zero hits means the assert is decorative.

• Cover the full success sequence for protocol-critical asserts — proves the whole shape occurred, not just its trigger.

• Cover boundary cases of windows (minimum and maximum latency) — a ##[1:4] window that only ever hits ##1 has untested timing.

• Cover properties never fail — they only count; cost is negligible next to their diagnostic value.

Cover-first methodology and density review

Cover-first: see it hit, then assert it

1. Write the cover property for the scenario first (e.g. cover the req ##[1:4] ack shape).

2. Run a quick smoke sim; confirm the cover hits. If it never hits, fix stimulus or your understanding of the protocol BEFORE writing the assert.

3. Convert to the assert (cover sequence becomes consequent, trigger becomes antecedent); keep the cover alive next to it.

4. In regression, monitor both: assert fails catch violations, cover counts prove continued exercise as the design and tests evolve.

Cover-first inverts the usual flow and kills two failure modes at once: assertions that are vacuous from day one, and assertions written against a misunderstanding of the protocol (the cover never hitting tells you your mental model is wrong before a false assert pollutes the regression).

Assertion density review

Density review asks: which protocol rules have no assertion at all? Walk the spec's rule list (or the interface signal list) against the assertion inventory. Typical finding: the team has five assertions on the request channel and zero on the response channel, because the request side was debugged first. Density is reviewed per interface and per FSM — every spec 'must/shall' sentence should map to an assert, a cover, or a documented waiver.

Worked audit: a handshake assertion set

// The set under audit — looks complete, isn't
ap_hold:  assert property (@(posedge clk) disable iff (!rst_n)
            req && !ack |=> req);              // req holds until ack
ap_win:   assert property (@(posedge clk) disable iff (!rst_n)
            $rose(req) |-> ##[1:8] ack);       // bounded ack
ap_orph:  assert property (@(posedge clk) disable iff (!rst_n)
            $rose(ack) |-> $past(req));        // no orphan ack

AUDIT RESULT (after one regression with per-assertion stats)

  check     real_pass   vacuous    verdict
  ──────────────────────────────────────────────────────────────
  ap_hold       8 412    491 588   exercised ✓
  ap_win            0    500 000   VACUOUS — $rose(req) never true!
  ap_orph       4 982    495 018   exercised ✓

  Root cause: req rises during reset in this TB, so after disable iff
  releases, req is ALREADY high — $rose(req) never fires post-reset.
  ap_hold and ap_orph masked the gap: the bounded-latency rule (the
  most important one) was checked ZERO times across the regression.

  Fixes applied:
    1. cp_rose_req cover added → now visibly counts (would have caught this day one)
    2. antecedent broadened:  ($rose(req) or (req && $past(!rst_n))) |-> ##[0:8] ack
    3. stimulus fixed to deassert req across reset; cover re-confirmed

Interview angle

The two reliable questions: "What is a vacuous pass and why is it dangerous?" — implication with a never-true antecedent passes while checking nothing; dangerous because the summary is green. And "How do you guard against it?" — per-assertion vacuity statistics plus a cover property on every antecedent, reviewed at regression sign-off; bonus credit for describing cover-first development and for the audit instinct (an assert nobody has ever seen fail OR really pass is unproven in both directions). This topic is where methodology-round interviews decide you are senior.

Key takeaways

• Vacuous pass = antecedent never true; the consequent was never examined; the summary still says PASS.

• Every assert with an implication ships with a cover on its antecedent — zero cover hits is a sign-off blocker.

• Cover the success shape and the window boundaries too — minimum/maximum latency are favorite hiding spots.

• Cover-first: prove the scenario occurs before asserting about it — kills vacuous-from-birth assertions.

• Density review maps every spec 'shall' to an assert/cover/waiver — finds whole unchecked interfaces.

Common pitfalls

• Equating a passing regression with a verified protocol — vacuity statistics are part of sign-off, not optional.

• Covering only the antecedent and never the full success sequence — the window may never be exercised end to end.

• Writing asserts for rules the stimulus cannot trigger yet — vacuous noise that erodes trust in the suite.

• Deleting 'useless' covers during cleanup — they are the evidence the asserts still exercise after design changes.

• Ignoring an assertion that has never really passed — unproven checks fail you precisely when you finally need them.