Goto Repetition vs Non-Consecutive Repetition

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

WhyWhat IfCompareScale It

1. Goto Repetition vs Non-Consecutive Repetition
2. WhyWhy Wait-for-Next Uses Goto OneL1 Junior

   Why do so many protocol rules contain gnt[->1]?

   Reveal the Model Answer

   gnt[->1] matches at the next edge where gnt is true, however long that takes, and ends exactly there. That is the shape of "until the grant arrives", so req throughout gnt[->1] reads as "req stays high until the next grant, inclusive".

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 gnt[->1] matches at the next edge where gnt is true, however long that takes, and ends exactly there. Key point 2 That is the shape of "until the grant arrives", so req throughout gnt[->1] reads as "req stays high until the next grant, inclusive".

   Misconception

   "gnt[->1] is the same as ##1 gnt."

   ##1 gnt checks one specific edge; gnt[->1] waits any number of edges for the first gnt, starting with the current edge.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8.13 (PDF p158)

   • Lesson A3.2Holding Until an Event: Until and Throughout
3. What IfA Grant in the Same Cycle as the RequestL1 JuniorL2 Mid-Level

   What if the grant can arrive in the same cycle as the request? How do |-> and |=> differ here?

   Reveal the Model Answer

   gnt[->1] can match at the very first tick, if gnt is already true there. So req |-> req throughout gnt[->1] passes in one cycle when the grant is immediate. With |=>, the check starts one tick later and misses that grant. It then waits for the next grant, which may belong to another transfer.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 gnt[->1] can match at the very first tick, if gnt is already true there. Key point 2 So req |-> req throughout gnt[->1] passes in one cycle when the grant is immediate. Key point 3 With |=>, the check starts one tick later and misses that grant. Key point 4 It then waits for the next grant, which may belong to another transfer.

   Misconception

   "gnt[->1] always waits at least one cycle."

   It matches at the first tick where gnt is true, which can be the tick where it starts.

   Source IEEE 1800-2017 §16.9.2

   • Lesson A3.2Holding Until an Event: Until and Throughout
4. CompareGoto Alone vs Throughout a GotoL2 Mid-Level

   Compare $rose(req) |-> gnt[->1] with $rose(req) |-> req throughout gnt[->1].

   Reveal the Model Answer

   The first only says a grant comes at some point. It is weak under assert, so it never fails if no grant arrives. The second also demands req at every edge up to and including the grant. So a request dropped early fails at once. The second shape is also one of the few goto forms Verilator 5.052 evaluates correctly.

   	$rose(req) |-> gnt[->1]	$rose(req) |-> req throughout gnt[->1]
   A grant comes	Pass	Pass, if req held until the grant
   req drops early	Not checked	Fails at once
   No grant ever comes	No failure: weak	No failure: weak

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The first only says a grant comes at some point. Key point 2 It is weak under assert, so it never fails if no grant arrives. Key point 3 The second also demands req at every edge up to and including the grant. Key point 4 So a request dropped early fails at once. Key point 5 The second shape is also one of the few goto forms Verilator 5.052 evaluates correctly.

   Missed Corner

   "The first one fails at the end of the test if no grant came."

   A goto in an asserted property is weak by default, so an attempt still waiting at the end is not a failure. A strong form is needed for that.

   Source IEEE 1800-2017 §16.12.2

   • Lesson A3.2Holding Until an Event: Until and Throughout
5. Scale ItA Team Policy for Constructs Tools Disagree OnL3 SeniorL4 Staff

   Your simulator and your formal tool disagree on some sequence operators. How do you keep a shared assertion library trustworthy?

   Reveal the Model Answer

   Probe each operator on every tool with one property that must fail and one that must pass. Record which forms give the standard verdict. Allow only that subset in shared checkers, and enforce it with a lint rule. Rewrite the rest with auxiliary logic or simpler forms. Re-run the probes whenever a tool version changes.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Probe each operator on every tool with one property that must fail and one that must pass. Key point 2 Record which forms give the standard verdict. Key point 3 Allow only that subset in shared checkers, and enforce it with a lint rule. Key point 4 Rewrite the rest with auxiliary logic or simpler forms. Key point 5 Re-run the probes whenever a tool version changes.

   What Interviewers Listen For (Staff)

   A good staff answer treats the supported subset as a versioned list with tests that must fail. A methodology team owns it and measures it again on every tool upgrade.

   Tool as Truth

   "If the vendor documents the operator, it works."

   Silent misbehaviour is the dangerous case: a tool that compiles a construct and never reports its failure passes every test.

   Source ASIC Point engine notes (Verilator 5.052 SVA probes)

   • Lesson A8.1Capstone: An Assertion Suite
6. What IfA Range of Non-Consecutive OccurrencesL2 Mid-Level

   What if the spec allows two to three acks before done, not exactly two?

   Reveal the Model Answer

   Write ack[=2:3] ##1 done: between two and three occurrences of ack, with any idle edges, and done after them while no further ack appears. Remember that the property passes at its first match, so a fourth ack before done needs its own rule.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Write ack[=2:3] ##1 done: between two and three occurrences of ack, with any idle edges, and done after them while no further ack appears. Key point 2 Remember that the property passes at its first match, so a fourth ack before done needs its own rule.

   Missed Corner

   "ack[=2:3] fails if a fourth ack arrives."

   The match can end after the second or third ack. Anything later belongs to the rest of the sequence, or to another rule.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8.11 (PDF p155)

   • Lesson A2.2Repetition and Counting Events