Interview Question · Code Reading

The Busy Signal That Lasted Too Long

L1 JuniorL2 Mid-Levelsvasequencesrepetition

The interviewer asks

The spec says that after req, busy is high for two to four consecutive cycles and then drops. Does this assertion catch a busy that lasts five cycles?

systemverilog

// Spec: after req, busy is high for 2 to 4 consecutive cycles, then drops.
a_busy: assert property (@(posedge clk) req |=> busy[*2:4]) else errors++;

Reveal the Model Answer

No. busy[*2:4] is a sequence that matches as soon as busy has been high for two cycles. An implication passes at the first match of its consequent. Nothing after that match is checked, so a five-cycle busy passes. The upper bound needs its own check, such as req ##1 busy[*4] |=> !busy: after four cycles of busy, the next must be low.

Four Edges of Busy, Then It Must DropOne lane per starting edge for busy[*4] |=> !busy, on a stretch of six busy edges from 25 to 75.busy[*4] |=> !busyMeasured on Verilator 5.052: one copy of the assertion per lane

attempt startspassfail

Edge 3 · t=25
busy rises at 25, and an attempt starts matching four edges of it: 25, 35, 45 and 55.
Edge 6 · t=55
Four attempts are in flight, from 25, 35, 45 and 55; the figure follows the first three.
Edge 7 · t=65
The attempt from 25 has seen four edges of busy, so busy must be low at 65. It is high, and that attempt fails.
Edge 8 · t=75
The attempt from 35 fails at 75 for the same reason: the fifth and sixth edges each add one failure.
Edge 9 · t=85
busy drops at 85, and the attempt from 45 passes there. Attempts from later edges never see four edges of busy, so they succeed vacuously.
More context
A stretch of six busy edges gives two failures. Debug from the first one; the second reports the same stretch.

Read the lanes as text

from @25, from edge 3 (t=25): fails at edge 7 (t=65).
from @35, from edge 4 (t=35): fails at edge 8 (t=75).
from @45, from edge 5 (t=45): passes at edge 9 (t=85).

Sampled values, edge 1 to 13: busy 0 0 1 1 1 1 1 1 0 0 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 at_most_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, busy = 0;

  at_most_4: assert property (@(posedge clk) busy[*4] |=> !busy);

  initial begin
    @(negedge clk); req = 1;            // request sampled at 15
    @(negedge clk); req = 0; busy = 1;  // busy sampled at 25, 35, ... 75
    repeat (6) @(negedge clk);
    busy = 0;
    @(negedge clk); req = 1;            // request sampled at 95
    @(negedge clk); req = 0; busy = 1;  // busy only at 105
    @(negedge clk); busy = 0;
    repeat (2) @(negedge clk);          // edges at 115 and 125
    $finish;
  end
endmodule

One failure per edge beyond the limit, and a pass for the attempt whose fourth edge is the last one.

The lower-bound rule and the upper-bound rule against bursts of 1, 3, 4 and 5 cycles.

RUNVerilator · simulator service

Edit the code, then run it

Expected: busy for 1: lower-bound failures=1 upper-bound failures=0 busy for 3: lower-bound failures=0 upper-bound failures=0 busy for 4: lower-bound failures=0 upper-bound failures=0 busy for 5: lower-bound failures=0 upper-bound failures=1

module tb;
  logic clk = 0, req = 0, busy = 0;
  int f_min = 0, f_max = 0;
  always #5 clk = ~clk;
  a_min: assert property (@(posedge clk) req |=> busy[*2:4]) else f_min++;
  a_max: assert property (@(posedge clk) req ##1 busy[*4] |=> !busy) else f_max++;
  task automatic burst(int n);          // one request, then busy for n cycles
    @(negedge clk) req = 1;
    @(negedge clk) begin req = 0; busy = 1; end
    repeat (n - 1) @(negedge clk);
    @(negedge clk) busy = 0;
    repeat (3) @(negedge clk);
    $display("busy for %0d: lower-bound failures=%0d upper-bound failures=%0d", n, f_min, f_max);
    f_min = 0; f_max = 0;
  endtask
  initial begin
    burst(1); burst(3); burst(4); burst(5);
    $finish;
  end
endmodule

Self-Check

Tick each key point you covered in your answer.

Key point 1 No. Key point 2 busy[*2:4] is a sequence that matches as soon as busy has been high for two cycles. Key point 3 An implication passes at the first match of its consequent. Key point 4 Nothing after that match is checked, so a five-cycle busy passes. Key point 5 The upper bound needs its own check, such as req ##1 busy[*4] |=> !busy: after four cycles of busy, the next must be low.

What Interviewers Listen For (Junior)

A good junior answer says the property already passes after two cycles of busy. It proposes a separate check for the maximum.

Cross-Questions

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

WhyWhat IfProve ItCompareScale It

The Busy Signal That Lasted Too Long
WhyWhy One Match Ends the AttemptL1 Junior
Why does the implication stop at the first match of busy[*2:4] instead of checking the longest one?

Reveal the Model Answer

A property built from a sequence asks whether the sequence can match. The implication succeeds as soon as one consequent match exists. Longer matches add nothing to that answer. Anything that must happen after the match has to be written as more sequence or as a separate rule.

Self-Check
Tick each key point you covered in your answer.
Key point 1 A property built from a sequence asks whether the sequence can match. Key point 2 The implication succeeds as soon as one consequent match exists. Key point 3 Longer matches add nothing to that answer. Key point 4 Anything that must happen after the match has to be written as more sequence or as a separate rule.

Misconception

"The simulator picks the longest match, like a greedy regular expression."

There is no greedy choice; the property holds if any match exists, and the earliest one already proves it.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8.8 (PDF p142)
- Lesson A2.2Repetition and Counting Events

CompareRepetition Operators vs an Auxiliary CounterL2 Mid-Level

Compare checking a length bound with repetition operators and with a small counter in the checker plus a plain implication.

Reveal the Model Answer

Repetition keeps the rule in one line and is natural for short, fixed bounds. A counter can count up while busy is high and clear when it drops. Then any bound becomes a one-edge check such as busy |-> busy_len <= 4. It is easy to debug in a waveform and costs nothing per attempt. For long or parameterised bounds, the counter is usually clearer and cheaper.

	Repetition operator	Counter plus one-edge check
Code	`busy[*2:4]` in one line	A few lines of helper logic
In a waveform	Nothing to look at	The count is a visible signal
Cost	Threads for each open attempt	One check per edge
Best for	Short, fixed bounds	Long or parameterised bounds

Self-Check

Tick each key point you covered in your answer.

Key point 1 Repetition keeps the rule in one line and is natural for short, fixed bounds. Key point 2 A counter can count up while busy is high and clear when it drops. Key point 3 Then any bound becomes a one-edge check such as busy |-> busy_len <= 4. Key point 4 It is easy to debug in a waveform and costs nothing per attempt. Key point 5 For long or parameterised bounds, the counter is usually clearer and cheaper.

Misconception

"Auxiliary logic in a checker is cheating; real SVA uses only operators."

Modelling code beside properties is a standard technique, especially for counts and data that operators express badly.

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

Scale ItThe Cost of a Thousand-Cycle RepetitionL3 Senior
A timeout rule says busy must drop within 1000 cycles. Why is busy[*1:1000] a poor way to write it, in simulation and in formal?

Reveal the Model Answer

In simulation, every cycle of busy can start an attempt, and each one stays open for up to 1000 edges. A long busy period then holds hundreds of open attempts. In formal, a deep bound makes the property expensive and may keep it from converging. A counter that stops at the limit makes it a one-edge check in both. The limit becomes a parameter that tests can shrink.

Self-Check
Tick each key point you covered in your answer.
Key point 1 In simulation, every cycle of busy can start an attempt, and each one stays open for up to 1000 edges. Key point 2 A long busy period then holds hundreds of open attempts. Key point 3 In formal, a deep bound makes the property expensive and may keep it from converging. Key point 4 A counter that stops at the limit makes it a one-edge check in both. Key point 5 The limit becomes a parameter that tests can shrink.

What Interviewers Listen For (Senior)
A good senior answer names the cost of one thread per open attempt. It prefers a counter with a limit parameter, and shrinks that parameter for formal and short tests.

Half-Truth

"Bounded is always cheap; only $ is expensive."

A bound of 1000 behaves like an unbounded range for cost when attempts overlap; what matters is how many threads stay open.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §20.1 (PDF p309)
- Lesson A3.1Weak and Strong: What the End of a Test Means
- Lesson F4.5Counter, Memory and Parameter Abstraction
What IfA Repetition That Can Match Zero TimesL2 Mid-Level
What if the range starts at zero, as in req |=> busy[*0:4] ##1 done?

Reveal the Model Answer

busy[*0] is an empty match, so one legal reading is req |=> done with no busy at all. Empty matches make the timing hard to read. The ##1 after an empty sequence does not add a cycle the way it seems to. Write the zero case as its own alternative, or avoid it.

Self-Check
Tick each key point you covered in your answer.
Key point 1 busy[*0] is an empty match, so one legal reading is req |=> done with no busy at all. Key point 2 Empty matches make the timing hard to read. Key point 3 The ##1 after an empty sequence does not add a cycle the way it seems to. Key point 4 Write the zero case as its own alternative, or avoid it.

Missed Corner

"[*0] means busy must be low for zero cycles, so it is a no-op."

It is an empty sequence, and concatenating with an empty sequence changes the delay arithmetic around it.

Source IEEE 1800-2017 §16.9.2
- Lesson A2.2Repetition and Counting Events
Prove ItSolve 6.6.7: Count the BeatsSimulator-graded

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

What People Get Wrong

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

Misconception

"busy[*2:4] fails when busy lasts more than four cycles."

The repetition matches at two cycles and the attempt is over. The twin's five-cycle busy reports zero failures until the upper-bound rule is added.

Run It

One request, then busy for five cycles.

RUNVerilator · simulator service

Edit the code, then run it

Expected: failures=0 FAIL: busy[*2:4] matched after two cycles, so a five-cycle busy passed

module tb;
  logic clk = 0, req = 0, busy = 0;
  int fails = 0;
  always #5 clk = ~clk;
  a_busy: assert property (@(posedge clk) req |=> busy[*2:4]) else fails++;
  initial begin
    @(negedge clk) req = 1;
    @(negedge clk) begin req = 0; busy = 1; end   // busy for five cycles: one too many
    repeat (5) @(negedge clk);
    busy = 0;
    repeat (3) @(negedge clk);
    $display("failures=%0d", fails);
    if (fails == 0) $display("FAIL: busy[*2:4] matched after two cycles, so a five-cycle busy passed");
    $finish;
  end
endmodule

See the Fix

module tb;
  logic clk = 0, req = 0, busy = 0;
  int fails = 0;
  always #5 clk = ~clk;
  a_busy: assert property (@(posedge clk) req |=> busy[*2:4]) else fails++;
  // The fix: a second rule for the upper bound. After four cycles of busy, it must drop.
  a_max:  assert property (@(posedge clk) req ##1 busy[*4] |=> !busy)
    else begin fails++; $display("t=%0t a_max failed", $time); end
  initial begin
    @(negedge clk) req = 1;
    @(negedge clk) begin req = 0; busy = 1; end   // busy for five cycles: one too many
    repeat (5) @(negedge clk);
    busy = 0;
    repeat (3) @(negedge clk);
    $display("failures=%0d", fails);
    if (fails > 0) $display("PASS: the upper-bound rule caught the fifth busy cycle");
    $finish;
  end
endmodule

Prints: t=65 a_max failed failures=1 PASS: the upper-bound rule caught the fifth busy cycle

Tool as Truth

"Just append ##1 !busy to the repetition."

That is the standard way to close the range. But Verilator 5.052 gives false failures and misses real ones when more sequence follows a ranged repetition. On that engine the separate upper-bound rule is the reliable form.

Source ASIC Point engine notes (Verilator 5.052 SVA probes), rows "[*m:n] followed by more"

Half-Truth

"Count the passes to see how long busy lasted."

An implication reports one success per attempt, so the pass count says nothing about length. Verilator 5.052 even runs the pass action once per longer match.

Source ASIC Point engine notes (Verilator 5.052 SVA probes), "Failing cases of the §7 forms" (busy[*2:4] row)

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

The Busy Signal That Lasted Too Long

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Mid-Level)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Senior)

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 (Mid-Level)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Senior)

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It