Sequence Operators: AND, OR, Intersect, Within

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

WhyWhat IfProve ItCompareScale It

1. Sequence Operators: AND, OR, Intersect, Within
2. WhyUsing Intersect to Bound a LengthL2 Mid-LevelL3 Senior

   Why would you intersect a sequence with 1[*1:8]?

   Reveal the Model Answer

   1[*1:8] matches every length from one to eight edges and constrains nothing else. Intersecting with it keeps only the matches of the other sequence that finish within eight edges. It is a compact way to bound something like req ##1 ack[->1], whose goto could otherwise wait forever.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 1[*1:8] matches every length from one to eight edges and constrains nothing else. Key point 2 Intersecting with it keeps only the matches of the other sequence that finish within eight edges. Key point 3 It is a compact way to bound something like req ##1 ack[->1], whose goto could otherwise wait forever.

   Misconception

   "Intersecting with 1[*1:8] delays the sequence by eight cycles."

   It filters matches by length; it adds no delay.

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

   • Lesson A2.1Delays and Ranges: One Attempt, Many Threads
3. What IfAn Intersect That Never MatchesL2 Mid-LevelL3 Senior

   What if the other sequence has no match shorter than 8 edges? What does the intersect give?

   Reveal the Model Answer

   No match at all, because intersect needs both sequences to match with the same start and end. In an antecedent, the property then never triggers and passes vacuously. In a consequent, every attempt fails. Cover the intersected sequence, so you see that it can match.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 No match at all, because intersect needs both sequences to match with the same start and end. Key point 2 In an antecedent, the property then never triggers and passes vacuously. Key point 3 In a consequent, every attempt fails. Key point 4 Cover the intersected sequence, so you see that it can match.

   Half-Truth

   "Intersect only removes long matches, so it can only remove failures."

   It removes matches. In a consequent, losing every match turns the attempt into a failure.

   • Lesson A2.1Delays and Ranges: One Attempt, Many Threads
4. CompareOne Sequence AND vs Two AssertionsL2 Mid-Level

   Compare req |-> (##1 ack) and (##3 status) with two assertions req |-> ##1 ack and req |-> ##3 status.

   Reveal the Model Answer

   As verdicts on each request they agree: both obligations must hold. The single property gives the conjunction an end point, so you can follow it with ##1 done measured from the later operand. Two assertions report separately, which makes the failing half obvious in the log. Prefer separate assertions unless something must follow the combined end.

   attempt startspassfail

   1. Edge 2 · t=15

      A request at 15 starts both operands at once: ack is due at 25 and stat at 45.

   2. Edge 6 · t=55

      ack came at 25 and stat at 45, so the and ends at 45. done at 55 completes the attempt, which passes.

   3. Edge 9 · t=85

      The second request has ack at 75. done arrives at 85, one edge after ack, but the and has not ended yet, so this done counts for nothing.

   4. Edge 11 · t=105

      stat came at 95, so done was due at 105. It is low, and the attempt fails.

      More context

      done one edge after the earlier operand is not enough. What follows an and is measured from its later end.

   5. Edge 13 · t=125

      The third request has no ack at 125. One operand failed, so the and cannot match, and the attempt fails at once, without waiting for stat.

   Read the lanes as text

   • req @15, from edge 2 (t=15): passes at edge 6 (t=55).
   • req @65, from edge 7 (t=65): fails at edge 11 (t=105).
   • req @115, from edge 12 (t=115): fails at edge 13 (t=125).

   Sampled values, edge 1 to 15: req 0 1 0 0 0 0 1 0 0 0 0 1 0 0 0; ack 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0; stat 0 0 0 0 1 0 0 0 0 1 0 0 0 0 1; done 0 0 0 0 0 1 0 0 1 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 both_then_done 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, stat = 0, done = 0;
   
     both_then_done: assert property (@(posedge clk) req |-> ((##1 ack) and (##3 stat)) ##1 done);
   
     initial begin
       @(negedge clk); req = 1;                     // request at 15
       @(negedge clk); req = 0; ack = 1;            // ack at 25
       @(negedge clk); ack = 0;
       @(negedge clk); stat = 1;                    // stat at 45
       @(negedge clk); stat = 0; done = 1;          // done at 55: in time
       @(negedge clk); done = 0; req = 1;           // request at 65
       @(negedge clk); req = 0; ack = 1;            // ack at 75
       @(negedge clk); ack = 0; done = 1;           // done at 85: too early
       @(negedge clk); done = 0; stat = 1;          // stat at 95
       @(negedge clk); stat = 0;                    // no done at 105
       @(negedge clk); req = 1;                     // request at 115
       @(negedge clk); req = 0;                     // no ack at 125
       @(negedge clk);
       @(negedge clk); stat = 1;                    // stat at 145
       @(negedge clk); stat = 0;
       $finish;
     end
   endmodule
   

   Both operands start together. The attempt fails as soon as either operand fails, or when what follows the later end fails.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 As verdicts on each request they agree: both obligations must hold. Key point 2 The single property gives the conjunction an end point, so you can follow it with ##1 done measured from the later operand. Key point 3 Two assertions report separately, which makes the failing half obvious in the log. Key point 4 Prefer separate assertions unless something must follow the combined end.

   Half-Truth

   "One failure of the and means both halves failed."

   The and fails if either operand fails; the report does not say which. Verilator 5.052 even reports one attempt twice when both fail.

   Source ASIC Point engine notes (Verilator 5.052 SVA probes), "Failing cases of the §7 forms" (and row)

   • Lesson A2.1Delays and Ranges: One Attempt, Many Threads
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. Prove ItWriting a Within Rule for a BurstL2 Mid-Level

   Write a property: after start, exactly one err_irq pulse must occur somewhere during the burst, which lasts until last, inclusive.

   Reveal the Model Answer

   Count instead of combining sequences. A counter clears at start and adds err_irq while the burst is open. Then last |-> err_cnt + err_irq == 1 checks the total on the last beat. A pure-SVA form built from err_irq[=1] and within a burst sequence is legal but hard to read. On Verilator 5.052 it also uses two constructs that engine cannot run, while the counter runs everywhere and shows up in the waveform.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Count instead of combining sequences. Key point 2 A counter clears at start and adds err_irq while the burst is open. Key point 3 Then last |-> err_cnt + err_irq == 1 checks the total on the last beat. Key point 4 A pure-SVA form built from err_irq[=1] and within a burst sequence is legal but hard to read. Key point 5 On Verilator 5.052 it also uses two constructs that engine cannot run, while the counter runs everywhere and shows up in the waveform.

   Missed Corner

   Writes start |-> ##[1:$] err_irq ##[1:$] last.

   That allows any number of extra pulses and is unbounded twice; it checks ordering, not "exactly one".

   Source IEEE 1800-2017 §16.9.10

   • Lesson A2.2Repetition and Counting Events
   • Lesson A8.1Capstone: An Assertion Suite