A counter is recoded from binary to one-hot to speed up the decode. Outputs match on every simulated sequence, yet the equivalence run reports a failure of the induction step from a state the design can never reach: binary 1 paired with one-hot 0100. The failure is real in the product machine and spurious for the design. This lesson shows where that counterexample comes from and the one invariant that removes it.
This lesson has one job: show that sequential equivalence is induction over a product machine, and that the step needs a state-correspondence invariant.
The product machine instantiates both designs, feeds them identical inputs and reset, and asserts equal outputs every cycle. The harness holds reset at the first step, so the bounded check searches reachable pairs from the reset pair: this is equivalence from reset, not from arbitrary state. The induction step, however, starts from arbitrary pairs: any binary value beside any one-hot value, including pairs no shared stimulus produces. From such a pair the compared outputs can diverge in one step, and the solver reports a counterexample to induction, a CTI, that is unreachable in practice.
The outputs compared here are deliberately coarser than the state: each counter exports only a wrap flag (the count equals 3). That is the realistic situation, since a block exposes outputs, not its state encoding, and it is why the invariant is needed. Had the compared signal been the state map itself, the property would be inductive on its own and there would be nothing to learn.
The fix is a correspondence invariant: a relation the two state spaces always satisfy together, such as the one-hot word equalling one shifted by the binary count. Asserted as a helper, it constrains the step to reachable pairs and the proof closes. The invariant itself must be proved, never assumed: an assumed map would make the proof conditional on a lemma nobody checked.
A 2-bit binary counter and its one-hot twin count enable cycles modulo 4. Without the map, the bounded check from reset passes and the induction step fails: the CTI starts from binary 1 beside one-hot 0100, a pair that reset can never produce (binary 1 is always paired with 0010). Both wrap flags are 0 there, so the pair looks fine, and one enable later binary 2 still gives 0 while one-hot 1000 gives 1. With the map asserted, the same depth proves; the third block rotates the one-hot word by two places instead of one, and fails:
// formal: prove 4 expect unproven slang top cnt_eq define HELPER=0
`define FORMAL
module cnt_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk) if (rst) q <= 2'd0; else if (en) q <= q + 2'd1;
endmodule
module cnt_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= 4'b0001;
else if (en) q <= (BUG == 1) ? {q[1:0], q[3:2]} : {q[2:0], q[3]};
endmodule
module cnt_eq #(parameter HELPER = 1, parameter BUG = 0) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
cnt_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
cnt_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared outputs: each counter's wrap flag (count equals 3), not its state
assign same = ((qb == 2'd3) == qh[3]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_map
always @(*) if (!init) h_map: assert (qh == (4'b0001 << qb));
end endgenerate
`endif
endmodule// formal: prove 4 expect pass slang top cnt_eq
`define FORMAL
module cnt_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk) if (rst) q <= 2'd0; else if (en) q <= q + 2'd1;
endmodule
module cnt_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= 4'b0001;
else if (en) q <= (BUG == 1) ? {q[1:0], q[3:2]} : {q[2:0], q[3]};
endmodule
module cnt_eq #(parameter HELPER = 1, parameter BUG = 0) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
cnt_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
cnt_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared outputs: each counter's wrap flag (count equals 3), not its state
assign same = ((qb == 2'd3) == qh[3]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_map
always @(*) if (!init) h_map: assert (qh == (4'b0001 << qb));
end endgenerate
`endif
endmodule// formal: prove 4 expect fail slang top cnt_eq define BUG=1
`define FORMAL
module cnt_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk) if (rst) q <= 2'd0; else if (en) q <= q + 2'd1;
endmodule
module cnt_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= 4'b0001;
else if (en) q <= (BUG == 1) ? {q[1:0], q[3:2]} : {q[2:0], q[3]};
endmodule
module cnt_eq #(parameter HELPER = 1, parameter BUG = 0) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
cnt_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
cnt_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared outputs: each counter's wrap flag (count equals 3), not its state
assign same = ((qb == 2'd3) == qh[3]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
generate if (HELPER) begin : g_map
always @(*) if (!init) h_map: assert (qh == (4'b0001 << qb));
end endgenerate
`endif
endmoduleStep of the CTI | Binary | One-hot | en | Binary wrap flag | One-hot wrap flag | Compared outputs |
|---|---|---|---|---|---|---|
start (arbitrary pair) | 1 | 0100 | 1 | 0 | 0 | equal: nothing wrong yet |
next | 2 | 1000 | 0 or 1 | 0 | 1 | differ: the step fails |
# not-run: illustrative trace, not executable here
CTI without the map: binary q=1 beside one-hot 0100 (unreachable: reset gives 0/0001, so 1 pairs with 0010)
en=1 -> binary 2 (wrap flag 0), one-hot rotates to 1000 (wrap flag 1) -> compared flags differ
verdict: the step fails from an unreachable pair | fix: assert the map as an invariant
with the map: that pair is excluded -> the step holds -> full proof at the same depth
rotated-by-two twin: the map fails at the first enable after reset, and the wrap flags part laterWhy not simply lengthen the induction window? With en low the machines hold, so the unreachable pair can sit still for any number of cycles while the outputs look equal; the relation, not the window, is what excludes it.
The comparison is outputs only; no internal register is compared by name across the two machines.
Every induction-based pass names its correspondence invariant and shows the invariant proved, not assumed.
A CTI is read as a question about reachability first: is the starting pair reachable from reset on shared inputs?
When the step fails, print the starting pair and ask whether reset plus shared inputs can produce it. If not, the invariant is missing, not the design wrong. Strengthen with the smallest relation that excludes the pair: here one equality between the two state words. If the base case fails instead, the reset states genuinely disagree and no invariant can help. Finally, break the map on purpose (the rotated-by-two twin) and confirm the proof fails: a map that cannot fail is not tied to the design.
Missing invariant. Reset produces binary 0 with one-hot 0001 and both advance together, so that pair is unreachable. Assert the map and rerun before suspecting the counters.