Case Study — FSM: X-Cleanup & Reset Signoff

Chapter 14 · Section 14.3 · Industry Case Studies

Project thread — the counter (14.2) becomes an FSM here, taken through X/reset signoff. 14.4 scales to a UART/timer peripheral; 14.5 to AXI-Lite; 14.6 to the mini-SoC.

1. Why Should I Learn This?

This is the archetypal GLS win — the reset-gap X that RTL hides and GLS exposes — as a full case.

• Surface the X (adapted TB, 5.5), root-cause it (backward-trace, 6.6), fix at source (reset, 7.5).
• xprop (6.5) shifts the catch left into RTL.
• Reset signoff = every state flop reset, no power-up X escapes — verified.

This is the case that justifies GLS's existence, applied to a controller.

2. Real Silicon Story — the FSM that powered up hung

An FSM controller occasionally powered up hung — outputs stuck, never advancing — in silicon, an intermittent field failure.

The root cause was a state flop whose reset was never connected (a reset gap): it powered up X, the X propagated to busy/done, and the FSM never reached a legal state. RTL had hidden it (X-optimism, 6.4); a properly adapted GLS run (5.5) surfaced it, and backward-tracing (6.6) reached the unreset flop. A one-line reset fix (7.5) cleared it — caught in simulation, not silicon.

Lesson: an FSM power-up X is almost always an unreset state flop — the reset-gap bug RTL hides and GLS exposes. Surface it, trace to source, fix the reset — before it hangs silicon.

3. Concept — the FSM X-cleanup case

The design: the FSM (IDLE → RUN → DONE + datapath) — real control state.

The case, end-to-end (Chapters 5–7):

1. Surface (5.5): the adapted testbench (port/bind checking, X-aware strobe, proper reset) shows a power-up X on busy/done.
2. Root-cause (6.6): trace backward — busy/done = X ← state = X ← a state flop that never saw reset (a reset gap, 2.6). Judge real, not pessimism (6.2).
3. Fix at source (7.5): connect a proper reset to every state flop (use the reset flop cell, assert long enough).
4. Shift-left (6.5): enable xprop in RTL so the state X appears in RTL regressions — catching the class earlier.

Reset signoff (the bar):

• Every state flop is reset (no reset gap).
• No power-up X escapes to the outputs — the X clears at reset and the FSM reaches legal states.
• Verified — the adapted testbench confirms it (no unexplained X after reset).

Scope (accuracy):

• Reset signoff here is functional/X (no unexplained X after reset) — the X was real (RTL-optimism hid it, 6.4). GLS stays dynamic (0.3).

4. Mental Model — the controller born blind, given sight by reset

The FSM is a controller born blind (X) at power-up — and reset gives it sight.

• Every state flop starts blind (X, 2.6); a proper reset opens its eyes (forces a known IDLE).
• Miss one flop's reset (a reset gap) and that eye stays blind — the blindness spreads (the X propagates) to the outputs, and the controller can't act (hangs).
• RTL doesn't notice (it imagines all eyes open — X-optimism, 6.4); GLS sees the blind eye (propagates the X).
• Trace the blindness back to the un-opened eye (the unreset flop) and open it (reset) — now the controller has full sight (all state reset, no X escapes).

Every eye must be opened by reset; GLS finds the one that wasn't.

5. Working Example — the FSM X-cleanup artifact set

The RTL (tri-HDL) — the FSM:

// SystemVerilog — FSM: IDLE -> RUN -> DONE, sync active-low reset
module fsm (input logic clk, rst_n, start, output logic busy, done);
  typedef enum logic [1:0] {IDLE, RUN, DONE} state_t; state_t state;
  always_ff @(posedge clk)
    if (!rst_n) state <= IDLE;
    else case (state) IDLE: state <= start ? RUN : IDLE; RUN: state <= DONE; DONE: state <= IDLE; endcase
  assign busy = (state == RUN); assign done = (state == DONE);
endmodule

// Verilog-2001 — same FSM
module fsm (clk, rst_n, start, busy, done);
  input clk, rst_n, start; output busy, done; reg [1:0] state;
  localparam IDLE=0, RUN=1, DONE=2;
  always @(posedge clk)
    if (!rst_n) state <= IDLE;
    else case (state) IDLE: state <= start?RUN:IDLE; RUN: state<=DONE; DONE: state<=IDLE; default: state<=IDLE; endcase
  assign busy = (state==RUN); assign done = (state==DONE);
endmodule

-- VHDL — same FSM
library ieee; use ieee.std_logic_1164.all;
entity fsm is port (clk, rst_n, start : in std_logic; busy, done : out std_logic); end entity;
architecture rtl of fsm is type state_t is (IDLE, RUN, DONE); signal state : state_t; begin
  process (clk) begin if rising_edge(clk) then
    if rst_n='0' then state<=IDLE;
    else case state is when IDLE=> if start='1' then state<=RUN; else state<=IDLE; end if;
      when RUN=>state<=DONE; when DONE=>state<=IDLE; end case; end if; end if;
  end process;
  busy <= '1' when state=RUN else '0'; done <= '1' when state=DONE else '0';
end architecture;

The bug (reset gap), the fix, and the expected log:

// Netlist — THE BUG: a state flop with no reset (reset gap) — REPRESENTATIVE
DFFX1  u_state1 (.D(next1), .CK(clk),             .Q(state[1]));  // NO RN -> powers up X -> propagates
// THE FIX: reset flop, reset on EVERY state bit (7.5)
DFFRX1 u_state1 (.D(next1), .CK(clk), .RN(rst_n), .Q(state[1]));  // RN=rst_n -> resets to 0

# Expected log — REPRESENTATIVE (X-cleanup & reset signoff):
#   BEFORE fix: busy/done = X after reset (state[1] unreset -> X propagates, 6.6)  -> FAIL
#   trace: busy(X) <- (state==RUN) <- state[1]=X <- u_state1 (DFFX1, no RN) = reset gap
#   AFTER fix: reset -> state=IDLE -> busy/done clean; FSM steps IDLE->RUN->DONE
#   xprop (6.5): RTL run now shows state X too (shift-left)
#   result: RESET SIGNOFF = every state flop reset, no power-up X escapes, VERIFIED

Practical context (representative, tool-neutral):

gls/case_fsm/
  rtl/fsm.v   netlist/fsm.vg (bug + fixed)   tb/tb_fsm.v   expected/fsm.log   rtl_xprop/ (6.5)
# Flow: synth -> adapted GLS surfaces power-up X -> backward-trace to unreset flop -> fix reset ->
#       re-run clean -> xprop in RTL catches the class. Reset signoff: every state flop reset, no X escapes.

The FSM X before the fix and clean after, as a real waveform:

6. Debugging Session — the FSM reset-gap X, root-caused and fixed

7. Common Mistakes

• Missing a state flop's reset (a reset gap) — power-up X propagates (6.6).
• Dismissing the X as pessimism — it's real, RTL-optimism hid it (6.2/6.4).
• Patching outputs instead of the reset at source (7.5).
• Not shifting left with xprop (6.5) — catch the class in RTL.
• Not verifying reset signoff — every state flop reset, no X escapes.

8. Industry Best Practices

• Reset every state flop — no reset gap.
• Surface power-up X with an adapted TB (X-aware strobe, 5.5).
• Backward-trace to source (6.6) and fix the reset (7.5).
• Shift the catch left with xprop (6.5).
• Verify reset signoff — every state flop reset, no unexplained X after reset.

Senior Engineer Thinking

• Beginner: "busy/done are X — I'll force them to a value in the TB."
• Senior: "That's a reset-gap X — trace it: busy ← state ← an unreset flop. I fix the reset on every state flop (source), verify reset signoff, and add xprop so RTL catches it next time. RTL hid it; GLS exposed it."

The senior root-causes the FSM X to an unreset flop, fixes the reset at source, and verifies reset signoff.

Silicon Impact

The FSM case is the archetype of a GLS-caught bug — and a high-stakes one: an FSM (or any controller) with an unreset state flop powers up in an illegal/unknown state and hangs or misbehaves in silicon, a power-up-dependent, intermittent failure that's brutal to reproduce and a classic field return (0.3). RTL's X-optimism hides this class (6.4), so only GLS (with faithful X-propagation) reliably catches it before tape-out — which is why GLS exists. The case's discipline — surface (adapted TB) → trace to source (backward) → fix the reset (every state flop) → verify reset signoff → shift left (xprop) — turns a scary wall of X into a one-line reset fix, in simulation, and prevents the hung-controller silicon failure. This is the reset-signoff bar every stateful design must clear.

Engineering Checklist

• Surfaced the power-up X with an adapted TB (X-aware strobe, 5.5).
• Backward-traced to the unreset state flop (6.6); judged real, not pessimism (6.2).
• Fixed the reset at source — every state flop (7.5).
• Verified reset signoff — no power-up X escapes to outputs after reset.
• Shifted the catch left with xprop in RTL (6.5).

Try Yourself

1. Synthesize the FSM with one state flop's reset disconnected and run the adapted GLS.
2. Observe: busy/done are X even after reset — trace back to the unreset DFFX1.
3. Change: swap it for a DFFRX1 with RN=rst_n (reset every state bit).
4. Expect: X clears at reset; the FSM steps IDLE→RUN→DONE — reset signoff. Then enable xprop in RTL and confirm the state X would have appeared there too.

Any free Verilog simulator runs the FSM X-cleanup case; xprop-style modes are widely available. No paid tool required.

Interview Perspective

• Weak: "The FSM outputs are X — I'd force them to a known value."
• Good: "I'd trace the X back — outputs from state, which is X because a flop isn't reset — and fix the reset."
• Senior: "It's a reset-gap X: an unreset state flop powers up X and propagates to busy/done. RTL's X-optimism hid it (6.4); the adapted GLS surfaced it. I backward-trace to the unreset flop, fix the reset at source on every state flop, verify reset signoff (no X escapes after reset), and add xprop so RTL catches the class. This is the bug GLS exists for."

9. Interview / Review Questions

10. Key Takeaways

• The FSM case does X-cleanup and reset signoff — the archetypal GLS win (the class RTL's X-optimism hides and GLS exposes, 6.4), on a real controller.
• The story end-to-end: a reset-gap X (an unreset state flop, 2.6) propagates to busy/done (Ch6); the adapted TB surfaces it (5.5); backward-tracing reaches the unreset flop (6.6); a proper reset at source on every state flop fixes it (7.5); xprop shifts the catch left into RTL (6.5).
• The X is real, not pessimism (6.2) — RTL hid it; GLS exposed it.
• Reset signoff = every state flop is reset, no power-up X escapes to the outputs — verified (adapted TB confirms clean states after reset).
• This is a functional/X signoff (no unexplained X after reset) — the bar every stateful case reuses; GLS stays dynamic (0.3). Next: 14.4 — UART / Timer peripheral GLS.

Quick Revision

FSM case = X-cleanup & reset signoff (the GLS-exists-for-this bug). Reset-gap X (unreset state flop, 2.6) → propagates to busy/done (Ch6) → adapted TB surfaces (5.5) → backward-trace to unreset flop (6.6) → fix reset at source, every state flop (7.5) → xprop shifts left (6.5). X is real (RTL hid it, 6.4). Reset signoff = every state flop reset + no power-up X escapes + verified. Next: 14.4 — UART / Timer peripheral GLS.