FSM Assertions

Assert the state diagram, not the implementation

FSM assertions transcribe the state diagram — the spec — into executable rules: which encodings are valid, which arcs are legal, that the machine cannot wedge, and that it wakes up in the right state. Done this way, the checker is independent of the RTL's case-statement structure, so it catches exactly the bugs RTL self-review misses: a missing case arm, an X creeping into the state register, a synthesis-time encoding disagreement, an arc the designer added but the spec never had.

Example FSM and its legal-transition table

        ┌─────────┐  start   ┌─────────┐  done    ┌─────────┐
   ┌──► │  IDLE   │ ───────► │  BUSY   │ ───────► │  DONE   │ ──┐
   │    └─────────┘          └────┬────┘          └─────────┘   │
   │         ▲                    │ err                ▲ (ack)  │
   │         │               ┌────▼────┐               │        │
   │         └────(clr)───── │  ERR    │               │        │
   │                         └─────────┘               │        │
   └───────────────────────────────────────────────────┘

  state   legal next states
  ─────────────────────────────
  IDLE    IDLE, BUSY
  BUSY    BUSY, DONE, ERR
  DONE    DONE, IDLE
  ERR     ERR,  IDLE

The canonical ruleset

1. Encoding validity: state is always a defined encoding (one-hot + X-free, or inside the enum set).

2. Legal transitions: every observed arc appears in the spec's transition table.

3. No deadlock (bounded): every non-idle state is exited within N cycles.

4. Reset state: the cycle after reset deasserts, the machine is in IDLE.

5. Arc coverage: every legal transition observed at least once across the regression.

Complete checker module

module fsm_checker #(
  parameter int MAX_BUSY = 256
)(
  input logic clk, rst_n,
  input logic [3:0] state   // one-hot: IDLE=0001 BUSY=0010
);                          //          DONE=0100 ERR=1000
  localparam logic [3:0] IDLE = 4'b0001, BUSY = 4'b0010,
                         DONE = 4'b0100, ERR  = 4'b1000;

  // R1: encoding always valid — one-hot and X-free
  a_onehot: assert property (@(posedge clk) disable iff (!rst_n)
    $onehot(state) && !$isunknown(state))
    else $error("state encoding corrupt: %b", $sampled(state));

  // R2: transition table — one assertion per ROW of the table
  a_from_idle: assert property (@(posedge clk) disable iff (!rst_n)
    (state == IDLE) |-> ##1 (state inside {IDLE, BUSY}));
  a_from_busy: assert property (@(posedge clk) disable iff (!rst_n)
    (state == BUSY) |-> ##1 (state inside {BUSY, DONE, ERR}));
  a_from_done: assert property (@(posedge clk) disable iff (!rst_n)
    (state == DONE) |-> ##1 (state inside {DONE, IDLE}));
  a_from_err:  assert property (@(posedge clk) disable iff (!rst_n)
    (state == ERR)  |-> ##1 (state inside {ERR, IDLE}));

  // R3: bounded no-deadlock — BUSY must be left within MAX_BUSY
  a_busy_exits: assert property (@(posedge clk) disable iff (!rst_n)
    (state != BUSY) ##1 (state == BUSY) |->
      ##[1:MAX_BUSY] (state != BUSY))
    else $error("stuck in BUSY > %0d cycles", MAX_BUSY);

  // R4: reset lands in IDLE on the first clean cycle
  a_reset_state: assert property (@(posedge clk)
    $rose(rst_n) |-> (state == IDLE));

  // R5: arc covers — every legal transition seen in regression
  c_idle_busy: cover property (@(posedge clk)
    (state == IDLE) ##1 (state == BUSY));
  c_busy_done: cover property (@(posedge clk)
    (state == BUSY) ##1 (state == DONE));
  c_busy_err:  cover property (@(posedge clk)
    (state == BUSY) ##1 (state == ERR));
  c_err_idle:  cover property (@(posedge clk)
    (state == ERR)  ##1 (state == IDLE));
endmodule

Illegal-arc and deadlock traces

  tick   :   1     2     3     4     5
  state  :  IDLE  IDLE  DONE  ...        ← IDLE→DONE: not in the table
  a_from_idle attempt @2: state==IDLE → obligation @3:
  state inside {IDLE,BUSY}; sampled DONE → FAIL@3, names the bad arc.

  Deadlock (MAX_BUSY=3 for illustration):
  tick   :   1     2     3     4     5     6
  state  :  IDLE  BUSY  BUSY  BUSY  BUSY  BUSY
  a_busy_exits: entry detected by (state!=BUSY)##1(state==BUSY) @1→2;
  window ##[1:3] = ticks 3..5 must show state!=BUSY; all BUSY → FAIL@5.
  Note the ENTRY-detection antecedent: one attempt per entry, not one
  per BUSY cycle — same edge-vs-level logic as $rose on a request.

Design choices in the ruleset

Row-per-assertion vs one big case

You could compress R2 into a single property with a case inside a function, but one assertion per table row pays off in triage: the failing assertion's name identifies the source state instantly, the per-row pass counts double as crude arc statistics, and reviewers can diff the assertion list against the spec table line by line. Mechanical, reviewable transcription is the goal — cleverness is the enemy here.

Why bounded deadlock checks

“The FSM never gets stuck” is a liveness property; in simulation, prefer the bounded safety form — “leaves BUSY within MAX_BUSY” — which fails loudly at a specific cycle. Choose the bound from the spec's worst-case dwell (longest transaction, timeout, etc.) plus margin; a too-tight bound creates false failures on legal long operations, so the bound itself is a reviewable spec artifact. For formal, keep an unbounded s_eventually variant alongside.

Enum-typed state? Adjust R1

If state is a SystemVerilog enum rather than raw one-hot bits, replace the one-hot rule with membership: state inside {IDLE, BUSY, DONE, ERR} plus !$isunknown(state). Membership alone does not imply X-freedom — an X-laden vector fails inside comparisons in ways that differ across tools, so keep the explicit X check.

Interview angle

FSM checking is a favorite because it tests whether you assert the spec or merely re-state the RTL. Lead with the five-rule decomposition (encoding, arcs, deadlock, reset, covers). Expected follow-ups: why $onehot needs !$isunknown beside it (X bits are not counted as ones — a corrupted 01x0 register still passes $onehot); why the deadlock antecedent detects entry into BUSY rather than testing the BUSY level (level form spawns a fresh timeout window every cycle — both wasteful and wrong, since each cycle restarts the count); and what cover points buy you (an arc with zero hits across a full regression is either dead spec or dead stimulus — both findings matter). If asked to handle an FSM with 30 states, say generate-from-table: emit the row assertions from the spec's transition table programmatically rather than hand-writing them.

Key takeaways

• Transcribe the state diagram: encoding validity, one assertion per transition-table row, deadlock bound, reset state, arc covers.

• $onehot plus !$isunknown — X bits silently pass a bare one-hot check.

• Detect ENTRY into a state for timeout rules; the level form restarts the window every cycle.

• Bounded exit checks turn liveness into failable safety; derive the bound from spec worst case.

• Zero-hit arc covers expose dead spec or dead stimulus — both are sign-off findings.

Common pitfalls

• Asserting transitions by copying the RTL case statement — the checker inherits the RTL's bugs.

• Bare $onehot(state) without the X check — 4'b01x0 passes while the register is corrupt.

• Deadlock rule with a level antecedent — a new timeout thread every BUSY cycle, none measuring dwell.

• Reset-state check clocked while reset is still asserted — sample the first cycle after $rose(rst_n).

• No arc covers — illegal arcs are caught, but never-exercised legal arcs stay invisible forever.