Until or Until With: Who Owns the Last Cycle?

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

WhyWhat IfProve ItBreak ItCompare

1. Until or Until With: Who Owns the Last Cycle?
2. CompareUntil_with vs Throughout a GotoL2 Mid-Level

   Compare req until_with gnt with req throughout gnt[->1].

   Reveal the Model Answer

   They give the same verdict when the grant comes: req must hold at every edge up to and including the first gnt. The difference is what they are. until_with is a property operator, so nothing can follow it in a sequence. throughout builds a sequence that you can extend or use in a cover. If the grant never arrives, both are weak and do not fail.

   	req until_with gnt	req throughout gnt[->1]
   Verdict when the grant comes	Same	Same
   What it builds	A property	A sequence with an end point
   Can be followed by more sequence	No	Yes
   Grant never comes	Weak: no failure	Weak: no failure

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 They give the same verdict when the grant comes: req must hold at every edge up to and including the first gnt. Key point 2 The difference is what they are. Key point 3 until_with is a property operator, so nothing can follow it in a sequence. Key point 4 throughout builds a sequence that you can extend or use in a cover. Key point 5 If the grant never arrives, both are weak and do not fail.

   Misconception

   "Throughout checks the condition only at the start and end."

   It requires the condition at every tick of the sequence's match.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8.16 (PDF p161-163)

   • Lesson A3.2Holding Until an Event: Until and Throughout
3. Break ItA Throughout That Stopped FailingL2 Mid-LevelL3 Senior

   You extended a working rule to (req throughout gnt[->1]) ##1 done, and now it never fails, even when you remove done from the design. Is the rule wrong?

   // passes on a design that never drives done
   a_req: assert property (@(posedge clk)
     $rose(req) |-> (req throughout gnt[->1]) ##1 done) else errors++;

   Reveal the Model Answer

   The rule is legal and should fail one edge after the grant when done is missing. Verilator 5.052 reports no failure for a throughout over a goto followed by more sequence, so the silence is the tool. Split it: keep req throughout gnt[->1] as the whole consequent, and add gnt |=> done as a second assertion.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The rule is legal and should fail one edge after the grant when done is missing. Key point 2 Verilator 5.052 reports no failure for a throughout over a goto followed by more sequence, so the silence is the tool. Key point 3 Split it: keep req throughout gnt[->1] as the whole consequent, and add gnt |=> done as a second assertion.

   Tool as Truth

   "It passed after the edit, so the design drives done correctly."

   The design never drives done at all. A rule that cannot fail on a broken design is broken evidence; always rerun a must-fail case after editing a property.

   Source ASIC Point engine notes (Verilator 5.052 SVA probes), "A3/A5 forms" ((v throughout r[->1]) ##1 done row)

   • Lesson A3.2Holding Until an Event: Until and Throughout
4. What IfA Grant That Never CameL2 Mid-Level

   What if the grant never arrives before the test ends? What do until, until_with and s_until report?

   Reveal the Model Answer

   The weak forms report nothing: an attempt still waiting at the end of simulation is not a failure. s_until is strong, so the open attempt fails at the end of simulation. Use the strong form when "the grant must come" is part of the rule. Make tests drain traffic before they stop, or legal stimulus fails it too.

   attempt startsfailstill running at the end: weak, no failure

   1. Edge 2 · t=15

      A starts at 15 with v high.

   2. Edge 4 · t=35

      At 35 r arrives, and until_with needs v on this edge as well. v is low, so A fails.

   3. Edge 6 · t=55

      B starts with r high, so its first edge is also its last. v is low there: B fails.

   4. End of the run · t=100

      C is still waiting at the end. until_with is weak too, so no verdict.

   Read the lanes as text

   • start @15, from edge 2 (t=15): fails at edge 4 (t=35).
   • start @55, from edge 6 (t=55): fails at edge 6 (t=55).
   • start @75, from edge 8 (t=75): is still running at the end of the run: weak, so no failure.

   Sampled values, edge 1 to 10: start 0 1 0 0 0 1 0 1 0 0; v 0 1 1 0 0 0 0 1 1 1; r 0 0 0 1 0 1 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 hold_until_with 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 start = 0, v = 0, r = 0;
   
     hold_until_with: assert property (@(posedge clk) start |-> v until_with r);
   
     initial begin
       @(negedge clk); start = 1; v = 1;   // A starts at 15
       @(negedge clk); start = 0;
       @(negedge clk); v = 0; r = 1;       // r at 35, v already low
       @(negedge clk); r = 0;
       @(negedge clk); start = 1; r = 1;   // B starts at 55 with r already high
       @(negedge clk); start = 0; r = 0;
       @(negedge clk); start = 1; v = 1;   // C starts at 75; r never comes
       @(negedge clk); start = 0;
       @(negedge clk);
       @(negedge clk);
       $finish;                            // the test stops at 100
     end
   endmodule
   

   The weak form leaves attempt C with no verdict. The strong form, s_until_with, would fail it at the end.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The weak forms report nothing: an attempt still waiting at the end of simulation is not a failure. Key point 2 s_until is strong, so the open attempt fails at the end of simulation. Key point 3 Use the strong form when "the grant must come" is part of the rule. Key point 4 Make tests drain traffic before they stop, or legal stimulus fails it too.

   Misconception

   "Strong operators are only for formal."

   Simulators evaluate them too: a strong obligation still open when simulation ends is reported as a failure.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §20.11 (PDF p325-328)

   • Lesson A3.1Weak and Strong: What the End of a Test Means
5. WhyWhy Nothing Can Follow an UntilL2 Mid-Level

   Why can't you write (req until gnt) ##1 done?

   Reveal the Model Answer

   until produces a property, a verdict over time, not a sequence with an end point, and ## concatenates sequences. Some tools accept the expression anyway, Verilator 5.052 among them, which makes it easy to ship illegal code. Use req throughout gnt[->1] when you need a sequence with an end point.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 until produces a property, a verdict over time, not a sequence with an end point, and ## concatenates sequences. Key point 2 Some tools accept the expression anyway, Verilator 5.052 among them, which makes it easy to ship illegal code. Key point 3 Use req throughout gnt[->1] when you need a sequence with an end point.

   Tool as Truth

   "It compiled, so it is legal."

   Verilator 5.052 compiles (v until r) ##1 done although until is not a sequence operator in the standard.

   Source ASIC Point engine notes (Verilator 5.052 SVA probes), "A3/A5 forms" ((v until r) ##1 done row)

   • Lesson A3.2Holding Until an Event: Until and Throughout
6. 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