"Simulation passes. How do you know this FSM is correct?" The interviewer is asking for the properties beyond directed tests, and how each one is checked.
The complete answer names three properties, gives the check for each, and states the input assumptions the checks rest on.
Three important structural checks are reachability, return to IDLE under explicit input assumptions, and illegal-code recovery. They are not a complete functional proof: also check output legality and the transaction contract. Here grant must be high only in SEND or WAIT, never while IDLE, arbitrating, retrying or DONE.
Property | Procedural check | SVA shape |
|---|---|---|
Reachability | Drive a legal input prefix to each state | Cover each state |
No deadlock | From each state, return to IDLE within N cycles | Assert return under input assumptions |
Unused-code RTL recovery | Force unused codes in this RTL encoding, expect IDLE | Assert recovery under an explicit fault model; check mapped implementation separately |
Read each arc as one line of the case statement. The three properties are statements about this picture.
Reachability: every state has an arc into it from IDLE through legal inputs.
Return to IDLE: from SEND, WAIT or RETRY the only way home is ack, then DONE. That is why the no-deadlock check assumes ack eventually arrives.
Unused codes 6 and 7 are not drawn; the default branch sends them to IDLE.
No-deadlock claims always rest on input assumptions. A WAIT state that holds for a missing acknowledge is a legal stay, not a bug. The check drives the awaited input and requires the return.
Fault model: the bench forces unused binary codes 6 and 7 with req low. Faults into legal states are undetected by a default, and synthesis can optimize/re-encode recovery. Safety requirements need supported safe-FSM controls, report inspection and implementation-level fault checks; see illegal states and recovery.
// snippet
// The two properties this lesson proves procedurally, in SVA shape:
// cp_reached_done: cover property (@(posedge clk) state == DONE);
// ap_return_home: assert property (@(posedge clk) (state != IDLE) |-> s_eventually (state == IDLE));
// Liveness (s_eventually) needs fairness assumptions on the inputs, so the
// testbench below drives those inputs explicitly instead.Simulation or formal for the no-deadlock claim? Simulation shows return paths exist. Formal proves them for all inputs under the stated assumptions. Use both where the FSM guards safety.
What exactly is assumed of the inputs? That an awaited response eventually arrives. Without that fairness, any wait state is a correct infinite stay.
Which coverage metric backs the claim? State and transition coverage. The checks below visit all six states and every return arc back to IDLE.
"Reset was tested, so the FSM is fine." Reset covers one state. The other five, and every arc between them, are still unproven.
"Full line coverage proves the FSM." Line coverage can pass while a state is never visited. State and transition coverage are the relevant metrics.
"The default guarantees silicon recovery." It specifies RTL unused-code behavior. Review synthesis safe-FSM settings and implemented recovery; neither a default nor unique/default diagnoses faults into another legal state.
Two cycles: WAIT to DONE, then DONE to IDLE. The bound of 6 covers the longest return path (three cycles from ARB or RETRY) with margin.
Without it the liveness claim is false: a missing acknowledge holds WAIT forever by design. Stating the assumption turns a hang into a checked contract on the peer block.
A 6-state transfer controller plus procedural checks for reachability, bounded return to IDLE, and illegal-code recovery.
// State codes are named once, above the design, so the testbench can reuse them.
typedef enum logic [2:0] {IDLE, ARB, SEND, WAIT, RETRY, DONE} state_t;
module xfer_ctrl (
input logic clk, rst_n, req, ack, err,
output logic grant, busy,
output logic [2:0] state_o
);
state_t state, next_state;
always_comb begin
next_state = state;
grant = 1'b0;
busy = 1'b1;
case (state)
IDLE: begin busy = 1'b0; if (req) next_state = ARB; end
ARB: next_state = SEND;
SEND: begin grant = 1'b1; if (ack) next_state = DONE; else if (err) next_state = RETRY; else next_state = WAIT; end
WAIT: begin grant = 1'b1; if (ack) next_state = DONE; else if (err) next_state = RETRY; else next_state = WAIT; end
RETRY: next_state = SEND;
DONE: begin busy = 1'b0; next_state = IDLE; end
default: next_state = IDLE;
endcase
end
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) state <= IDLE;
else state <= next_state;
// Named-state readout for the testbench: literals only, so no enum-to-vector cast.
always_comb begin
case (state)
IDLE: state_o = 3'd0;
ARB: state_o = 3'd1;
SEND: state_o = 3'd2;
WAIT: state_o = 3'd3;
RETRY: state_o = 3'd4;
DONE: state_o = 3'd5;
default: state_o = 3'd7; // illegal is observable, never disguised as IDLE
endcase
end
endmodule
Bench run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It forces unused binary codes 6 and 7 with req low. Faults into legal states are not detected by a default, and synthesis can optimise or re-encode the recovery logic.