State, transitions and reachability

Add flip-flops and a circuit gains memory. A synchronous design can be described completely by:

• a set of state variables — the flops, e.g. s[1:0];
• the initial states — the values after reset;
• the transition function — next state as a Boolean function of current state and inputs;
• the output function.

A property such as "the FSM never enters ERROR" becomes a question about reachability: starting from the initial states and repeatedly applying the transition function, can we ever arrive at a state where the property is false?

Example: a 2-bit sequencer with an unreachable state

// phase_seq.sv — cycles A -> B -> C -> A while 'go' is high
module phase_seq (
  input  logic       clk, rst, go,
  output logic [1:0] phase
);
  localparam logic [1:0] A = 2'd0, B = 2'd1, C = 2'd2;   // 2'd3 is never used

  always_ff @(posedge clk) begin
    if (rst)     phase <= A;
    else if (go) case (phase)
                   A:       phase <= B;
                   B:       phase <= C;
                   default: phase <= A;   // C (and the unused 3) go back to A
                 endcase
  end
endmodule

The value phase == 3 is representable by two flops but unreachable from reset. That distinction matters a lot in formal:

• An assertion phase != 3 is true — it holds in every reachable state.
• But an engine that reasons about "any state", not just reachable ones, may stumble over state 3 — you will see exactly this problem with induction later in this chapter.

Computing the reachable set

Conceptually, an engine computes reachable states as a growing set:

1. R₀ = initial states = {A}
2. R₁ = R₀ ∪ successors(R₀) = {A, B}
3. R₂ = R₁ ∪ successors(R₁) = {A, B, C}
4. R₃ = R₂ — nothing new; we have reached a fixed point.

Once the fixed point is reached, if no state in it violates the property, the property is proven for all time. The trick is representing these sets compactly when there are billions of states — that is what BDDs and SAT-based methods do.