Two passing results in the report prove nothing. The first is vacuity: the trigger never fires, so the rule is never tested. The second is the tautology: the rule is true of every value, so no design can break it. Both pass on the mutant that should kill them. This lesson's one job is the two different exposures: a cover for the trigger, a mutant for the tautology.
Vacuity means the antecedent is never true: a state the machine never reaches, an encoding the decoder never emits, an enable that never rises. The consequent can be anything, including false, and the rule still passes. The exposure is an antecedent cover: reach the trigger, or admit the rule was never tried. A weak sequence that never completes is not vacuity, it is an incomplete attempt with its own window reasoning; do not confuse the two.
Read an unreached cover carefully. A cover not reached within a depth is inconclusive: a longer run might still reach it. It becomes a statement of unreachability only when something else shows the state cannot be reached, for example a proof of an invariant that excludes it. The worked example below does both: the cover is not reached, which is inconclusive on its own, and a one-line invariant is then proved, which turns the suspicion into a fact.
A tautology is true by construction: a three-bit value never exceeds seven, a one-hot check on a signal the encoder guarantees, a bound the type already enforces. The exposure is mutation: break the design in a way the rule should catch, and watch the rule pass anyway. Covers cannot see tautologies, because the trigger fires constantly; only a mutant the rule misses proves it checks nothing.
The machine below cycles through eight states, 0 to 7, and the rule demands something of state nine, which never happens. The property passes, and the cover of the trigger is not reached:
// formal: bmc 8 expect pass slang
`define FORMAL
// fsm_trig: an eight-state machine (states 0 to 7) with a rule about state 9, which never
// happens. a_state9 passes vacuously and c_state9 is its antecedent cover. a_range, st <= 7, is
// the invariant that turns the unreached cover into a proof that state 9 is unreachable.
module fsm_trig (
input wire clk,
input wire rst
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [3:0] st;
always @(posedge clk) begin
if (rst) st <= 4'd0;
else if (st == 4'd7) st <= 4'd0;
else st <= st + 4'd1;
end
wire out_ok = 1'b0;
always @(*) if (!init) a_state9: assert (!(st == 4'd9) || out_ok);
always @(*) if (!init) a_range: assert (st <= 4'd7);
always @(*) if (!init) c_state9: cover (st == 4'd9);
endmodule// formal: cover 8 expect fail slang
`define FORMAL
// fsm_trig: an eight-state machine (states 0 to 7) with a rule about state 9, which never
// happens. a_state9 passes vacuously and c_state9 is its antecedent cover. a_range, st <= 7, is
// the invariant that turns the unreached cover into a proof that state 9 is unreachable.
module fsm_trig (
input wire clk,
input wire rst
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [3:0] st;
always @(posedge clk) begin
if (rst) st <= 4'd0;
else if (st == 4'd7) st <= 4'd0;
else st <= st + 4'd1;
end
wire out_ok = 1'b0;
always @(*) if (!init) a_state9: assert (!(st == 4'd9) || out_ok);
always @(*) if (!init) a_range: assert (st <= 4'd7);
always @(*) if (!init) c_state9: cover (st == 4'd9);
endmoduleNot reached within 8 is inconclusive by itself. Here the reason is the counter, which wraps from 7 to 0. The invariant that the state never exceeds 7 is proved with its base case and its induction step, and it excludes state nine for good, so the unreachability is now a proof and not a hunch:
// formal: prove 4 expect pass slang
`define FORMAL
// fsm_trig: an eight-state machine (states 0 to 7) with a rule about state 9, which never
// happens. a_state9 passes vacuously and c_state9 is its antecedent cover. a_range, st <= 7, is
// the invariant that turns the unreached cover into a proof that state 9 is unreachable.
module fsm_trig (
input wire clk,
input wire rst
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [3:0] st;
always @(posedge clk) begin
if (rst) st <= 4'd0;
else if (st == 4'd7) st <= 4'd0;
else st <= st + 4'd1;
end
wire out_ok = 1'b0;
always @(*) if (!init) a_state9: assert (!(st == 4'd9) || out_ok);
always @(*) if (!init) a_range: assert (st <= 4'd7);
always @(*) if (!init) c_state9: cover (st == 4'd9);
endmoduleThe rule below checks a three-bit value against seven. It passes on the good mirror and on the mutant that inverts every bit, because no three-bit value exceeds seven either way. The real check beside it, output equals input, tells the two apart:
// formal: bmc 4 expect pass slang
`define FORMAL
// taut_check: out mirrors v, or its inverse under BUG=1. p_taut is true by
// construction on both; p_real tells the good design from the mutant.
module taut_check #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [2:0] v,
output wire [2:0] out
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
assign out = (BUG == 1) ? ~v : v;
always @(*) if (!init) begin
p_taut: assert (v <= 3'd7);
p_real: assert (out == v);
end
endmodule// formal: bmc 4 expect fail slang define BUG=1
`define FORMAL
// taut_check: out mirrors v, or its inverse under BUG=1. p_taut is true by
// construction on both; p_real tells the good design from the mutant.
module taut_check #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [2:0] v,
output wire [2:0] out
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
assign out = (BUG == 1) ? ~v : v;
always @(*) if (!init) begin
p_taut: assert (v <= 3'd7);
p_real: assert (out == v);
end
endmoduleIn the second run the failing label is the real check; the tautology still passes in the same run. A suite made only of tautologies would call this mutant a pass.
Every implication-style rule has an antecedent cover, and the report shows it reached: an unreached trigger fails sign-off, not just the rule.
An unreached cover is called inconclusive until a proof or a design argument shows the state cannot happen; only then is it called unreachable.
Every bound is checked against the type width: a comparison the width already decides is a tautology until a mutant proves otherwise.
Weak sequences and vacuity are named separately: an incomplete attempt gets window reasoning, an unfired trigger gets a cover.
Run the cover with the proof, every time, not after it. A passing proof with an unreached antecedent cover is the definition of a vacuous result: fix the trigger or delete the rule, never ship the pass. For suspected tautologies, mutate first and read second: if no mutant in the rule's cone fails it, the rule checks nothing, however often it passes.
No: the cover proves the trigger fires, so the rule was tried. It fails because the design is wrong or the rule is, which the trace then decides. Vacuity is only the case where the trigger never fires at all.