Verilog design patterns

FSM Design in Verilog: One-Hot vs Binary vs Gray Encoding

A finite state machine is the workhorse of control logic in RTL, and two decisions shape how robust yours will be: the coding style you use to write it, and the state encoding the synthesizer maps it to. This page covers both. It walks through the two-always and three-always FSM templates, compares binary, one-hot, and gray encoding on area, speed, and power, and then turns to the failure modes that actually bite in silicon — the missing default arm, the parasitic codes a binary state vector can land on, unreachable states that signal dead logic, and how a safe FSM recovers from an illegal state. It closes with what structural FSM analysis can tell you about a design before you ever run synthesis — encoding, reachability, and missing-default evidence — and, just as importantly, what it cannot: it is pre-signoff evidence, not a formal proof that the machine is live.

Coding style: 2-block vs 3-block FSM

A finite state machine has three jobs: hold the current state, compute the next state, and drive outputs. How you partition those jobs across always blocks is the coding style, and it is independent of the encoding. The two templates you will see everywhere are the two-always and three-always styles.

The two-always (2-block) FSM uses one sequential block to register the state on a clock edge and one combinational block to compute the next state and the outputs together. It is compact and is the form most people reach for first.

// Two-always (2-block) FSM. One sequential block registers the state;
// one combinational block computes next state AND outputs together.
typedef enum logic [1:0] {IDLE, REQ, BUSY, DONE} state_e;

state_e state, next;

// 1) sequential: the only edge-sensitive block
always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) state <= IDLE;
    else        state <= next;

// 2) combinational: next state + Moore output, every signal defaulted
always_comb begin
    next  = state;     // default: hold (no latch on 'next')
    valid = 1'b0;      // default every output (no latch on 'valid')
    case (state)
        IDLE: if (start) next = REQ;
        REQ:             next = BUSY;
        BUSY: if (done)  next = DONE;
        DONE: begin valid = 1'b1; next = IDLE; end
        default:         next = IDLE;   // recover from any illegal code
    endcase
end

Notice the two defaults at the top of the combinational block: next = state and valid = 1'b0. Without them, any state arm that forgets to drive a signal infers a latch. That is the single most common FSM bug, and it is covered in depth in our inferred latches article.

The three-always (3-block) FSM splits the combinational block in two: one block for next-state logic, a separate block for outputs. The win is clarity — Moore outputs become a pure function of the current state, and turning an output into a registered output is a one-line move (compute it in the sequential block instead). The cost is one more block to keep in sync.

// Three-always (3-block) FSM: next-state and outputs in SEPARATE blocks.
// Cleaner Moore outputs; registered outputs become a one-line change.
always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) state <= IDLE;
    else        state <= next;

always_comb begin           // next-state ONLY
    next = state;
    case (state)
        IDLE: if (start) next = REQ;
        REQ:             next = BUSY;
        BUSY: if (done)  next = DONE;
        DONE:            next = IDLE;
        default:         next = IDLE;
    endcase
end

always_comb begin           // outputs ONLY (Moore: function of state)
    valid = (state == DONE);
end

One rule cuts across both styles: only the sequential block uses non-blocking assignment (<=), and the combinational blocks use blocking (=). Mixing them is a classic source of simulation-versus-synthesis mismatch — see blocking vs non-blocking.

State encoding: binary, one-hot, gray

The encoding is the bit pattern each state maps to. The same machine can be encoded three ways without changing a line of the control flow — only the enum values change.

// The encoding is just how the enum maps to bits. Same machine, three maps.
// Binary: ceil(log2 N) flops, densest.
typedef enum logic [1:0] {B_IDLE=2'd0, B_REQ=2'd1, B_BUSY=2'd2, B_DONE=2'd3} bin_e;

// One-hot: N flops, exactly one bit asserted. Shallow, fast decode.
typedef enum logic [3:0] {H_IDLE=4'b0001, H_REQ=4'b0010, H_BUSY=4'b0100, H_DONE=4'b1000} oh_e;

// Gray: adjacent transitions flip ONE bit. Lower toggle power; CDC-friendly.
typedef enum logic [1:0] {G_IDLE=2'b00, G_REQ=2'b01, G_BUSY=2'b11, G_DONE=2'b10} gray_e;

• Binary. States numbered 0, 1, 2, … in ceil(log2 N) flip-flops. The most register-efficient encoding, so it wins when flops are scarce or the machine has many states. The trade-off is deeper, slower decode logic (every output and next-state term must decode the full binary value) and parasitic codes — covered below.
• One-hot. One flip-flop per state; exactly one bit high at a time. Next-state and output logic become a single product term per state, so the decode is shallow and fast. It costs N flops, which is cheap on an FPGA (registers are abundant and the LUT depth saved matters more) and the usual default there. On an ASIC with a large state count the flop cost is more visible.
• Gray. States ordered so that each legal transition flips exactly one bit. Fewer toggles means lower switching power, and — the bigger reason — if the encoded state value is sampled in another clock domain, a one-bit-at-a-time code prevents multi-bit skew from producing a transient illegal value. That is the same principle a gray-coded pointer uses in an async FIFO; see clock domain crossing. Gray only flips one bit on adjacent transitions, so it helps most when the state sequence is roughly linear.

A practical caveat: most synthesis tools re-encode FSMs themselves (Design Compiler’s fsm_auto, Yosys’s fsm pass). Your source encoding is a starting point and a hint, not a guarantee of the gates you get. If the encoding matters for power or CDC reasons, set the synthesis attribute explicitly and check the result rather than trusting the enum.

The traps: default, parasitic, and unreachable states

Three related failure modes account for most FSM bugs that survive a green simulation and only surface later.

• Missing default. A next-state case with no default leaves the next state undefined for any selector value you did not list. Synthesis infers a latch on next or leaves the behaviour tool-dependent. Both are bugs.
• Parasitic states. With binary or gray encoding, ceil(log2 N) flops can represent more codes than you have legal states. A 5-state machine in 3 bits has 3 parasitic codes. They are unreachable in normal operation, but a single-event upset, a reset glitch, or an x on power-up can land the machine on one. Without a recovery path the FSM can lock up. One-hot has its own version: any vector that is not exactly one-hot is illegal.
• Unreachable states. The mirror image: a declared state with no incoming transition in the next-state logic. It is never a crash, but it is a strong signal of dead code, a typo in a transition target, or a feature half-removed. Worth flagging in review even though it is not a functional failure on its own.

Simulation alone rarely catches these. A directed test exercises the legal transitions you thought of; it does not inject a parasitic code or drive the machine into the arm you forgot. That is why a structural check that reasons over all codes pays off — more on that below.

Writing a safe FSM

A safe FSM is one that recovers deterministically from an illegal state instead of locking up. The discipline is two rules applied together:

• Assign every next-state and output signal an unconditional default at the top of each combinational block, so nothing latches and outputs are glitch-free in unlisted states.
• Give the next-state case a default arm that steers the machine back to a known recovery state — usually IDLE or a dedicated RESET state. For one-hot, you can additionally detect a non-one-hot vector and force recovery explicitly.

The 2-block example above is already written this way: next = state defaults the next state, every output is defaulted, and the default: next = IDLE arm gives every illegal code a defined exit. This is sound defensive coding. It is not, and does not replace, a formal liveness proof: it guarantees a defined transition out of an illegal state, not that the machine can always make forward progress from every legal one.

What structural FSM analysis can tell you

You do not need to run synthesis or write a formal harness to learn a lot about an FSM. By parsing the RTL and reasoning over the next-state logic, a structural analyzer can extract the machine and report concrete, file-and-line evidence:

• State register and encoding. Identify the state flip-flop and classify the encoding it appears to use — binary, one-hot, gray, or custom — from the enum values and the assignment pattern.
• Reachability graph. Build the directed graph of states from the next-state case/if logic and flag states with no incoming edge (unreachable) so you can tell dead code from a transition typo.
• Missing default / illegal-state exit. Detect a next-state case with no default, which is where parasitic codes go undefined, and the inferred-latch risk that comes with it.

This is evidence to triage, gathered fast and without a license. It is explicitly structural, pre-signoff analysis — not a formal proof of liveness or deadlock-freedom, and not a foundry signoff. A reachability graph built from the RTL tells you a state has no incoming edge in the code you wrote; it does not prove the machine cannot deadlock under all input sequences. For that you need a formal model checker, which is a different and heavier tool. Used for what it is, structural FSM analysis catches the missing-default and unreachable-state class of bug early, where it is cheap to fix.

Where FSM checks fit in a verification flow

Structural FSM analysis sits alongside lint and simulation as an early, cheap gate. A reasonable order: run a lint checklist on every push (it catches the missing-default and latch shapes), pull the structural FSM evidence to review encoding and reachability, then escalate the machines that matter to SystemVerilog assertions and formal property checking for the liveness and safety properties a structural pass cannot prove. The bigger picture of how lint, simulation, structural checks, and formal compose is in our RTL verification overview.

Related rules

• Inferred latches — the FSM next-state block is the #1 source; default every signal at the top of the combinational block.
• Blocking vs non-blocking — sequential block uses <=, combinational blocks use =; mixing them breaks the FSM in subtle ways.
• Clock domain crossing — why gray encoding matters when a state vector is sampled in another clock domain.
• RTL lint checklist — the missing-default and latch rules that catch the most common FSM structural bugs before elaboration.
• SystemVerilog assertions — how to express the liveness and one-hot safety properties a structural pass cannot prove on its own.
• RTL verification — where structural FSM checks fit in a pre-synthesis flow.

FAQ

Scan your repo

Point ChipVerify AI at a GitHub URL and its FSM analysis extracts the state machines in your RTL: it reports the inferred encoding (binary / one-hot / gray / custom), builds the reachability graph, and flags states with no incoming edge and next-state cases with no default. No install, no synthesis license, no formal setup — structural evidence you can triage in minutes.