Sequence Pattern Drills

Drill 1 — A then B then C, with arbitrary gaps

Problem

Interviewer: 'After start fires, we must eventually see grant, and after grant we must see done. Gaps of any length are allowed. Write it, then tell me what your version does NOT guarantee.'

Think it through

• Arbitrary gaps — goto repetition b[->1] ('first occurrence of b, however far away') reads better than ##[1:$] b and matches exactly once, at the FIRST b.

• ##[1:$] b creates one thread per future b; with [->1] there is a single thread. For an assert the end behavior is similar, but [->1] is cheaper and is the idiomatic answer.

• The honest caveat: both forms are WEAK in simulation. If grant simply never arrives, the attempt is still pending at end-of-sim and quietly passes. Say this before being asked.

property p_start_grant_done;
  @(posedge clk) disable iff (!rst_n)
  $rose(start) |=> grant[->1] ##1 done[->1];
endproperty
a_start_grant_done: assert property (p_start_grant_done);

PASS trace                          FAIL trace
cycle :  0  1  2  3  4  5  6        cycle :  0  1  2  3  4  5  6
start :  0  1  0  0  0  0  0        start :  0  1  0  0  0  0  0
grant :  0  0  0  1  0  0  0        grant :  0  0  0  0  0  1  0
done  :  0  0  0  0  0  1  0        done  :  0  0  0  1  0  0  0

start@1, first grant@3,             done (cycle 3) arrives BEFORE
done@5 after grant → PASS           grant (cycle 5). grant[->1]
                                    matches at 5, then needs done at
                                    6 or later — none. Pending at
                                    end-of-sim: weak property does
                                    not fail. Order bug missed →
                                    needs Drill 3's B-before-C form!

Variation — bounded version that CAN fail in simulation

// Give each step a deadline; now sim catches missing events:
property p_start_grant_done_bounded;
  @(posedge clk) disable iff (!rst_n)
  $rose(start) |-> ##[1:10] grant ##[1:10] done;
endproperty

Common wrong answers

• $rose(start) |=> grant ##1 done — no gaps allowed: grant must be exactly next cycle and done right after. Spec said 'eventually'.

• Believing grant[->1] ##1 done[->1] guarantees done comes after grant arrives AND that grant comes at all — it is weak; absence passes silently.

• ##[1:$] grant ##[1:$] done and claiming it checks 'the first grant' — it matches ANY grant/done pair; subtle difference worth knowing even when the assert verdict coincides.

Drill 2 — exactly N B-events between A and C

Problem

Interviewer: 'Between burst_start and burst_end there must be exactly 4 data beats (beat pulses). beats need not be back-to-back. burst_end may trail the last beat by any number of idle cycles. Choose your repetition operator carefully and justify it.'

Think it through

• This is THE [->N] vs [=N] discrimination question. Both mean 'N occurrences with gaps allowed'; they differ only at the END of the match.

• beat[->4] ends EXACTLY on the 4th beat — use it when something must happen at/right after the Nth occurrence.

• beat[=4] allows extra non-beat cycles AFTER the 4th beat before the sequence ends — use it when the closing event (burst_end) may trail. The spec says burst_end may trail → [=4].

• [=4] also guarantees exactly 4 (not 'at least 4') within the matched window — a 5th beat before burst_end kills every match thread.

property p_four_beats;
  @(posedge clk) disable iff (!rst_n)
  $rose(burst_start) |=> (beat[=4]) ##1 burst_end;
endproperty
a_four_beats: assert property (p_four_beats);

PASS trace ([=4] tolerates trailing idle)
cycle :  0  1  2  3  4  5  6  7  8  9
start :  0  1  0  0  0  0  0  0  0  0
beat  :  0  0  1  1  0  1  0  1  0  0
end   :  0  0  0  0  0  0  0  0  0  1
4 beats (2,3,5,7), idle 8, end@9 → PASS
( beat[->4] ##1 burst_end would FAIL here:
  [->4] ends at cycle 7, demands end at 8 — too early )

FAIL trace (5th beat sneaks in)
cycle :  0  1  2  3  4  5  6  7  8  9
beat  :  0  0  1  1  1  1  1  0  0  0
end   :  0  0  0  0  0  0  0  0  0  1
Any window containing burst_end holds 5 beats;
no [=4] match can absorb the 5th → FAIL.

Variation — burst_end exactly one cycle after the 4th beat

// Now the Nth occurrence anchors the close: [->N] is correct.
property p_four_beats_tight;
  @(posedge clk) disable iff (!rst_n)
  $rose(burst_start) |=> beat[->4] ##1 burst_end;
endproperty

Common wrong answers

• beat[*4] — CONSECUTIVE repetition; any idle gap between beats fails. The * vs -> vs = triage is the whole drill.

• beat[->4] when end may trail — fails legal traces with idle cycles before burst_end (shown above).

• beat[=4] when end must immediately follow beat 4 — passes traces where burst_end dawdles, missing the timing bug.

Drill 3 — after A, B must come before C

Problem

Interviewer: 'After a write is accepted, the data phase (dphase) must occur before the response (resp) is given. resp in the same cycle as dphase is legal. Assert the ordering.'

Think it through

• 'B before C' is really 'C stays away until B arrives' — flip it into a stability-style obligation on !resp.

• !resp until_with dphase: resp must be absent every cycle up to dphase; until_with lets dphase and resp coincide (spec allows same-cycle).

• This formulation fails the moment resp jumps the queue — unlike the weak A-then-B-then-C chain from Drill 1, which silently tolerated the order violation.

property p_dphase_before_resp;
  @(posedge clk) disable iff (!rst_n)
  $rose(wr_accept) |=> (!resp) until_with dphase;
endproperty
a_dphase_before_resp: assert property (p_dphase_before_resp);

PASS trace                          FAIL trace
cycle  :  0  1  2  3  4  5          cycle  :  0  1  2  3  4  5
accept :  0  1  0  0  0  0          accept :  0  1  0  0  0  0
dphase :  0  0  0  1  0  0          dphase :  0  0  0  0  1  0
resp   :  0  0  0  1  0  0          resp   :  0  0  1  0  0  0

resp coincides with dphase at 3     resp at 2 with no dphase yet:
(until_with permits) → PASS         !resp violated at 2 → FAIL
                                    immediately, at the offense.

Common wrong answers

• $rose(wr_accept) |=> dphase[->1] ##[0:$] resp — states B-then-C but never FORBIDS an early resp; an early resp plus a later dphase/resp pair passes. Ordering checks must constrain the forbidden event, not just sequence the wanted ones.

• until instead of until_with — rejects the legal same-cycle dphase+resp.

• not (resp before dphase) style with the rarely-supported 'before' — nonstandard; stick to until_with.

Drill 4 — exact bit pattern 1-0-1 on consecutive cycles

Problem

Interviewer: 'On grant, the strobe line must emit the training pattern: high, low, high on three consecutive cycles, starting the cycle after grant.'

property p_strobe_101;
  @(posedge clk) disable iff (!rst_n)
  $rose(grant) |=> strobe ##1 !strobe ##1 strobe;
endproperty
a_strobe_101: assert property (p_strobe_101);

PASS trace                          FAIL trace
cycle  :  0  1  2  3  4             cycle  :  0  1  2  3  4
grant  :  0  1  0  0  0             grant  :  0  1  0  0  0
strobe :  0  0  1  0  1             strobe :  0  0  1  1  1

cycles 2,3,4 = 1,0,1 → PASS         cycle 3 should be 0, is 1
                                    → FAIL at cycle 3.

Think it through + common wrong answers

• Fixed consecutive pattern — pure ##1 chaining of boolean values. No repetition operators, no goto. Simplest tool that works.

• Wrong: $rose(strobe) ##1 $fell(strobe) ##1 $rose(strobe) — sampled-value functions describe TRANSITIONS, doubling up the timing reasoning and breaking if strobe was already high. Assert values, not edges, for pattern matching.

• Wrong: strobe ##2 strobe with a separate !strobe check — same cycles, but split properties lose the single-failure atomicity; the interviewer wants one property per spec sentence.

Drill 5 — signal must toggle every cycle (alternating)

Problem

Interviewer: 'While phase_en is high, ph must alternate 0,1,0,1 every cycle.'

a_ph_alternates: assert property (
  @(posedge clk) disable iff (!rst_n)
  (phase_en && $past(phase_en)) |-> (ph != $past(ph)));

// Equivalent, more idiomatic:
a_ph_changed: assert property (
  @(posedge clk) disable iff (!rst_n)
  (phase_en && $past(phase_en)) |-> $changed(ph));

Think it through + common wrong answers

• Alternating ≡ different from the previous sample, every qualifying cycle. $changed(ph) is exactly $past(ph) != ph.

• Qualify with phase_en && $past(phase_en), same logic as the stability drill — the first enabled cycle has no alternation obligation against the pre-enable value.

• Wrong: ph |=> !ph alone — only constrains 1-to-0; you also need !ph |=> ph, or just use $changed and cover both polarities in one line.

• Wrong: $rose(ph) |=> $fell(ph) — edge functions again; $fell next cycle is implied by the value form and the doubled edges invite off-by-ones.

Key takeaways

• [*N] consecutive, [->N] ends ON the Nth occurrence, [=N] tolerates trailing gap — pick from where the NEXT event anchors.

• 'B before C' must be written as a prohibition on C (!c until_with b), not as a B-then-C sequence — weak sequences never flag the early C.

• Fixed patterns are plain value chains with ##1; sampled-value edge functions only complicate them.

Common pitfalls

• Using [*N] when the spec allows gaps — the silent killer in burst-counting drills.

• Relying on weak goto chains to enforce ordering or existence in simulation — pending-at-end-of-sim passes.

• Forgetting [=N] forbids extra occurrences inside its window — candidates often think it means 'at least N'.

• Edge functions ($rose/$fell) inside consecutive patterns — value chaining is simpler and X-safer.