The checker transcribes the diagram, not the RTL. That independence catches a missing case arm, a creeping X, or an arc the spec never had.
State | Legal next states |
|---|---|
IDLE | IDLE, BUSY |
BUSY | BUSY, DONE, ERR |
DONE | DONE, IDLE |
ERR | ERR, IDLE |
The machine visits one row of the table per cycle; each step must appear in its row.
Slot 0: IDLE; reset has just released.
Slot 1: IDLE; start not yet seen.
Slot 2: BUSY; start accepted.
Slot 3: BUSY; the operation continues.
Slot 4: DONE; finish accepted.
Slot 5: IDLE; the machine is ready again.
module fsm_checker #(
parameter int MAX_BUSY = 256
)(
input logic clk, rst_n,
input logic [3:0] state
);
// bit, not logic: Verilator 5.048 rejects inside against 4-state localparams.
localparam bit [3:0] IDLE = 4'b0001, BUSY = 4'b0010,
DONE = 4'b0100, ERR = 4'b1000;
int n_fail = 0, n_ib = 0, n_bd = 0, n_be = 0, n_ei = 0;
function automatic void fail(string msg);
n_fail++;
$display("[%0t] fsm_checker: %s (state %b)", $time, msg, state);
endfunction
// R1: encoding always valid, one-hot and X-free
a_onehot: assert property (@(posedge clk) disable iff (!rst_n)
$onehot(state) && !$isunknown(state))
else fail("state encoding corrupt");
// R2: transition table, one assertion per row
a_from_idle: assert property (@(posedge clk) disable iff (!rst_n)
(state == IDLE) |-> ##1 (state inside {IDLE, BUSY})) else fail("illegal arc out of IDLE");
a_from_busy: assert property (@(posedge clk) disable iff (!rst_n)
(state == BUSY) |-> ##1 (state inside {BUSY, DONE, ERR})) else fail("illegal arc out of BUSY");
a_from_done: assert property (@(posedge clk) disable iff (!rst_n)
(state == DONE) |-> ##1 (state inside {DONE, IDLE})) else fail("illegal arc out of DONE");
a_from_err: assert property (@(posedge clk) disable iff (!rst_n)
(state == ERR) |-> ##1 (state inside {ERR, IDLE})) else fail("illegal arc out of ERR");
// R3: bounded no-deadlock, entry-detected so one thread measures each visit
a_busy_exits: assert property (@(posedge clk) disable iff (!rst_n)
(state != BUSY) ##1 (state == BUSY) |->
##[1:MAX_BUSY] (state != BUSY))
else fail("stuck in BUSY past bound");
// R4: reset leaves the machine in IDLE
a_reset_state: assert property (@(posedge clk)
$rose(rst_n) |-> (state == IDLE)) else fail("not IDLE out of reset");
// R5: arc covers, every legal transition seen in regression
c_idle_busy: cover property (@(posedge clk) (state == IDLE) ##1 (state == BUSY)) n_ib++;
c_busy_done: cover property (@(posedge clk) (state == BUSY) ##1 (state == DONE)) n_bd++;
c_busy_err: cover property (@(posedge clk) (state == BUSY) ##1 (state == ERR)) n_be++;
c_err_idle: cover property (@(posedge clk) (state == ERR) ##1 (state == IDLE)) n_ei++;
endmodule
// The machine, one-hot like the checker, with three plantable bugs.
module wfsm (
input logic clk, rst_n, start, done_in, err_in, clr,
input logic [1:0] bug, // 0 none, 1 DONE jumps to BUSY, 2 BUSY ignores done_in
output logic [3:0] state
);
localparam logic [3:0] IDLE = 4'b0001, BUSY = 4'b0010, DONE = 4'b0100, ERR = 4'b1000;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) state <= IDLE;
else case (state)
IDLE: if (start) state <= BUSY;
BUSY: if (err_in) state <= ERR; else if (done_in && bug != 2) state <= DONE;
DONE: state <= (bug == 1) ? BUSY : IDLE;
ERR: if (clr) state <= IDLE;
default: state <= IDLE;
endcase
endmodule
legal runs through DONE and through ERR: 0 new report(s)
arc covers: IDLE->BUSY 2, BUSY->DONE 1, BUSY->ERR 1, ERR->IDLE 1
[195] fsm_checker: illegal arc out of DONE (state 0010)
DONE jumped straight back to BUSY: 1 new report(s)
[325] fsm_checker: stuck in BUSY past bound (state 0010)
BUSY held for 12 cycles against a bound of 8: 1 new report(s)
PASS: the legal runs hit all 4 arc covers, and each planted bug was reported by the rule for its rowOne assertion per table row names the source state on failure. A single clever property would hide that name.
The listing is one file you can paste into the Code Lab: the checker first, then a small design and a bench that runs legal traffic before planting one bug at a time. Every rule reports through fail(), which counts and prints the report and lets the run go on; Verilator 5.048 stops at the first $error, and production checkers often count the same way. The design uses the checker's own one-hot encoding, so the two agree on what each state is.
The exit rule detects entry into BUSY, not the BUSY level. A level antecedent restarts the window every cycle and never measures dwell.
Control shape repeats two patterns. Mutex says two enables never coincide; hold-until-clear says a raised flag persists until serviced.
// snippet
// N-way mutex in one assertion (idle allowed):
// a_mutex_n: assert property (@(posedge clk) disable iff (!rst_n)
// $onehot0({mode_a, mode_b, mode_c, mode_d}));
// Interrupt held until serviced, then cleared promptly:
// a_irq_held: assert property (@(posedge clk) disable iff (!rst_n)
// irq && !service |-> ##1 irq);
// a_irq_clears: assert property (@(posedge clk) disable iff (!rst_n)
// irq && service |-> ##[1:2] !irq);The hold rule is the valid/ready skeleton again. irq && !service |-> ##1 irq matches valid && !ready |-> ##1 valid.
state == BUSY as its antecedent. What goes wrong?Every BUSY cycle spawns a fresh window, so no single thread measures dwell from entry. Detect entry with (state != BUSY) ##1 (state == BUSY).
Use membership plus an X check: state inside {IDLE, BUSY, DONE, ERR} with !$isunknown(state). With a 4-state base type (enum logic [3:0]), membership alone already fails on X, because an X result counts as false in an assertion; the $isunknown term makes that intent explicit. With the default int base type the enum is 2-state and cannot hold X.
Two legal runs, one through DONE and one through ERR, give no reports and hit all four arc covers. A design that jumps from DONE straight back to BUSY is reported by the DONE row, by name. A BUSY that ignores done_in for 12 cycles is reported by the exit rule once, because its antecedent detects entry into BUSY rather than the BUSY level.
Run with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.