Coverage says a state was never visited. That is either dead code to remove or the most important case to test, and the cover alone cannot tell which: a cover not reached within a bound is inconclusive, never proof of unreachability. The symptom of confusing the two is a waiver that says cannot happen with no evidence, signed off two releases before the corner case arrives. This lesson shows the full ladder: cover per state, read the miss, prove the invariant, and see the invariant fail on a variant that does reach the state.
Cover every state and every branch, so the interesting events are witnessed and the silent ones are named. For the unreached one, write the unreachability as an invariant over the state register and prove it inductively: the base case holds from reset, the step holds because no transition targets the dead state. Only the proven invariant turns the unreached cover from inconclusive into unreachable. The same ladder applies to branches: a default that never fires needs either a test or an invariant saying why.
The lesson-local machine has three live states and one dead state with no incoming transition. One module serves every run below. The invariant proves the dead state never holds; the first cover run witnesses the live states, and the second run covers the dead state alone, because a cover run needs every cover in it to be reached. The script after the blocks enumerates the same reachability explicitly, so the invariant and the enumeration agree:
// formal: prove 4 expect pass slang top fsm_dead
`define FORMAL
module fsm_dead #(parameter BUG = 0, parameter COVERS = 0) (
input wire clk,
input wire rst,
input wire go,
input wire done,
output reg [1:0] state
);
localparam IDLE = 2'd0, BUSY = 2'd1, FINISH = 2'd2, DEAD = 2'd3;
always @(posedge clk) begin
if (rst) state <= IDLE;
else case (state)
IDLE: if (go) state <= BUSY;
BUSY: if (done) state <= (BUG == 1 && go) ? DEAD : FINISH;
FINISH: state <= IDLE;
default: state <= IDLE;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the dead-state cover run has no assertion in it: in a cover run an assertion would act as a constraint
generate if (COVERS == 0) begin : g_live
always @(*) if (!init) begin
d_never_dead: assert (state != DEAD);
c_idle: cover (state == IDLE);
c_busy: cover (state == BUSY);
c_finish: cover (state == FINISH);
end
end else begin : g_dead
always @(*) if (!init) c_dead: cover (state == DEAD);
end endgenerate
`endif
endmodule// formal: cover 6 expect reached slang top fsm_dead
`define FORMAL
module fsm_dead #(parameter BUG = 0, parameter COVERS = 0) (
input wire clk,
input wire rst,
input wire go,
input wire done,
output reg [1:0] state
);
localparam IDLE = 2'd0, BUSY = 2'd1, FINISH = 2'd2, DEAD = 2'd3;
always @(posedge clk) begin
if (rst) state <= IDLE;
else case (state)
IDLE: if (go) state <= BUSY;
BUSY: if (done) state <= (BUG == 1 && go) ? DEAD : FINISH;
FINISH: state <= IDLE;
default: state <= IDLE;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the dead-state cover run has no assertion in it: in a cover run an assertion would act as a constraint
generate if (COVERS == 0) begin : g_live
always @(*) if (!init) begin
d_never_dead: assert (state != DEAD);
c_idle: cover (state == IDLE);
c_busy: cover (state == BUSY);
c_finish: cover (state == FINISH);
end
end else begin : g_dead
always @(*) if (!init) c_dead: cover (state == DEAD);
end endgenerate
`endif
endmodule// formal: cover 6 expect fail slang top fsm_dead define COVERS=1
`define FORMAL
module fsm_dead #(parameter BUG = 0, parameter COVERS = 0) (
input wire clk,
input wire rst,
input wire go,
input wire done,
output reg [1:0] state
);
localparam IDLE = 2'd0, BUSY = 2'd1, FINISH = 2'd2, DEAD = 2'd3;
always @(posedge clk) begin
if (rst) state <= IDLE;
else case (state)
IDLE: if (go) state <= BUSY;
BUSY: if (done) state <= (BUG == 1 && go) ? DEAD : FINISH;
FINISH: state <= IDLE;
default: state <= IDLE;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the dead-state cover run has no assertion in it: in a cover run an assertion would act as a constraint
generate if (COVERS == 0) begin : g_live
always @(*) if (!init) begin
d_never_dead: assert (state != DEAD);
c_idle: cover (state == IDLE);
c_busy: cover (state == BUSY);
c_finish: cover (state == FINISH);
end
end else begin : g_dead
always @(*) if (!init) c_dead: cover (state == DEAD);
end endgenerate
`endif
endmoduleThe last run is the miss: the dead-state cover is not reached within 6. On its own that result is inconclusive; only the proven invariant above promotes it to unreachable. Never present the unreached cover as the proof. The failing partner for the invariant is a variant with a transition into the dead state. The invariant then fails, and the dead-state cover, run on the same variant, is reached: a witness, not a miss:
// formal: bmc 6 expect fail slang top fsm_dead define BUG=1
`define FORMAL
module fsm_dead #(parameter BUG = 0, parameter COVERS = 0) (
input wire clk,
input wire rst,
input wire go,
input wire done,
output reg [1:0] state
);
localparam IDLE = 2'd0, BUSY = 2'd1, FINISH = 2'd2, DEAD = 2'd3;
always @(posedge clk) begin
if (rst) state <= IDLE;
else case (state)
IDLE: if (go) state <= BUSY;
BUSY: if (done) state <= (BUG == 1 && go) ? DEAD : FINISH;
FINISH: state <= IDLE;
default: state <= IDLE;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the dead-state cover run has no assertion in it: in a cover run an assertion would act as a constraint
generate if (COVERS == 0) begin : g_live
always @(*) if (!init) begin
d_never_dead: assert (state != DEAD);
c_idle: cover (state == IDLE);
c_busy: cover (state == BUSY);
c_finish: cover (state == FINISH);
end
end else begin : g_dead
always @(*) if (!init) c_dead: cover (state == DEAD);
end endgenerate
`endif
endmodule// formal: cover 6 expect reached slang top fsm_dead define COVERS=1 define BUG=1
`define FORMAL
module fsm_dead #(parameter BUG = 0, parameter COVERS = 0) (
input wire clk,
input wire rst,
input wire go,
input wire done,
output reg [1:0] state
);
localparam IDLE = 2'd0, BUSY = 2'd1, FINISH = 2'd2, DEAD = 2'd3;
always @(posedge clk) begin
if (rst) state <= IDLE;
else case (state)
IDLE: if (go) state <= BUSY;
BUSY: if (done) state <= (BUG == 1 && go) ? DEAD : FINISH;
FINISH: state <= IDLE;
default: state <= IDLE;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the dead-state cover run has no assertion in it: in a cover run an assertion would act as a constraint
generate if (COVERS == 0) begin : g_live
always @(*) if (!init) begin
d_never_dead: assert (state != DEAD);
c_idle: cover (state == IDLE);
c_busy: cover (state == BUSY);
c_finish: cover (state == FINISH);
end
end else begin : g_dead
always @(*) if (!init) c_dead: cover (state == DEAD);
end endgenerate
`endif
endmodulestates = {"IDLE": 0, "BUSY": 1, "FINISH": 2, "DEAD": 3}
def step(state, go, done, bug):
if state == 0:
return 1 if go else 0
if state == 1:
if done:
return 3 if (bug and go) else 2
return 1
if state == 2:
return 0
return 0
def reachable(bug):
reached, frontier = {0}, {0}
while frontier:
nxt = {step(s, go, done, bug) for s in frontier for go in (0, 1) for done in (0, 1)} - reached
reached |= nxt
frontier = nxt
return reached
assert reachable(False) == {0, 1, 2}, reachable(False)
assert 3 not in reachable(False)
assert reachable(True) == {0, 1, 2, 3}, "the variant reaches the dead state"
print("PASS: reachable states are IDLE, BUSY, FINISH; DEAD is unreachable unless a transition into it exists")A case statement that does not assign its output in every branch creates a latch: the output keeps its old value for the unassigned selector, which is a hidden extra state. The property is that the output is a function of the current inputs only, written here as an equality with the intended function. The complete version proves. The variant with the default branch missing fails at the first checked step, with the selector at the unassigned value and the latch holding whatever it held:
// formal: prove 4 expect pass slang top comb_case
`define FORMAL
module comb_case #(parameter BUG = 0) (
input wire clk,
input wire [1:0] sel,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y
);
always @(*) begin
case (sel)
2'd0: y = a;
2'd1: y = b;
2'd2: y = c;
default: if (BUG == 0) y = 8'h00; // BUG 1: no assignment, so y holds its old value
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (!init)
a_complete: assert (y == ((sel == 2'd0) ? a : (sel == 2'd1) ? b : (sel == 2'd2) ? c : 8'h00));
`endif
endmodule// formal: bmc 4 expect fail slang top comb_case define BUG=1
`define FORMAL
module comb_case #(parameter BUG = 0) (
input wire clk,
input wire [1:0] sel,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y
);
always @(*) begin
case (sel)
2'd0: y = a;
2'd1: y = b;
2'd2: y = c;
default: if (BUG == 0) y = 8'h00; // BUG 1: no assignment, so y holds its old value
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (!init)
a_complete: assert (y == ((sel == 2'd0) ? a : (sel == 2'd1) ? b : (sel == 2'd2) ? c : 8'h00));
`endif
endmoduleEvery state and branch has a cover, and every unreached cover has either a test plan entry or a proven invariant.
The unreachability claim cites the invariant and its induction result, never the cover miss alone.
Combinational completeness is checked: no inferred latch hiding an extra state in an unassigned branch.
A newly unreached cover first asks whether the bound suffices: lengthen it and re-run before claiming anything. Then check the stimulus freedom: a tied input can hide a state the design reaches in the system. Only then write the invariant, prove it, and file the waiver with the proof attached.
The models differ: the simulation drives inputs or sequences the proof excluded, or the RTL changed after the proof. Check the assumption list and the revision the proof ran on before doubting the invariant.