Finite State Machines

Finite state machines control almost everything in a chip: bus interfaces, protocol engines, power controllers. Their bugs are typically in the corners: a transition that forgets to clear a timer, a state that can never be left, a state that can never be reached. This article lists the standard properties for state machines and uses them on a request controller with a timeout, whose timer is not cleared when a new request starts.

9 min read | Intermediate

What You'll Learn

• Write the standard properties of a state machine: legal states, transitions, outputs, no deadlock
• Check every state for reachability with covers
• Find a timer that is not reinitialized on a transition
• Prove a state machine property with k-induction

Standard FSM Properties

• Legal states: the state register only holds defined encodings. With a 2-bit register and 3 states, the fourth encoding must never appear.
• Legal transitions: each state goes only to its allowed successors, under the right conditions.
• Outputs per state: outputs match the state, such as busy exactly in WAIT.
• No deadlock: the machine cannot get stuck, which in a bounded check means a limit on how long it stays in a waiting state.
• Reachability: every state and every transition can happen, shown with covers.

The Design: a Request Controller

On req, the controller goes to WAIT and waits for ack. If no acknowledge comes within 4 cycles, it goes to ERR until software clears it:

module req_fsm (input clk, input rst, input req, input ack, input clr,
                output busy, output err, output reg [1:0] state);
  localparam IDLE = 2'd0, WAIT = 2'd1, ERR = 2'd2;
  reg [2:0] t;
  assign busy = (state == WAIT);
  assign err  = (state == ERR);
  always @(posedge clk)
    if (rst) begin
      state <= IDLE; t <= 3'd0;
    end else case (state)
      IDLE: if (req) state <= WAIT;                     // bug: t is not cleared here
      WAIT: if (ack)            begin state <= IDLE; end
            else if (t == 3'd3) begin state <= ERR;  t <= 3'd0; end
            else                      t <= t + 3'd1;
      ERR:  if (clr) state <= IDLE;
      default: state <= IDLE;
    endcase
endmodule

The timer t is cleared on reset and on the timeout, but not when an acknowledge ends the wait. The next request then starts with a timer that is already running.

The Properties

a_legal:   assert property (@(posedge clk) disable iff (rst) state != 2'd3);
a_timeout: assert property (@(posedge clk) disable iff (rst)
                            state == IDLE && req ##1 (state == WAIT && !ack) [*4] |=> state == ERR);
a_early:   assert property (@(posedge clk) disable iff (rst) $rose(err) |-> $past(state == WAIT, 4));

a_timeout says that four cycles of waiting without an acknowledge lead to ERR. a_early says that ERR is never entered without four cycles of WAIT before it. In the lab form, a helper counter w measures the time spent in WAIT:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // legal states only
  always @(*) if (!init) assert (state != 2'd3);
  // helper: how long the machine has been waiting
  reg [3:0] w = 4'd0;
  always @(posedge clk) w <= (rst || state != WAIT) ? 4'd0 : w + 4'd1;
  // ERR only after 4 cycles of waiting without ack
  always @(posedge clk) if (!init && !$past(rst) && err && !$past(err)) assert ($past(w) == 4'd3);
  // never stuck in WAIT: at most 4 cycles
  always @(*) if (!init) assert (w <= 4'd4);
`endif

The run fails at step 9:

The first request is acknowledged in its second cycle of waiting, which leaves t at 1. The second request starts with t = 1, so the controller reaches ERR after only 3 cycles of waiting. A slow memory that answers in the fourth cycle would be reported as failed. The fix clears the timer when a request is accepted: IDLE: if (req) begin state <= WAIT; t <= 3'd0; end.

Reachability

For every state, a cover shows that it can be reached, and the trace shows how. In the lab, the meant-to-fail form assert (!err) fails at step 6 on the fixed design: a request in step 1 and four cycles without an acknowledge. A state machine with an unreachable state either has dead logic or a bug that blocks the path to it.

A Proof

The fixed controller passes in prove mode with k-induction at depth 6, and with the PDR engine. A small state machine with a short timer is a typical case where a full proof is cheap, so there is no reason to stop at a bounded result.

Running It in ChipVerify Lab

The example below is the buggy controller with the properties above. It fails at step 9 within the free depth.

Common Mistakes