Interview Question · Concept

Vacuous Success in SVA Implication

L1 JuniorL2 Mid-Levelsvaimplicationvacuity

The interviewer asks

What is a vacuous pass of a property like req |=> ack, and why can it hide a bug?

Reveal the Model Answer

An implication has an antecedent (the left side) and a consequent (the right side). On every clock tick where the antecedent does not match, the implication succeeds vacuously. There is nothing to check, so those attempts count as passes. An assertion whose antecedent never fires reports success without ever checking the consequent. Cover the antecedent, and read the real hit count before trusting a clean run.

Six Attempts, Two Real ChecksEvery edge starts an attempt of req |=> gnt. Only the attempts where req is high check anything.req |=> gntMeasured on Verilator 5.052: one copy of the assertion per lane

attempt startspassfailvacuous success: the antecedent did not match

Edge 1 · t=5
req is low, so the attempt from 5 ends at once with a vacuous success. Its pass action still runs.
Edge 2 · t=15
req is high at 15. This attempt is real, and it waits for the next edge to check gnt.
Edge 3 · t=25
gnt is high, so the attempt from 15 passes. The attempt that starts at 25 is vacuous, even though gnt is high: no request asked for it.
Edge 4 · t=35
Another vacuous success. gnt is still high, and still nothing checks it.
Edge 5 · t=45
A second request starts a real attempt, which will look at gnt at 55.
Edge 6 · t=55
gnt is low, so the attempt from 45 fails. The attempt from 55 is vacuous.
More context
The pass action ran five times, but only one of those passes checked gnt. Counting the edges where req was high gives the real number of checks: two.

Read the lanes as text

attempt @5, from edge 1 (t=5): succeeds vacuously at edge 1 (t=5).
attempt @15, from edge 2 (t=15): passes at edge 3 (t=25).
attempt @25, from edge 3 (t=25): succeeds vacuously at edge 3 (t=25).
attempt @35, from edge 4 (t=35): succeeds vacuously at edge 4 (t=35).
attempt @45, from edge 5 (t=45): fails at edge 6 (t=55).
attempt @55, from edge 6 (t=55): succeeds vacuously at edge 6 (t=55).

Sampled values, edge 1 to 6: req 0 1 0 0 1 0; gnt 0 0 1 1 0 0.

The program behind the lanes

The lanes come from running this program on Verilator 5.052. Each lane is a separate copy of gnt_next that can start only at that lane's edge, so every verdict and its edge are read from that copy's own output.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic req = 0, gnt = 0;

  gnt_next: assert property (@(posedge clk) req |=> gnt);

  initial begin
    @(negedge clk); req = 1;            // request sampled at 15
    @(negedge clk); req = 0; gnt = 1;   // grant sampled at 25 and 35
    @(negedge clk);
    @(negedge clk); req = 1; gnt = 0;   // request sampled at 45
    @(negedge clk); req = 0;            // no grant at 55
    @(negedge clk);
    $finish;
  end
endmodule

A vacuous success ends at the edge where it starts. A real attempt spans to the edge where its consequent is checked.

Tick with req low
The antecedent has no match. The attempt ends at once as a vacuous success.
Tick with req high
The antecedent matches, so the consequent is checked one tick later. Only this is a real pass or a failure.
The report
Zero failures plus zero antecedent hits means the property never checked anything.

Self-Check

Tick each key point you covered in your answer.

Key point 1 An implication has an antecedent (the left side) and a consequent (the right side). Key point 2 On every clock tick where the antecedent does not match, the implication succeeds vacuously. Key point 3 There is nothing to check, so those attempts count as passes. Key point 4 An assertion whose antecedent never fires reports success without ever checking the consequent. Key point 5 Cover the antecedent, and read the real hit count before trusting a clean run.

What Interviewers Listen For (Junior)

A good junior answer defines vacuous success and says that it counts as a pass. It suggests a cover property on the antecedent.

Cross-Questions

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfProve ItBreak ItScale It

Vacuous Success in SVA Implication
WhyWhy Implication Passes When the Antecedent Is FalseL1 Junior
Why does the language make a |-> b succeed when a is false, instead of failing or skipping it?

Reveal the Model Answer

An attempt starts at every clock tick, so one assertion is evaluated thousands of times. The implication says "whenever a holds, b must follow". A tick without a breaks no promise, so it has to succeed. If it failed instead, the assertion would fire on every idle cycle and be useless.

Self-Check
Tick each key point you covered in your answer.
Key point 1 An attempt starts at every clock tick, so one assertion is evaluated thousands of times. Key point 2 The implication says "whenever a holds, b must follow". Key point 3 A tick without a breaks no promise, so it has to succeed. Key point 4 If it failed instead, the assertion would fire on every idle cycle and be useless.

Misconception

"Implication only starts an attempt when the antecedent is true."

An attempt starts at every tick. On ticks without a match, it ends at once as a vacuous success. That is why the pass count can be huge.

Source IEEE 1800-2017 §16.5, §16.14; Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.) §6.6 p97
- Lesson A1.3Implication and Vacuous Success
What IfAn Antecedent That Starts but Does Not FinishL1 JuniorL2 Mid-Level
What if the antecedent is a ##1 b, and a is seen but b never follows? Is the consequent checked?

Reveal the Model Answer

No. The consequent starts only from an end point of the antecedent. A partial match has no end point, so the attempt ends as a vacuous success. A half-started request therefore counts as a pass. Cover the full antecedent to see whether complete requests happened.

Self-Check
Tick each key point you covered in your answer.
Key point 1 No. Key point 2 The consequent starts only from an end point of the antecedent. Key point 3 A partial match has no end point, so the attempt ends as a vacuous success. Key point 4 A half-started request therefore counts as a pass. Key point 5 Cover the full antecedent to see whether complete requests happened.

Misconception

"Once the antecedent starts, the consequent is checked."

The check waits for the antecedent to match completely. A partial match gives no end point and no check.

Source IEEE 1800-2017 §16.12.7
- Lesson A1.3Implication and Vacuous Success
Prove ItWriting the Cover That Proves an Assertion Checked SomethingL1 JuniorL2 Mid-Level
Write the cover you would add next to assert property (@(posedge clk) disable iff (rst) req |=> ack);.

Reveal the Model Answer

Cover the antecedent with the same clock and reset: cover property (@(posedge clk) disable iff (rst) req);. A nonzero count shows the consequent was checked at least that often. Many teams also cover the whole scenario, req ##1 ack, to show the good path happened.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Cover the antecedent with the same clock and reset: cover property (@(posedge clk) disable iff (rst) req);. Key point 2 A nonzero count shows the consequent was checked at least that often. Key point 3 Many teams also cover the whole scenario, req ##1 ack, to show the good path happened.

Missed Corner

Writes the cover without the assertion's disable iff.

Then it counts req during reset, when the assertion was disabled, and overstates how often the check ran.

Source IEEE 1800-2017 §16.12 (disable iff); Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.) §6.8 p102-104
- Lesson A1.3Implication and Vacuous Success
- Problem 6.6.6Hold the Offer
Prove ItSolve 6.6.6: Hold the OfferSimulator-graded

Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
Open Problem 6.6.6
What IfAn Assertion Under Reset for the Whole TestL2 Mid-Level
Asked if they mention disable iff

What if reset stays asserted for the whole test? What does an assertion with disable iff (rst) report?
systemverilog
```
// rst remains asserted throughout this test.
assert property (@(posedge clk) disable iff (rst) req |=> ack);
```
2:30

You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.

Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
Reveal the Model Answer

Every attempt is disabled, so the assertion reports no passes and no failures. A summary that only lists failures looks clean, which is the same trap as vacuity. An antecedent cover with the same disable iff reads zero and exposes it.

Disabled, Not FailedOne lane per request for disable iff (!rst_n) req |-> ##2 gnt.disable iff (!rst_n) req |-> ##2 gntMeasured on Verilator 5.052: one copy of the assertion per lane

attempt startspassfaildisabled by disable iff

Edge 2 · t=15
A request at 15 waits for gnt two edges later.
Edge 4 · t=35
gnt at 35: the attempt passes.
Edge 5 · t=45
A second request at 45 waits for gnt at 65.
Edge 6 · t=55
Reset arrived at 50, between edges 5 and 6. The attempt from 45 was disabled at that moment, and no verdict is ever reported for it.
Edge 9 · t=85
Reset ended at 70. A request at 85 starts a fresh attempt.
Edge 11 · t=105
No gnt at 105, so this attempt fails. Outside reset the rule still checks everything.

Read the lanes as text
req @15, from edge 2 (t=15): passes at edge 4 (t=35).
req @45, from edge 5 (t=45): is disabled between edges 5 and 6.
req @85, from edge 9 (t=85): fails at edge 11 (t=105).
Sampled values, edge 1 to 11: rst_n 1 1 1 1 1 0 0 1 1 1 1; req 0 1 0 0 1 0 0 0 1 0 0; gnt 0 0 0 1 0 0 0 0 0 0 0.
The program behind the lanes
The lanes come from running this program on Verilator 5.052. Each lane is a separate copy of gnt_in_2 that can start only at that lane's edge, so every verdict and its edge are read from that copy's own output.
module tb; logic clk = 0; always #5 clk = ~clk; // rising edges at 5, 15, 25, ... logic rst_n = 1, req = 0, gnt = 0; gnt_in_2: assert property (@(posedge clk) disable iff (!rst_n) req |-> ##2 gnt); initial begin @(negedge clk); req = 1; // request at 15 @(negedge clk); req = 0; @(negedge clk); gnt = 1; // granted at 35 @(negedge clk); gnt = 0; req = 1; // request at 45 @(negedge clk); req = 0; rst_n = 0; // reset from 50 to 70 @(negedge clk); @(negedge clk); rst_n = 1; @(negedge clk); req = 1; // request at 85 @(negedge clk); req = 0; @(negedge clk); // no grant at 105 @(negedge clk); $finish; end endmodule

Self-Check
Tick each key point you covered in your answer.
Key point 1 Every attempt is disabled, so the assertion reports no passes and no failures. Key point 2 A summary that only lists failures looks clean, which is the same trap as vacuity. Key point 3 An antecedent cover with the same disable iff reads zero and exposes it.
- Lesson A3.5Reset and Abort: disable iff, Accept and Reject
Break ItA Bug That Escapes Through VacuityL2 Mid-Level
Give a real bug that escapes req |=> ack because the assertion passes vacuously.

Reveal the Model Answer

A typical one is a bind mistake: the assertion's req is tied to a signal that never goes high. Every attempt is then vacuous while the real handshake is broken. Another is a test that never reaches the mode where req is raised. Both show up only as an antecedent cover stuck at zero.
Passes with nothing checked
Every edge starts an attempt, and every attempt passes vacuously because no error response ever occurs.

Self-Check
Tick each key point you covered in your answer.
Key point 1 A typical one is a bind mistake: the assertion's req is tied to a signal that never goes high. Key point 2 Every attempt is then vacuous while the real handshake is broken. Key point 3 Another is a test that never reaches the mode where req is raised. Key point 4 Both show up only as an antecedent cover stuck at zero.

Half-Truth

"Vacuity only happens in badly written properties."

A correct property goes vacuous whenever the stimulus or the wiring never produces the antecedent. It is a test and setup problem as often as a property problem.
- Lesson A1.3Implication and Vacuous Success
- Lesson F3.2Over-Constraint and Vacuity
Scale ItAssertion Quality Sign-Off Across an IPL3 SeniorL4 Staff
Your IP has several hundred assertions. How do you show in sign-off that they actually checked something?

Reveal the Model Answer

Pair every implication with an antecedent cover. Make "every antecedent hit in regression" a sign-off item, and review zero-hit covers like failures. In formal, run the covers too, and treat an unreachable antecedent as a vacuous proof. Track the counts per assertion in the verification plan. Then a property that stops firing after a design change is caught.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Pair every implication with an antecedent cover. Key point 2 Make "every antecedent hit in regression" a sign-off item, and review zero-hit covers like failures. Key point 3 In formal, run the covers too, and treat an unreachable antecedent as a vacuous proof. Key point 4 Track the counts per assertion in the verification plan. Key point 5 Then a property that stops firing after a design change is caught.

Misconception

"The formal tool says proven, so the property is meaningful."

A proof can pass because constraints rule out the antecedent. Without a reached cover, proven may mean vacuous.

Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 9 "Vacuity issues" (PDF p310), Tip 9.11 (p318)
- Lesson F3.2Over-Constraint and Vacuity

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Misconception

"No assertion failures means the design does what the property says."

If the antecedent never matched, the consequent was never checked. In the twin, zero failures hide a design that never acks.

Run It

The design never drives ack, and the stimulus never raises req. Does the assertion complain?

RUNVerilator · simulator service

Edit the code, then run it

Expected: assertion failures: 0 antecedent hits: 0 FAIL: no failures, yet ack was never checked once

module tb;
  logic clk = 0, rst = 1, req = 0, ack = 0;
  int fails = 0, hits = 0;
  always #5 clk = ~clk;
  // The bug: nothing ever drives ack.
  a_req_ack: assert property (@(posedge clk) disable iff (rst) req |=> ack) else fails++;
  // Count the clock ticks where the antecedent actually matched.
  always @(posedge clk) if (!rst && req) hits++;
  initial begin
    #12 rst = 0;
    // The belief: no failures means the design is right.
    repeat (10) @(posedge clk);
    $display("assertion failures: %0d", fails);
    $display("antecedent hits: %0d", hits);
    if (fails == 0 && hits == 0) $display("FAIL: no failures, yet ack was never checked once");
    else if (fails > 0) $display("PASS: req fired and the missing ack was caught");
    $finish;
  end
endmodule

See the Fix

module tb;
  logic clk = 0, rst = 1, req = 0, ack = 0;
  int fails = 0, hits = 0;
  always #5 clk = ~clk;
  // The bug: nothing ever drives ack.
  a_req_ack: assert property (@(posedge clk) disable iff (rst) req |=> ack) else fails++;
  // Count the clock ticks where the antecedent actually matched.
  always @(posedge clk) if (!rst && req) hits++;
  initial begin
    #12 rst = 0;
    // The fix: drive the antecedent, and count it, before trusting zero failures.
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    repeat (8) @(posedge clk);
    $display("assertion failures: %0d", fails);
    $display("antecedent hits: %0d", hits);
    if (fails == 0 && hits == 0) $display("FAIL: no failures, yet ack was never checked once");
    else if (fails > 0) $display("PASS: req fired and the missing ack was caught");
    $finish;
  end
endmodule

Prints: assertion failures: 1 antecedent hits: 1 PASS: req fired and the missing ack was caught

Misconception

"Vacuous means the assertion was disabled."

A vacuous attempt is a success, and an assert statement's pass action runs for it. A disabled attempt, from disable iff, is neither a pass nor a failure.

Source IEEE 1800-2017 §16.12.7, §16.14.1, §16.12 (disable iff)

Misconception

"Write req ##0 ack instead of req |-> ack, so it can never pass vacuously."

A sequence used as a property must match from every attempt, and an attempt starts at every tick. That property fails on every tick where req is low.

Source IEEE 1800-2017 §16.12.2; Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.) §17.16 p285

Delivery

Explains vacuity correctly but never proposes how to detect it.

The follow-up is always "so what do you do about it?". A pass names the cover, or the tool's vacuity report.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

Vacuous Success in SVA Implication

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It