A two-bit binary controller is recoded to one-hot to shorten the critical path, and its datapath flop is clock-gated to save power. Simulation matches on every sequence. The one-to-one comparison still fails, because binary 2 and one-hot 0100 share no bit pattern, and the gated flop holds its value on cycles the reference flop never skips. Both transformations are correct and both need sequential equivalence with the right invariant. This lesson proves the pair and defines the two terms every such proof leans on.
This lesson has one job: show which invariants recoding and gating need, and name which transformations one-to-one comparison cannot cover.
Recoding replaces the state encoding, so the proof needs a state-map invariant: a proved relation saying the two state words always encode the same abstract state, for example one-hot equals one shifted by the binary value. The outputs are then compared through the decode, not bit by bit.
Clock gating replaces always-clocked flops with flops that update only when a gate condition holds. The proof needs the gate condition as its invariant: whenever the gate is shut, loading would not have changed the value, and the flop holds. Two definitions pin down the comparison. Stutter tolerance means the comparison ignores idle cycles where both sides hold state: a finite stretch of no change cannot break it, for example up to 3 idle cycles (illustrative). Latency window means the number of cycles within which a change on one side must appear on the other: a bounded response such as an answer within 2 cycles of the stimulus (illustrative). A gated design stutters relative to its reference; the window says how long it may lag. The example below is exact (window of zero cycles): the gated flop must equal the enabled flop at every cycle.
A 2-bit saturating counter is the reference; the twin counts one-hot. Each exports a saturation flag (the count equals 3), and that flag is the compared output. Without the map the bounded check passes and the step fails: from binary 1 beside one-hot 0100 both flags are 0, and one enable later binary 2 gives 0 while one-hot 1000 gives 1. With the map asserted the pair proves. The broken variant resets the one-hot word to 0100 instead of 0001: the map fails at the first cycle after reset, and the flags part on later enables. A broken map that nobody asserts would pass silently, which is why the map is an assertion, not an assumption:
// formal: prove 5 expect unproven slang top recode_eq define HELPER=0
`define FORMAL
module sat_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk)
if (rst) q <= 2'd0;
else if (en && q != 2'd3) q <= q + 2'd1;
endmodule
module sat_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= (BUG == 1) ? 4'b0100 : 4'b0001;
else if (en && !q[3]) q <= {q[2:0], 1'b0};
endmodule
module recode_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
sat_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
sat_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared output: the saturation flag of each counter (count equals 3)
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 ((4'b0001 << qb) == qh);
end endgenerate
`endif
endmodule// formal: prove 5 expect pass slang top recode_eq
`define FORMAL
module sat_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk)
if (rst) q <= 2'd0;
else if (en && q != 2'd3) q <= q + 2'd1;
endmodule
module sat_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= (BUG == 1) ? 4'b0100 : 4'b0001;
else if (en && !q[3]) q <= {q[2:0], 1'b0};
endmodule
module recode_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
sat_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
sat_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared output: the saturation flag of each counter (count equals 3)
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 ((4'b0001 << qb) == qh);
end endgenerate
`endif
endmodule// formal: prove 5 expect fail slang top recode_eq define BUG=1
`define FORMAL
module sat_bin (
input wire clk, rst, en,
output reg [1:0] q
);
always @(posedge clk)
if (rst) q <= 2'd0;
else if (en && q != 2'd3) q <= q + 2'd1;
endmodule
module sat_hot #(parameter BUG = 0) (
input wire clk, rst, en,
output reg [3:0] q
);
always @(posedge clk)
if (rst) q <= (BUG == 1) ? 4'b0100 : 4'b0001;
else if (en && !q[3]) q <= {q[2:0], 1'b0};
endmodule
module recode_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst, en,
output wire same
);
wire [1:0] qb;
wire [3:0] qh;
sat_bin u_b (.clk(clk), .rst(rst), .en(en), .q(qb));
sat_hot #(.BUG(BUG)) u_h (.clk(clk), .rst(rst), .en(en), .q(qh));
// compared output: the saturation flag of each counter (count equals 3)
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 ((4'b0001 << qb) == qh);
end endgenerate
`endif
endmoduleThe reference is an ordinary enabled flop. The twin is data-driven gated: its gate opens only when the enable is high and the incoming data differs from the stored value, since loading an equal value changes nothing. The proof model has one clock, so the gate is represented by the enable condition it implements. Three assertions carry it: the outputs are equal; the gate condition (a shut gate with the enable high means the data equals the stored value); and hold (when the gate was shut in the previous cycle and there was no reset, the stored value did not change). The injected twin builds its gate from a stale enable, one cycle old. Its hold assertion still passes, because a shut gate does hold (measured: with only the hold assertion kept, the stale-enable twin shows no counterexample to depth 10, a bounded result); the gate-condition assertion and the output comparison each fail on their own. The hold alone would have signed off a wrong gate. Be plain about what the gate-condition assertion is: it restates the gate's definition in terms of the enable and the data, so on a correct gate it cannot fail, and it earns its place only because it fails when the gate is built from the wrong enable. It is a specification check on the gate, not independent evidence that gating is safe, and this one-clock model has no real gated clock, so the pitfall below (an assertion that stops evaluating on a gated clock) is stated, not demonstrated:
// formal: prove 4 expect pass slang top gate_eq
`define FORMAL
module flop_en (
input wire clk, rst, en,
input wire [7:0] d,
output reg [7:0] q
);
always @(posedge clk) if (rst) q <= 8'd0; else if (en) q <= d;
endmodule
module flop_gate #(parameter BUG = 0) (
input wire clk, rst, en,
input wire [7:0] d,
output reg [7:0] q,
output wire gate_ok
);
// data-driven gating: the flop is only enabled when loading would change it.
// BUG=1 builds the gate from a stale (one cycle old) enable.
reg en_q;
always @(posedge clk) en_q <= en;
wire en_use = (BUG == 1) ? en_q : en;
assign gate_ok = en_use && (d != q);
always @(posedge clk) if (rst) q <= 8'd0; else if (gate_ok) q <= d;
endmodule
module gate_eq #(parameter BUG = 0) (
input wire clk, rst, en,
input wire [7:0] d,
output wire same
);
wire [7:0] q1, q2;
wire g;
flop_en u_e (.clk(clk), .rst(rst), .en(en), .d(d), .q(q1));
flop_gate #(.BUG(BUG)) u_g (.clk(clk), .rst(rst), .en(en), .d(d), .q(q2), .gate_ok(g));
assign same = (q1 == q2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [7:0] q2_prev;
reg g_prev, rst_prev;
always @(posedge clk) begin q2_prev <= q2; g_prev <= g; rst_prev <= rst; end
// equal outputs, the gate condition, and hold while the gate was shut
always @(*) if (!init) a_equiv: assert (same);
always @(*) if (!init) h_gate: assert (g || !en || (d == q2));
always @(*) if (!init && !rst_prev && !g_prev) h_hold: assert (q2 == q2_prev);
`endif
endmodule// formal: prove 4 expect fail slang top gate_eq define BUG=1
`define FORMAL
module flop_en (
input wire clk, rst, en,
input wire [7:0] d,
output reg [7:0] q
);
always @(posedge clk) if (rst) q <= 8'd0; else if (en) q <= d;
endmodule
module flop_gate #(parameter BUG = 0) (
input wire clk, rst, en,
input wire [7:0] d,
output reg [7:0] q,
output wire gate_ok
);
// data-driven gating: the flop is only enabled when loading would change it.
// BUG=1 builds the gate from a stale (one cycle old) enable.
reg en_q;
always @(posedge clk) en_q <= en;
wire en_use = (BUG == 1) ? en_q : en;
assign gate_ok = en_use && (d != q);
always @(posedge clk) if (rst) q <= 8'd0; else if (gate_ok) q <= d;
endmodule
module gate_eq #(parameter BUG = 0) (
input wire clk, rst, en,
input wire [7:0] d,
output wire same
);
wire [7:0] q1, q2;
wire g;
flop_en u_e (.clk(clk), .rst(rst), .en(en), .d(d), .q(q1));
flop_gate #(.BUG(BUG)) u_g (.clk(clk), .rst(rst), .en(en), .d(d), .q(q2), .gate_ok(g));
assign same = (q1 == q2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [7:0] q2_prev;
reg g_prev, rst_prev;
always @(posedge clk) begin q2_prev <= q2; g_prev <= g; rst_prev <= rst; end
// equal outputs, the gate condition, and hold while the gate was shut
always @(*) if (!init) a_equiv: assert (same);
always @(*) if (!init) h_gate: assert (g || !en || (d == q2));
always @(*) if (!init && !rst_prev && !g_prev) h_hold: assert (q2 == q2_prev);
`endif
endmoduleTransformation | Method | Invariant |
|---|---|---|
Resynthesis, same encoding | One-to-one comparison | None: names usually match |
Constant propagation, tie-offs | One-to-one with aligned constants | Constants listed in the setup |
Recoding (binary to one-hot) | Sequential equivalence | State-map invariant, proved |
Retiming across logic | Sequential equivalence | Cut invariant across the moved cut |
Clock gating | Sequential equivalence or dedicated gating mode | Gate condition; hold while gated |
Stutter tolerance and latency window are defined with numbers before first use: how many idle cycles, how many cycles of lag.
The state map is an asserted invariant with its own proof, and a broken-map variant is shown to fail.
The table above is filled per transformation: anything below the recoding row is never claimed for one-to-one comparison.
Mutate the map, not the design: change one reset value or one rotation direction and confirm the map invariant fires before the output comparison does. For gating, hold the enable low for a long stretch and confirm stability, then pulse it once and confirm the load lands within the window. A gating failure that only the outputs and the gate condition catch, never the hold, points at the gate timing rather than the gate function.
The proof is conditional on an unchecked lemma: a wrong map assumed true proves anything. Assert the map, show it holds from reset, and show a broken map fails.