A job controller gained an abort input last week. Since then, software sometimes reads its status as READY and BUSY together. It writes a new job, which is accepted, but the controller also keeps doing the old one. No test failed until a bench with a reference model was added.
Which of the usual FSM bug shapes is this, and what would you read first to be sure?
They read the new line, | abort on the IDLE term, find it correct, and look elsewhere: the software, the status register, a race. The new line is correct; the bug is in the lines that did not change. FSM bugs hide in the cells of the state-by-input table that nobody wrote.
The RTL course's FSM bug stories walk three FSM bugs in detail; two of them, an output decoded from an unqualified input and an event that arrives in a state that does not test it, are shapes in the table below. Here is what each looks like when you meet it in a trace or a log.
Shape | In a trace or log | First thing to read |
|---|---|---|
Stuck state | the state holds one value for hundreds of cycles; a watchdog or timeout fires; nothing is wrong, nothing moves | the event that would leave this state, and whether it can still come |
Illegal state | a state value no case branch names, or two one-hot bits set; two outputs high that never should be | the cycle the value became illegal, and the inputs on the edge before it |
Missing transition | the release event happens, but in a state that does not look for it; the machine then waits forever | every state the event can arrive in, and whether each one tests it |
Mealy glitch | an output decoded from inputs pulses for less than a cycle, or for a cycle when its qualifier is low | which inputs feed the output, and whether they change between edges |
On the debug loop this is Localise then Hypothesise: the state register is the one signal that summarises the whole controller, so the first wrong cycle is usually the first wrong state.
Decode the state at the failure. Print it as an enum name (state.name()) or check $onehot. An unnamed value or two hot bits ends the search for the shape: it is illegal.
Measure time in state. Find when the state last changed. A long stay with no progress is a stuck state; then list what would move it on and check whether that event already happened in an earlier state.
Find the edge that broke it. Go to the cycle the state went wrong and read every input on the edge before it. Then fill in that state's row of the table: for each input combination, where should it go?
The controller has three states, written one-hot with one equation per state bit. Abort was added by OR-ing it into the IDLE bit. FIX = 0 is that change as first written; FIX = 1 (the default) also clears the RUN and DRAIN bits. The bench runs a reference model written as an enum and a case statement next to it, and checks $onehot and every output each cycle.
// onehot: a one-hot controller (IDLE, RUN, DRAIN) with an abort input added later. FIX = 0 is
// the change as first written: abort sets IDLE but does not clear RUN or DRAIN, so the state
// can hold two hot bits. FIX = 1 (the default) clears them. The bench compares the design with
// a reference model written as an enum and a case statement, and checks $onehot every cycle.
`timescale 1ns/1ps
module ctl #(parameter bit FIX = 1) (
input logic clk, rst_n, start, stop, empty, abort,
output logic ready, busy, flush);
localparam int IDLE = 0, RUN = 1, DRAIN = 2;
logic [2:0] st; // one-hot state
logic kill;
assign kill = FIX ? abort : 1'b0; // bad when FIX = 0: abort never clears
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) st <= 3'b001;
else begin
st[IDLE] <= (st[IDLE] & ~start) | (st[DRAIN] & empty) | abort;
st[RUN] <= ((st[IDLE] & start) | (st[RUN] & ~stop)) & ~kill;
st[DRAIN] <= ((st[RUN] & stop) | (st[DRAIN] & ~empty)) & ~kill;
end
assign ready = st[IDLE];
assign busy = st[RUN];
assign flush = st[DRAIN];
endmodule
module tb;
parameter bit FIX = 1;
typedef enum logic [1:0] {M_IDLE, M_RUN, M_DRAIN} mstate_t;
mstate_t m;
logic clk = 1'b0, rst_n = 1'b0, start = 1'b0, stop = 1'b0, empty = 1'b0, abort = 1'b0;
logic ready, busy, flush;
logic [15:0] lfsr = 16'hace1;
int cyc = 0, aborts = 0;
ctl #(.FIX(FIX)) u (.clk, .rst_n, .start, .stop, .empty, .abort, .ready, .busy, .flush);
always #5 clk = ~clk;
always_ff @(posedge clk or negedge rst_n) // reference model
if (!rst_n) m <= M_IDLE;
else if (abort) m <= M_IDLE;
else case (m)
M_IDLE: if (start) m <= M_RUN;
M_RUN: if (stop) m <= M_DRAIN;
M_DRAIN: if (empty) m <= M_IDLE;
default: m <= M_IDLE;
endcase
initial begin
#12 rst_n = 1'b1;
repeat (400) begin
@(negedge clk);
if (!$onehot(u.st) || ready !== (m == M_IDLE) || busy !== (m == M_RUN) || flush !== (m == M_DRAIN))
$fatal(1, "cycle %0d: st=%b (ready=%b busy=%b flush=%b), model is %s; inputs last edge: abort=%b",
cyc, u.st, ready, busy, flush, m.name(), abort);
lfsr = {lfsr[14:0], lfsr[15] ^ lfsr[13] ^ lfsr[12] ^ lfsr[10]};
start = lfsr[0]; stop = lfsr[3] & lfsr[5]; empty = lfsr[7];
abort = (lfsr[11:8] == 4'hf); // about 1 cycle in 16
if (abort && m != M_IDLE) aborts++;
cyc++;
end
$display("PASS: 400 cycles, %0d aborts outside IDLE, state one-hot and equal to the model (FIX=%0d)", aborts, FIX);
$finish;
end
endmodule$ iverilog -g2012 -P tb.FIX=0 -o o0.vvp onehot.sv && vvp -n o0.vvp
FATAL: onehot.sv:51: cycle 11: st=011 (ready=1 busy=1 flush=0), model is M_IDLE; inputs last edge: abort=1
Time: 130000 Scope: tb
$ verilator --binary --timing --assert -Wno-fatal --top-module tb -GFIX=0 -Mdir vl0 onehot.sv > /dev/null 2>&1 && vl0/Vtb
[130000] %Fatal: onehot.sv:51: Assertion failed in tb.unnamedblk1_1: cycle 11: st=011 (ready=1 busy=1 flush=0), model is M_IDLE; inputs last edge: abort=1
...
$ iverilog -g2012 -P tb.FIX=1 -o o1.vvp onehot.sv && vvp -n o1.vvp
PASS: 400 cycles, 11 aborts outside IDLE, state one-hot and equal to the model (FIX=1)Read the failing line with the checks. Check 1: st=011 is not one-hot, so the shape is an illegal state, and READY and BUSY are both high, exactly the report. Check 3: the input on the edge before was abort=1, and the model went to IDLE. Fill in the RUN row for abort: IDLE's bit sets, RUN's bit has no term that clears it. Both simulators agree to the cycle, so this is plain logic, not a race or an X. Lint is no help here: verilator --lint-only -Wall on the buggy controller reports only a file name and a C++ keyword.
A directed run of the same buggy controller. st is shown as a number: bit 0 IDLE, bit 1 RUN, bit 2 DRAIN, so 2 is RUN, 3 is IDLE plus RUN, 5 is IDLE plus DRAIN.
Slot 0: start is high. Slot 1: st is 2 (RUN), ready falls and busy rises.
Slot 3: abort is high. Slot 4: st is 3, and ready and busy are both high for three cycles.
Slots 6 to 7: stop moves the RUN bit on to DRAIN, and st is 5: still two states. The IDLE bit holds itself, so the machine is in IDLE and somewhere else until the extra bit drains out at slot 8.
dbglab's B2 is a deadlock, owned by the case study. Seen from the DMA's FSM it is the stuck-state shape. A check that reports any busy state held for more than 500 cycles finds it long before the watchdog:
// not-run: needs dbglab's sources and bench; compile it next to them (command in the Evidence box)
// stuck_check: report when the DMA's FSM sits in one busy state for more than 500 cycles.
// It only reads the design.
`timescale 1ns/1ps
module stuck_check;
int unsigned since = 0;
string last = "";
bit seen = 0;
always @(posedge dbglab_tb.clk) begin
#0.5; // just after the edge
if (dbglab_tb.dut.u_dma.state.name() != last) begin
last = dbglab_tb.dut.u_dma.state.name(); since = dbglab_tb.cycle;
end
if (!seen && last != "IDLE" && dbglab_tb.cycle - since > 500) begin
$display("STUCKCHK cycle=%0d: DMA in %s since cycle %0d", dbglab_tb.cycle, last, since);
seen = 1;
end
end
endmodule$ ../probes/run-probe.sh ../probes/stuck_check.sv dma_burst_backpressure 1
dbglab: test=dma_burst_backpressure seed=1
STUCKCHK cycle=668: DMA in WAIT since cycle 167
FAIL test=dma_burst_backpressure seed=1 cycle=2165: WATCHDOG: no bus or stream progress for 2000 cycles; cpu_valid=1 cpu_ready=0 cpu_addr=00003008
$ ../probes/run-probe.sh ../probes/stuck_check.sv dma_copy 1
dbglab: test=dma_copy seed=1
PASS test=dma_copy seed=1 cycles=1182 time=11816 nsThe check names the state (WAIT) and the cycle it was entered (167), which is where the case study's wait-for table starts. It is silent on passing tests. Then ask what would move the state on: WAIT needs FIFO space, and the case study follows that chain.
One next-state, one place. Write the machine as an enum state and a case that assigns a single next state. A global input such as abort goes first, as if (abort) next = IDLE; else case ..., so no state can forget it.
If you keep per-bit one-hot equations, every new input that leaves a state must appear in that state's bit as well as in the target's.
Illegal values go somewhere. A default that returns to a safe state, and an error flag, so an upset or a bug is recovered and reported.
Mealy outputs: qualify the decode with its valid signal, or register the output and pay the cycle.
Assert legality every cycle: $onehot(st) for one-hot, state inside {...} for an enum. The reproduction above found the bug at the first abort that reached RUN.
Assert time in state: a bound on how long any busy state may last, as stuck_check does, so a hang fails near its cause.
Cover every arc, not every state: abort from RUN and from DRAIN are two arcs a test must reach.
Review question: "For this new input, what does each state do with it?" Ask it of the rows, not of the new line.
ack pulsing once, two cycles before the machine entered WAIT_ACK. Which shape is this, and what do you check?A missing transition: the release event happened, but in a state (the one before WAIT_ACK) that did not look for it, so WAIT_ACK waits forever. Check every state ack can arrive in and whether each one tests it; the protocol may allow an early answer. The RTL course's story 3 has this exact shape.
With the outputs alone you need to know when READY and BUSY together is wrong, which the per-bit design does not tell you. The enum model has one state at a time by construction, so any second hot bit shows up as a mismatch, and $onehot checks the same thing directly. The check was written from the rule, not from the RTL.
onehot.sv as shown, 2026-10-18: iverilog -g2012 -P tb.FIX=0 then vvp -n (Icarus Verilog 13.0) stops at cycle 11 with st=011; verilator --binary --timing --assert -Wno-fatal --top-module tb -GFIX=0 (Verilator 5.048) stops with the same message; FIX=1 passes 400 cycles with 11 aborts outside IDLE in both. verilator --lint-only -Wall -GFIX=0 --top-module ctl reports only DECLFILENAME and SYMRSVDWORD.
The waveform comes from COURSE=dbg node scripts/tools/gen-waves.mjs bug-classes:fsm-bugs (Icarus), which matched its expectations; a second run changed nothing.
dbglab at HEAD 49c5f04: stuck_check.sv compiled next to the bench (iverilog -g2012 -Wno-timescale -I tb -o build/probe.vvp <rtl/files.f> tb/bus_rules.sv tb/dbglab_tb.sv stuck_check.sv, vvp -n build/probe.vvp +TEST=dma_burst_backpressure +SEED=1) prints at cycle 668; silent on dma_copy 1 and random 1, which pass.
Limits: one small controller and one dbglab hang. Mealy glitches are described and linked, not reproduced here: a zero-delay RTL simulation shows them only when inputs change between clock edges.