FSM & Arbiter Drills

Drill 1 — only legal FSM transitions

Problem

Interviewer: 'A 3-state FSM: IDLE→RUN, RUN→RUN, RUN→DONE, DONE→IDLE. Nothing else. Assert the transition relation.'

Think it through

• One property per source state: state==S |=> state inside {legal next set}. The inside operator keeps each line readable and each failure attributable.

• Add a state-validity invariant (state always one of the three encodings) — the transition properties assume the state is legal to begin with.

• |=> not |-> : the transition lands on the NEXT sampled state.

a_state_legal: assert property (
  @(posedge clk) disable iff (!rst_n)
  state inside {IDLE, RUN, DONE});

a_from_idle: assert property (
  @(posedge clk) disable iff (!rst_n)
  (state == IDLE) |=> (state inside {IDLE, RUN}));

a_from_run: assert property (
  @(posedge clk) disable iff (!rst_n)
  (state == RUN) |=> (state inside {RUN, DONE}));

a_from_done: assert property (
  @(posedge clk) disable iff (!rst_n)
  (state == DONE) |=> (state == IDLE));

PASS trace                          FAIL trace
cycle :  0    1    2    3    4      cycle :  0    1    2    3
state :  IDLE RUN  RUN  DONE IDLE   state :  IDLE DONE ...

Every adjacent pair is in the       IDLE→DONE at 0→1 is not in
legal set → PASS                    {IDLE,RUN}: a_from_idle FAILS
                                    at cycle 1, naming the source
                                    state in the failure.

Common wrong answers

• One mega-property OR-ing every legal (prev,next) pair with $past(state) — works but failures say only 'illegal transition somewhere'; per-source properties localize instantly.

• Writing the transitions with |-> — checks the next state in the SAME cycle as the source state: always self-comparing, never meaningful.

• Forgetting IDLE→IDLE / RUN→RUN self-loops in the legal sets — the FSM stalls legally and your assertion fires on every wait state.

Drill 2 — onehot state register

Problem

Interviewer: 'The state register is onehot-encoded, 5 bits. Assert the encoding never corrupts, including coming out of reset.'

a_state_onehot: assert property (
  @(posedge clk) disable iff (!rst_n)
  $onehot(state));

Think it through + common wrong answers

• $onehot = exactly one bit set; $onehot0 = at most one. A onehot FSM that is ever all-zeros is corrupt, so $onehot is the right strictness here.

• X poisoning: if any state bit is X, $onehot returns X and the assertion neither passes nor fails cleanly — pair with !$isunknown(state) (previous lesson) for a complete net.

• Wrong: $onehot0 'to be safe' — quietly legalizes the all-zero corruption you were hired to catch.

• Worth saying: onehot corruption usually comes from a bit-flip or a reset-tree gap, so this assert plus the X-check together localize the root cause fast.

Drill 3 — arbiter grant rules: no grant without request, single grant

Problem

Interviewer: 'Four requesters, four grant lines. Rule 1: a grant implies its request. Rule 2: never two grants at once. Write both; mind the per-bit versus whole-vector distinction.'

// Rule 1 — per-bit: gnt[i] implies req[i]
generate
  for (genvar i = 0; i < 4; i++) begin : g_gr
    a_gnt_has_req: assert property (
      @(posedge clk) disable iff (!rst_n)
      gnt[i] |-> req[i]);
  end
endgenerate

// Rule 1, vector idiom (equivalent, no loop):
a_gnt_subset: assert property (
  @(posedge clk) disable iff (!rst_n)
  ((gnt & ~req) == '0));

// Rule 2 — whole vector:
a_single_gnt: assert property (
  @(posedge clk) disable iff (!rst_n)
  $onehot0(gnt));

FAIL traces
            rule 1 violation        rule 2 violation
cycle :     0     1                 0     1
req   :     0010  0010              0011  0011
gnt   :     0010  0100              0001  0011

@1: gnt[2] high, req[2] low —       @1: two grants —
a_gnt_has_req[2] FAILS              $onehot0 false, FAILS

Common wrong answers

• |gnt |-> |req — 'some grant implies some request': grants to the WRONG requester pass. The per-bit (or mask) form is the entire point.

• gnt == req — demands a grant for every request immediately; arbiters by definition delay losers. Implication, not equality.

• $onehot(gnt) — forces a grant every cycle even when nobody requests; idle cycles fail.

Drill 4 — fairness: no starvation beyond N cycles

Problem

Interviewer: 'No requester that keeps its request asserted may wait more than 16 cycles for a grant. Phrase the antecedent carefully — what exactly re-arms the timer?'

Think it through

• Timer starts when an UNGRANTED request appears: $rose of (req[i] && !gnt[i]) — covers both a fresh request and a request that just lost arbitration again.

• The waiter may give up: discharge the obligation if req[i] drops — (gnt[i] || !req[i]) in the window, exactly like the basic latency drill but now stated as a fairness guarantee.

• The strong version 'every persistent request is EVENTUALLY granted' is a liveness property — unbounded, meaningful only in formal (s_eventually). In simulation, the bounded window IS the fairness check. Saying this distinction is the senior marker.

property p_no_starve(idx);
  @(posedge clk) disable iff (!rst_n)
  $rose(req[idx] && !gnt[idx]) |->
    ##[1:16] (gnt[idx] || !req[idx]);
endproperty
generate
  for (genvar i = 0; i < 4; i++) begin : g_st
    a_no_starve: assert property (p_no_starve(i));
  end
endgenerate

FAIL trace (i=3, two hogs ping-pong)
cycle  :  0  1  2  3  4  ... 17 18
req[3] :  0  1  1  1  1  ... 1  1
gnt[3] :  0  0  0  0  0  ... 0  0
gnt[0] :  0  1  0  1  0  ... 1  0
gnt[1] :  0  0  1  0  1  ... 0  1

req[3] rises ungranted at 1; cycles 2..17 show neither gnt[3]
nor a request drop → FAIL at 17. The arbiter ping-pongs 0/1
forever — a real RR-implementation bug class this catches.

Common wrong answers

• req[i] |-> ##[1:16] gnt[i] — level antecedent restarts the 16-cycle budget EVERY waiting cycle, so the deadline never effectively expires... and it fails givers-up. Doubly wrong.

• $rose(req[i]) alone as the trigger — a requester that was granted and immediately re-requests while losing arbitration never re-arms the timer.

• Claiming s_eventually gnt[i] 'also works in sim' — strong eventuality over an infinite horizon cannot fail at any finite cycle; it only reports at end-of-sim, and only as 'not yet satisfied'.

Drill 5 — round-robin order, simplified

Problem

Interviewer: 'Round-robin between two requesters: if I was just granted and my rival is requesting, the rival goes next — I cannot win twice in a row over a waiting rival. Just this pairwise rule.'

// 'No double-grant over a waiting rival', both directions
a_rr_01: assert property (
  @(posedge clk) disable iff (!rst_n)
  (gnt[0] && req[1]) |=> !gnt[0]);

a_rr_10: assert property (
  @(posedge clk) disable iff (!rst_n)
  (gnt[1] && req[0]) |=> !gnt[1]);

PASS trace                          FAIL trace
cycle  :  0  1  2  3                cycle  :  0  1  2  3
req[0] :  1  1  1  1                req[0] :  1  1  1  1
req[1] :  1  1  1  1                req[1] :  1  1  1  1
gnt    :  01 10 01 10               gnt    :  01 01 10 01
          (alternates) → PASS                  ↑
                                    gnt[0] repeats at cycle 1 while
                                    req[1] was up at 0 → a_rr_01
                                    FAILS at cycle 1.

Think it through + common wrong answers

• The full N-way round-robin order check needs a pointer model (aux register tracking last grant) — pairwise no-double-grant is the standard interview-scope simplification; name the limitation.

• Wrong: gnt[0] |=> gnt[1] — forces a grant to 1 even if requester 1 never asked; the rival-request qualifier is essential.

• Wrong: gnt[0] && req[1] |=> gnt[1] — too strong for arbiters with idle/bubble cycles between grants; the spec only forbade ME winning again, not WHO must win.

Key takeaways

• Per-source-state transition properties with inside sets give localized failures; |=> carries the transition to the next sample.

• Arbiter rules are per-bit obligations — vector-OR forms collapse 'the right requester' into 'any requester'.

• Bounded grant windows are the simulation-honest form of fairness; unbounded eventually belongs to formal.

Common pitfalls

• FSM transition checks with |-> — comparing a state to itself in the same cycle.

• Omitting self-loop transitions from legal-next sets — wait states fire the assertion.

• $onehot vs $onehot0 confusion — all-zeros is corruption for onehot FSMs, but idle for grant vectors.

• Level antecedents on starvation timers — the deadline re-arms every cycle and never expires.