Counting & Window Drills

Drill 1 — at most N transactions outstanding

Problem

Interviewer: 'The master may have at most 4 requests outstanding (issued, not yet completed). req and done are one-cycle pulses and can fire in the same cycle. Write the check.'

Think it through

• Counting across an unbounded number of overlapping transactions is NOT a job for sequence operators — local variables are per-attempt and cannot see each other. This is the canonical 'model it with auxiliary code' drill.

• Build a small always_ff counter: +1 on req, -1 on done, handle the same-cycle case (net zero).

• Then the assertions are trivial invariants on the counter: never above 4, and done never fires with nothing outstanding (underflow).

logic [2:0] outst;
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) outst <= '0;
  else        outst <= outst + (req && !done) - (done && !req);
end

a_max_outstanding: assert property (
  @(posedge clk) disable iff (!rst_n)
  outst <= 4)
  else $error("more than 4 outstanding");

// reject the 5th issue at the offending cycle, not one later:
a_no_issue_at_max: assert property (
  @(posedge clk) disable iff (!rst_n)
  (outst == 4) |-> !(req && !done));

a_no_underflow: assert property (
  @(posedge clk) disable iff (!rst_n)
  (outst == 0) |-> !(done && !req));

FAIL trace (5th issue while 4 outstanding)
cycle :  0  1  2  3  4  5  6
req   :  0  1  1  1  1  1  0
done  :  0  0  0  0  0  0  1
outst :  0  0  1  2  3  4  4*

At cycle 5: outst==4 and req&&!done → a_no_issue_at_max FAILS at 5.
(a_max_outstanding alone would fail at 6, one cycle late —
 that is why the |-> guard version is the stronger answer.)

Common wrong answers

• Trying (req, cnt = cnt + 1) with property local variables — locals are private to each attempt thread; there is no shared counter. Interviewers set this trap deliberately.

• outst <= outst + req - done without the same-cycle guard — works arithmetically (net 0), but the separate underflow assert then needs the !req qualifier; be consistent.

• Only asserting outst <= 4 — reports one cycle after the illegal issue; pair with the at-max guard for cycle-accurate blame.

Drill 2 — every requester granted within N cycles

Problem

Interviewer: 'An arbiter serves 4 requesters. Any asserted request must receive its grant within 8 cycles — unless the requester gives up and drops the request. Write it for all 4 without copy-pasting.'

Think it through

• Per-bit property + generate loop. One parameterized property, four instances — the expected structure.

• 'Unless it drops the request' — the obligation dissolves if req[i] deasserts; bake (gnt[i] || !req[i]) into the consequent window.

• Antecedent: the rise of an UNGRANTED request, $rose(req[i]) — a level antecedent would launch 8-cycle timers every cycle of waiting.

property p_grant_within(idx);
  @(posedge clk) disable iff (!rst_n)
  $rose(req[idx]) |-> ##[1:8] (gnt[idx] || !req[idx]);
endproperty

generate
  for (genvar i = 0; i < 4; i++) begin : g_fair
    a_grant_within: assert property (p_grant_within(i))
      else $error("requester %0d starved past 8 cycles", i);
  end
endgenerate

PASS trace (i=2)                    FAIL trace (i=2)
cycle  :  0  1  2  3  4  5          cycle  : 0 1 2 3 4 5 6 7 8 9
req[2] :  0  1  1  1  0  0          req[2] : 0 1 1 1 1 1 1 1 1 1
gnt[2] :  0  0  0  1  0  0          gnt[2] : 0 0 0 0 0 0 0 0 0 0

rise@1, gnt@3 (within 8) → PASS     rise@1; cycles 2..9 show neither
                                    gnt[2] nor request drop →
                                    FAIL at cycle 9. Starvation.

Common wrong answers

• req[i] |-> ##[1:8] gnt[i] — level antecedent (timer storm) AND fails honest traces where the requester legitimately gave up.

• One flat property over the whole vector (|req |-> ##[1:8] |gnt) — proves SOME grant followed SOME request; requester 3 can starve forever while requester 0 is served. Per-index is the point.

• Hardcoding four copy-pasted properties — functionally fine, structurally a miss; parameterize.

Drill 3 — exactly K events inside a W-cycle window

Problem

Interviewer: 'After window_start, the next 10 cycles must contain exactly 3 ev pulses. Pure SVA if you can; explain the trick.'

Think it through

• Two constraints in one: window LENGTH fixed at 10, event COUNT fixed at 3. Neither plain repetition nor plain delay does both.

• intersect is the trick: ev[=3] intersect 1[*10]. Both operands must match over the SAME cycles — 1[*10] pins the length to exactly 10, ev[=3] pins the count to exactly 3 within it.

• [=3]'s tolerance of leading/trailing gaps is what makes the intersection nonempty wherever the 3 events land inside the window.

property p_3_in_10;
  @(posedge clk) disable iff (!rst_n)
  $rose(window_start) |=> (ev[=3]) intersect 1[*10];
endproperty
a_3_in_10: assert property (p_3_in_10);

PASS trace
cycle :  0  1 | 2  3  4  5  6  7  8  9 10 11 | 12
wstart:  0  1 |                              |
ev    :  0  0 | 0  1  0  1  0  0  1  0  0  0 | 0
window (cycles 2..11): exactly 3 ev pulses → PASS

FAIL trace (4 events)
ev    :  0  0 | 0  1  1  1  0  0  1  0  0  0 | 0
ev[=3] can match many sub-windows, but NONE of length
exactly 10 contains exactly 3 — the 4th kills every
intersect thread → FAIL at cycle 11 (window close).

Variation — at least K in the window

// 'at least 3 in 10' — let the count run open-ended:
property p_atleast_3_in_10;
  @(posedge clk) disable iff (!rst_n)
  $rose(window_start) |=> (ev[->3] ##[0:$] 1) intersect 1[*10];
endproperty
// ev[->3] reaches the 3rd event, ##[0:$] 1 pads to the
// window edge; extra events beyond 3 are now tolerated.

Common wrong answers

• ##10 then 'count somehow' — delay moves a point in time; it cannot count. Candidates flail here unless they know intersect.

• ev[=3] alone — matches a window of ANY length with 3 events; the 10-cycle bound evaporates.

• Using and instead of intersect — and lets the operands match over DIFFERENT lengths; only intersect equalizes them. This distinction is the follow-up question every time.

Drill 4 — no more than N consecutive stall cycles

Problem

Interviewer: 'The pipeline may stall, but never more than 5 cycles in a row. Two different correct forms, please.'

// Form 1: forbid the bad run directly
a_stall_run_not: assert property (
  @(posedge clk) disable iff (!rst_n)
  not (stall[*6]));

// Form 2: after 5 in a row, the 6th cycle must clear
a_stall_run_imp: assert property (
  @(posedge clk) disable iff (!rst_n)
  stall[*5] |=> !stall);

FAIL trace (6 consecutive stalls)
cycle :  0  1  2  3  4  5  6  7
stall :  0  1  1  1  1  1  1  0

Form 1: attempt at cycle 1 matches stall[*6] over 1..6;
        'not' inverts → FAIL reported at cycle 6.
Form 2: stall[*5] matches 1..5 → consequent wants !stall
        at 6; stall still high → FAIL at cycle 6. Same verdict.

Think it through + common wrong answers

• Both forms fail at the same cycle; Form 2's failure message ('6th stall after 5') is usually clearer in logs. Form 1 generalizes better to forbidding whole sequences.

• Wrong: not (stall[*5]) — off by one, forbids exactly the maximum the spec allows. Always re-read whether N is the limit or the violation.

• Wrong: stall[*5] |-> !stall — overlapping implication puts !stall ON the 5th stall cycle: contradiction, fails every legal 5-stall run.

• Note 'not' is not negation of pass/fail in all senses — vacuity and multi-thread subtleties exist — but for a simple run-length forbid it is idiomatic and safe.

Key takeaways

• Cross-attempt counting (outstanding transactions) requires auxiliary always_ff state — property local variables are per-attempt by design.

• Per-requester fairness needs a generate loop of per-index properties; vector-OR forms hide starvation.

• intersect 1[*W] is the standard idiom to pin a counted pattern to an exact window length.

Common pitfalls

• Local-variable 'counters' inside properties — each attempt gets a private copy; no shared count exists.

• Level antecedents on latency checks — a waiting requester spawns a fresh deadline every cycle.

• and vs intersect — and tolerates different match lengths; only intersect forces same-cycle spans.

• [*N] vs [*N+1] in run-length limits — decide whether N itself is legal before writing the bound.