Q&A: Vacuity & Correctness

Q: What is a vacuous pass, and why is it dangerous?

Direct answer: an implication attempt whose antecedent never matched — the consequent was never tested, and the attempt counts as a pass. Vacuity is built into implication semantics and is usually healthy (idle cycles SHOULD pass). It becomes dangerous when every attempt of an assertion is vacuous for the whole regression: the assertion has checked nothing, reports green, and everyone reads green as verified. The classic causes: stimulus never produced the scenario, a typo made the antecedent unsatisfiable, or reset/enable gating swallowed it.

a: assert property (@(posedge clk) (req && grant_mode==3) |-> ##2 ack);

  ... but the testbench never drives grant_mode==3.

  every cycle: antecedent false → vacuous pass
  regression dashboard: a : PASS  (100 000 attempts)
  reality: ZERO attempts ever examined ack.

  An assertion that cannot fail is indistinguishable from a
  passing one — unless you measure non-vacuous activity.

Follow-up: 'Is vacuity ever the intended behavior?'

Yes — that is the point of encoding exceptions in the antecedent. The write-readback drill deliberately routes 'overwritten in between' traces into vacuity. Healthy design: common-case attempts vacuous, interesting attempts non-vacuous, and a cover proving the interesting ones happened.

Junior vs senior answer

• Junior: 'it passes because the if-part never happened'.

• Senior: distinguishes per-attempt vacuity (normal) from whole-regression vacuity (silent hole), lists the three usual causes, and notes vacuity-as-a-feature for spec exceptions.

Q: How do you detect assertions that are checking nothing?

Direct answer: measure, don't trust. Four layers: (1) tool vacuity reporting — simulators and formal tools can report pass-vacuous vs pass-non-vacuous counts per assertion; demand non-vacuous > 0 in regression signoff. (2) cover the antecedent — a paired cover property on the triggering scenario turns 'did it ever check' into a coverage metric. (3) mutation/fault injection — break the RTL deliberately (or use a mutation tool) and confirm the assertion fires; an assertion that survives its own bug is dead. (4) In formal: prove the antecedent is reachable — a cover that the tool proves unreachable exposes over-constraint or dead logic.

// the assert and its vacuity guard travel together:
ap_ack_in4: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:4] ack);

cp_req_seen: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req));                       // antecedent ever happened?

cp_req_b2b: cover property (@(posedge clk) disable iff (!rst_n)
  $rose(req) ##[1:4] ack ##[1:2] $rose(req));  // stressing case too

Follow-up: 'Your regression is green — convince me the assertions earned it.'

1. Show per-assertion non-vacuous pass counts > 0 across the merged regression.

2. Show the paired covers hit, including corner variants (back-to-back, boundary N).

3. Show at least one historical or injected failure per assertion family — proof the checker can fire.

Junior vs senior answer

• Junior: 'check the assertion fired in the log'.

• Senior: vacuity counters, paired covers as a metric, mutation as the ground truth, and reachability proofs on the formal side — a layered audit, not a glance.

Q: Why pair cover properties with assert properties?

Direct answer: assert and cover answer orthogonal questions — assert: was the rule ever violated? Cover: was the rule ever exercised? Green needs both: an assert with an unexercised antecedent is vacuously green; a hit cover with no assert is observation without checking. The pairing convention: for every assert, cover its antecedent scenario (minimum), plus the boundary variants the assert is supposed to police — maximum-latency ack, minimum-width pulse, full-window counts.

assert PASSES        assert FAILS
  cover HIT        ✓ verified behavior    real bug found
  cover NOT HIT    ⚠ VACUOUS — says       (impossible: a non-
                     nothing about DUT     vacuous fail implies
                                           the scenario occurred)

  Bottom-left is the dangerous quadrant — and it is invisible
  on a dashboard that only displays assertion pass/fail.

Follow-up: 'Which covers, concretely, for ack-within-4?'

• cover $rose(req) — the antecedent at all.

• cover $rose(req) ##4 ack — the boundary: latency exactly at the limit.

• cover $rose(req) ##1 ack — the other boundary: fastest legal ack.

• If any boundary cover never hits, the assert's bound was never actually stressed.

Junior vs senior answer

• Junior: 'cover tells you it happened'.

• Senior: the two-axis matrix, the dangerous quadrant, and boundary-value covers that stress the assertion's specific constants.

Q: Can all assertions pass and the design still be broken?

Direct answer: absolutely — green assertions bound the design only as tightly as the assertion set itself. Four standing gaps: (1) specification gaps — nobody wrote a property for the behavior that broke; assertions verify what you thought to state. (2) vacuity — properties exist but were never exercised. (3) weak/unbounded forms — liveness that cannot fail in finite simulation. (4) observability limits — sampled, clocked checks cannot see sub-cycle glitches, asynchronous misbehavior between edges, or analog effects. Assertions are necessary conditions, never sufficient ones.

Follow-up: 'So what closes the gap?'

• Verification-plan review tracing every spec MUST/SHALL to a property or test — attacks gap 1.

• Vacuity audits and paired covers — gap 2.

• Formal for liveness and unbounded claims; bounded sim forms documented as bounded — gap 3.

• Scoreboards and end-to-end data checking alongside assertions — different observability than point properties.

Junior vs senior answer

• Junior: 'yes, if you forgot an assertion' — one gap of four.

• Senior: enumerates the four gap classes and the counter-measure for each; frames assertions as necessary-not-sufficient.

Q: Strong vs weak operators — what changes at end of simulation?

Direct answer: the verdict for unfinished attempts. A weak sequence/property (the default for sequences in asserts) that is still in progress when simulation ends is not a failure — the pending attempt is discharged successfully or reported as merely unfinished. A strong form (strong(seq), s_eventually, s_until) demands completion: an attempt that cannot complete by end-of-time fails . In LTL terms weak = safety-style tolerance of incompleteness, strong = liveness obligation.

// weak: pending at $finish → quietly OK
a_weak: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:$] ack);

// strong: pending at $finish → FAILURE reported
a_strong: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> strong(##[1:$] ack));

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

Follow-up: 'Then why not mark everything strong in simulation?'

Every transaction legitimately in flight at $finish would fail — end-of-test noise proportional to traffic. The practical sim policy is bounded windows (which fail crisply mid-sim); strong operators earn their keep in formal, where infinite traces give liveness real meaning and fairness constraints keep it honest.

Junior vs senior answer

• Junior: 'strong must finish, weak need not'.

• Senior: ties it to end-of-sim verdict mechanics, explains why all-strong drowns in end-of-test noise, and lands on the policy: bounded in sim, strong in formal.

Key takeaways

• Per-attempt vacuity is healthy; whole-regression vacuity is a silent verification hole — measure non-vacuous counts.

• Pair every assert with covers on its antecedent AND its boundary constants.

• Green assertions are necessary, not sufficient: spec gaps, vacuity, weak forms, and observability limits all survive a green dashboard.

Common pitfalls

• Reading 'assertion passed' as 'behavior verified' without a hit cover behind it.

• Writing antecedents so specific they are unsatisfiable — permanently vacuous and permanently green.

• Marking sim properties strong wholesale — end-of-test in-flight traffic becomes a failure storm.