Match the output style to its destination. Boundaries want registered outputs, and local fast paths want Mealy.
Situation | Pick |
|---|---|
Output crosses a block or chip boundary | Specify receiver timing/latency; register where the interface requires it |
Output crosses a clock-domain boundary | Use the appropriate synchronization or handshake protocol; source registration alone is insufficient |
Output must not glitch | Registered output, or an explicitly justified hazard-free decode; Moore alone is insufficient |
Local control signal that must react this very cycle (e.g. a handshake that cannot add latency) | Mealy |
State count must be tiny (very small block) | Mealy |
You are unsure | Moore: simpler timing, easier to verify |
Reset state is legal and outputs are known after reset.
Intended states are reachable through legal inputs. Progress holds under the specified environment assumptions: e.g. a WAIT_ACK state progresses only if an acknowledgement arrives. Terminal/error states may intentionally absorb inputs until reset; reject prohibited lock-up, not every non-returning path.
Outputs are assigned a default at the top of the combinational block, so no latch is inferred.
For Mealy outputs: inputs are stable before the clock edge in the testbench, and the check happens after settling.
Compare against a reference or a cycle-accurate model; for FSMs with small input alphabets, test every state × input combination.
Check illegal states (see state encoding): what happens after a bit-flip?
The check below reaches every state through legal inputs rather than forcing the state register. Forcing is quicker, but it can hide reset and encoding bugs, because it visits states the real machine might never enter.
Outputs are fully defined at the specified observation points, and intended states are reachable. Also check the specified progress/terminal behavior under explicit environment assumptions and the illegal-state policy; unconditional return to reset is not a universal requirement.
The listing reaches all three states through legal prefixes and checks all six state/input combinations: Moore y before the edge must reflect the current state, then state and y after the edge must reflect the transition table. Coverage records the actually observed pre-edge state/input pair.
// Exhaustive state x input check for the two-ones detector.
// Reach each state through legal inputs, apply each input, and compare with the transition table.
module det_probe (input logic clk, rst_n, x, output logic y, output logic [1:0] st);
typedef enum logic [1:0] {S0, S1, S11} state_t;
state_t state, next;
always_comb begin
next = state;
unique case (state)
S0: if (x) next = S1;
S1: if (x) next = S11; else next = S0;
S11: if (!x) next = S0;
default: next = S0;
endcase
end
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) state <= S0; else state <= next;
assign y = (state == S11);
assign st = state;
endmodule