What the End of a Test Means for an Assertion

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

WhyProve ItBreak ItCompareScale It

1. What the End of a Test Means for an Assertion
2. WhyWhy Assertions Are Weak by DefaultL2 Mid-Level

   Why did the standard make sequences weak by default in assertions?

   Reveal the Model Answer

   Every test ends at some point, usually with traffic still in flight. If open attempts failed by default, almost every test would end with false failures. Weak by default means "no bad thing seen so far". You ask for strong, end-of-test failures only where you mean them.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Every test ends at some point, usually with traffic still in flight. Key point 2 If open attempts failed by default, almost every test would end with false failures. Key point 3 Weak by default means "no bad thing seen so far". Key point 4 You ask for strong, end-of-test failures only where you mean them.

   Misconception

   "Weak means the assertion is less strict on every cycle."

   Weak and strong differ only for attempts still open when the test ends. On every completed attempt they give the same verdict.

   Source IEEE 1800-2017 §16.12.2

   • Lesson A3.1Weak and Strong: What the End of a Test Means
3. Break ItThe Hang a Weak Property HidesL2 Mid-Level

   Break it: which bug can a weak req |-> ##[1:$] ack hide completely?

   Reveal the Model Answer

   A hang. If ack never comes, the weak attempt is still pending at the end and does not fail. The log shows no failure, even though the design locked up. Catch it with a bounded window, a strong form, or an end-of-test check that no request is outstanding.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 A hang. Key point 2 If ack never comes, the weak attempt is still pending at the end and does not fail. Key point 3 The log shows no failure, even though the design locked up. Key point 4 Catch it with a bounded window, a strong form, or an end-of-test check that no request is outstanding.

   Tool as Truth

   "No assertion failed, so nothing hung."

   Weak unbounded properties never fail on a hang. Only a bound, a strong form or an end-of-test check reports it.

   Source IEEE 1800-2017 §16.12.2

   • Lesson A3.1Weak and Strong: What the End of a Test Means
4. CompareA Spec Bound vs EventuallyL2 Mid-LevelL3 Senior

   Compare req |-> ##[1:16] ack with req |-> s_eventually ack.

   Reveal the Model Answer

   The bounded form fails at cycle 16 of the attempt, right where the promise breaks, and it stops tracking the attempt there. s_eventually cannot fail until the test ends, so the failure shows up far from its cause. Use the bound whenever the spec gives one. Keep s_eventually for rules that truly have no limit.

   attempt startspassfailstill running at the end: weak, no failurethread dies; the attempt goes onthread dropped: the attempt has already passed

   1. Edge 2 · t=15

      The request at 15 forks four threads, one per delay of ##[1:4].

   2. Edge 4 · t=35

      ack at 35 ends the attempt with a pass. The longer threads stop looking.

   3. Edge 5 · t=45

      The DUT drops the request at 45. Its four threads start waiting.

   4. Edge 9 · t=85

      At 85 the last thread runs out of window, so the dropped request fails here.

   5. Edge 11 · t=105

      A legal request at 105. Its answer is due at 125.

   6. End of the run · t=120

      The test stops at 120 with three threads still open. The consequent is weak, so this request ends with no verdict: it was never checked.

   Read the lanes as text

   • req @15, from edge 2 (t=15): thread 1 (to edge 3 (t=25)) dies at edge 3 (t=25); thread 2 (to edge 4 (t=35)) passes at edge 4 (t=35); thread 3 (to edge 5 (t=45)) is dropped at edge 4 (t=35), because the attempt has already passed; thread 4 (to edge 6 (t=55)) is dropped at edge 4 (t=35), because the attempt has already passed.
   • req @45, from edge 5 (t=45): thread 1 (to edge 6 (t=55)) dies at edge 6 (t=55); thread 2 (to edge 7 (t=65)) dies at edge 7 (t=65); thread 3 (to edge 8 (t=75)) dies at edge 8 (t=75); thread 4 (to edge 9 (t=85)) fails at edge 9 (t=85).
   • req @105, from edge 11 (t=105): thread 1 (to edge 12 (t=115)) dies at edge 12 (t=115); thread 2 (to the end of the run (t=120)) is still running at the end of the run: weak, so no failure; thread 3 (to the end of the run (t=120)) is still running at the end of the run: weak, so no failure; thread 4 (to the end of the run (t=120)) is still running at the end of the run: weak, so no failure.

   Sampled values, edge 1 to 12: req 0 1 0 0 1 0 0 0 0 0 1 0; ack 0 0 0 1 0 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 ack_within_4 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, ack = 0;
   
     ack_within_4: assert property (@(posedge clk) req |-> ##[1:4] ack);
   
     initial begin
       @(negedge clk); req = 1;            // request at 15
       @(negedge clk); req = 0;
       @(negedge clk); ack = 1;            // answered at 35
       @(negedge clk); ack = 0; req = 1;   // request at 45: the DUT drops it
       @(negedge clk); req = 0;
       repeat (5) @(negedge clk);
       req = 1;                            // request at 105, legal, answer due at 125
       @(negedge clk); req = 0;
       @(negedge clk);
       $finish;                            // the test stops at 120
     end
   endmodule
   

   attempt startspassstill running at the end: strong, fails

   1. Edge 2 · t=15

      The request at 15 starts waiting for ack, with no deadline.

   2. Edge 4 · t=35

      It passes at 35.

   3. Edge 5 · t=45

      The dropped request starts waiting. Nothing in this run will end the wait.

   4. Edge 11 · t=105

      The legal request at 105 starts waiting too.

   5. End of the run · t=120

      Both waits are still open at 120, and both fail there. A strong rule cannot tell a lost request from one in flight.

   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 still running at the end of the run: strong, so it fails.
   • req @105, from edge 11 (t=105): is still running at the end of the run: strong, so it fails.

   Sampled values, edge 1 to 12: req 0 1 0 0 1 0 0 0 0 0 1 0; ack 0 0 0 1 0 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 ack_some_time 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, ack = 0;
   
     ack_some_time: assert property (@(posedge clk) req |-> s_eventually ack);
   
     initial begin
       @(negedge clk); req = 1;            // request at 15
       @(negedge clk); req = 0;
       @(negedge clk); ack = 1;            // answered at 35
       @(negedge clk); ack = 0; req = 1;   // request at 45: the DUT drops it
       @(negedge clk); req = 0;
       repeat (5) @(negedge clk);
       req = 1;                            // request at 105, legal, answer due at 125
       @(negedge clk); req = 0;
       @(negedge clk);
       $finish;                            // the test stops at 120
     end
   endmodule
   

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The bounded form fails at cycle 16 of the attempt, right where the promise breaks, and it stops tracking the attempt there. Key point 2 s_eventually cannot fail until the test ends, so the failure shows up far from its cause. Key point 3 Use the bound whenever the spec gives one. Key point 4 Keep s_eventually for rules that truly have no limit.

   Half-Truth

   "A bound is a guess; eventually is the real rule."

   Most specs and performance targets do give a bound. Checking it is stronger and gives a failure at the right cycle.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §20.1

   • Lesson A2.1Delays and Ranges: One Attempt, Many Threads
   • Lesson A3.1Weak and Strong: What the End of a Test Means
   • Problem 6.6.8Answer in Time
5. Break ItA Strong Property That Failed a Good DesignL2 Mid-Level

   How can a strong property fail on a correct design?

   Reveal the Model Answer

   The test stops while a legal request is still waiting for its answer. The strong attempt is still open at the end, so it fails, although the design would have answered one cycle later. Drain the test: stop new traffic, wait for outstanding responses, and only then call $finish.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The test stops while a legal request is still waiting for its answer. Key point 2 The strong attempt is still open at the end, so it fails, although the design would have answered one cycle later. Key point 3 Drain the test: stop new traffic, wait for outstanding responses, and only then call $finish.

   Half-Truth

   "Make the test longer."

   A longer test still stops with traffic in flight unless it drains. The fix is to stop sending, then wait for responses.

   • Lesson A3.1Weak and Strong: What the End of a Test Means
   • Lesson 7.7Capstone: The Complete Layered Testbench
   • Problem 7.7.3Premature Test Completion
6. Scale ItLiveness in Simulation and in FormalL3 Senior

   Your team wants to sign off "every request is eventually answered". How do simulation and formal each contribute?

   Reveal the Model Answer

   Simulation checks the bounded version on real traffic, and the strong version flags requests left open at the end of each test. Formal can prove the unbounded property over all input sequences. It usually needs fairness assumptions, such as "the downstream eventually accepts". Review those assumptions carefully, because a wrong one makes the proof empty.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Simulation checks the bounded version on real traffic, and the strong version flags requests left open at the end of each test. Key point 2 Formal can prove the unbounded property over all input sequences. Key point 3 It usually needs fairness assumptions, such as "the downstream eventually accepts". Key point 4 Review those assumptions carefully, because a wrong one makes the proof empty.

   What Interviewers Listen For (Senior)

   A good senior answer splits the claim between bounded checks in simulation and a liveness proof in formal. It names the fairness assumption that the proof depends on.

   Wrong Altitude

   "Long random simulation proves the liveness property."

   Simulation only shows the rule held in the traces run. Only formal covers all traces, and only under its assumptions.

   • Lesson F8.2An Arbiter: Exclusion, Rotation and Fairness
7. Prove ItSolve 6.6.8: Answer in TimeSimulator-graded

   Show it, don't just say it: this Silicon Lab problem is graded by the simulator.

   Open Problem 6.6.8