The first counterexample a new proof returns often starts in a state the design cannot reach: arbitrary register values with reset asserted one cycle too late, or a state no reset sequence produces. The two-copy harness turns that annoyance into the proof: run two copies of the design with different free initial values through the same reset sequence and the same inputs, and assert their observable outputs agree afterwards. If they disagree, either a register misses reset or the assertion watches unreset storage.
Build the harness with both copies in one module so the proof sees both at once. Constrain only the reset sequence at the start, leave every other initial value free and different between the copies, drive identical inputs, and compare after the reset cycle. Compare resettable control, valid and ready, not unreset data storage: the data registers of the handshake stage are correctly unreset, and comparing them would fail a correct design for the wrong reason.
The harness below instantiates the handshake stage twice with identical inputs and asserts the two copies agree on valid and ready at every cycle after a non-reset cycle. The proof passes: the control registers are reset, and the free initial values of the data registers cannot leak into valid or ready. The second harness does the same for the register block, comparing what every address reads in the cycle after reset:
// formal: prove 4 expect pass slang top twocopy
`define FORMAL
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
a_no_ready_comb: assert (in_ready == !svld);
end
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
// the running stage with the reset clause of its skid-valid flop removed, properties off
module hs_bridge_nr #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
end else if (stalled) begin
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
endmodule
module twocopy #(parameter MUT = 0) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready
);
wire in_ready_a, out_valid_a, in_ready_b, out_valid_b;
wire [7:0] out_data_a, out_data_b;
hs_bridge u_a (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_a),
.in_data(in_data), .out_valid(out_valid_a), .out_ready(out_ready),
.out_data(out_data_a));
generate if (MUT == 0) begin : g_good
hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_b),
.in_data(in_data), .out_valid(out_valid_b), .out_ready(out_ready),
.out_data(out_data_b));
end else begin : g_mut
hs_bridge_nr u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_b),
.in_data(in_data), .out_valid(out_valid_b), .out_ready(out_ready),
.out_data(out_data_b));
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
d_valid: assert (out_valid_a == out_valid_b);
d_ready: assert (in_ready_a == in_ready_b);
end
`endif
endmodule// formal: prove 4 expect pass slang top twocopy_csr
`define FORMAL
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status;
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0])
: (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
always @(posedge clk) if (!init) begin
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule
// the register block with the reset clause of CTRL removed, properties off
module csr_block_nr #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status;
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0])
: (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
endmodule
module twocopy_csr #(parameter MUT = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err
);
wire [7:0] rdata_a, rdata_b;
csr_block u_a (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_a));
generate if (MUT == 0) begin : g_good
csr_block u_b (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_b));
end else begin : g_mut
csr_block_nr u_b (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_b));
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// after the reset sequence every register reads the same in both copies, whatever the free initial values were
always @(posedge clk) if (!init && $past(rst)) begin
d_rdata: assert (rdata_a == rdata_b);
end
`endif
endmoduleThe failing partner is the same harness around a copy of the handshake stage in which the reset clause of the skid-valid flop is removed, with the stage's own properties switched off so only the harness judges. Copy B starts with its skid flag set and the reset does not clear it, so the stage drains a skid word no input wrote: valid rises in copy B and not in copy A:
Step | rst | skid valid A / B |
| Outcome |
|---|---|---|---|---|
0 | 1 | 0 / 1 (arbitrary) | 0 / 1 | reset cycle, not checked; B's skid flag survives the reset |
1 | 0 | 0 / 1 | 0 / 0 | B drains its skid word |
2 | 0 | 0 / 0 | 0 / 1 | B shows a valid word that was never sent |
3 | - | - | - | counterexample: |
// formal: bmc 8 expect fail slang top twocopy define MUT=1
`define FORMAL
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
a_no_ready_comb: assert (in_ready == !svld);
end
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
// the running stage with the reset clause of its skid-valid flop removed, properties off
module hs_bridge_nr #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
end else if (stalled) begin
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
endmodule
module twocopy #(parameter MUT = 0) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready
);
wire in_ready_a, out_valid_a, in_ready_b, out_valid_b;
wire [7:0] out_data_a, out_data_b;
hs_bridge u_a (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_a),
.in_data(in_data), .out_valid(out_valid_a), .out_ready(out_ready),
.out_data(out_data_a));
generate if (MUT == 0) begin : g_good
hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_b),
.in_data(in_data), .out_valid(out_valid_b), .out_ready(out_ready),
.out_data(out_data_b));
end else begin : g_mut
hs_bridge_nr u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready_b),
.in_data(in_data), .out_valid(out_valid_b), .out_ready(out_ready),
.out_data(out_data_b));
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
d_valid: assert (out_valid_a == out_valid_b);
d_ready: assert (in_ready_a == in_ready_b);
end
`endif
endmoduleRoot cause: a flop on the control path with no reset clause, so the state after reset depends on the free initial value. Fix the RTL, not the harness: pinning the initial value would prove the harness. The register block has the same failing partner: a copy whose CTRL register has no reset clause reads a different value from copy A at the control offset in the cycle after reset:
// formal: bmc 4 expect fail slang top twocopy_csr define MUT=1
`define FORMAL
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status;
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0])
: (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
always @(posedge clk) if (!init) begin
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule
// the register block with the reset clause of CTRL removed, properties off
module csr_block_nr #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status;
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0])
: (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
endmodule
module twocopy_csr #(parameter MUT = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err
);
wire [7:0] rdata_a, rdata_b;
csr_block u_a (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_a));
generate if (MUT == 0) begin : g_good
csr_block u_b (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_b));
end else begin : g_mut
csr_block_nr u_b (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata_b));
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// after the reset sequence every register reads the same in both copies, whatever the free initial values were
always @(posedge clk) if (!init && $past(rst)) begin
d_rdata: assert (rdata_a == rdata_b);
end
`endif
endmoduleStep | rst | address | CTRL in copy A / B | Outcome |
|---|---|---|---|---|
0 | 1 | - | free / free | reset cycle, not checked; B has no reset clause for CTRL |
1 | 0 | 0 (CTRL) | 0x00 / 0x01 | counterexample: |
The lesson-local pair below is the same idea on a two-bit counter whose copy B has no reset clause on its low bit. The high bit is reset, the low bit keeps its free initial value, so the copies differ from the first cycle after reset whether or not the counter runs. The correct variant proves; the bounded run to 3 passes, because the clocked check judges one step after the state, and the run to 4 finds it. A depth one short would have called the bug clean:
// formal: prove 4 expect pass slang top detpair define BUG=0
module detpair #(parameter BUG = 1) (
input wire clk,
input wire rst,
input wire en,
output wire [1:0] cnt_a,
output wire [1:0] cnt_b
);
reg [1:0] ra, rb;
assign cnt_a = ra;
assign cnt_b = rb;
always @(posedge clk) begin
if (rst) begin
ra <= 2'b00;
rb[1] <= 1'b0;
if (BUG == 0) rb[0] <= 1'b0; // BUG 1: the low bit of copy B has no reset clause
end else if (en) begin
ra <= ra + 2'd1;
rb <= rb + 2'd1;
end
end
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) d_equal: assert (cnt_a == cnt_b);
endmoduleStep | rst |
|
| Outcome |
|---|---|---|---|---|
0 | 1 | 0x0 (arbitrary) | 0x1 (arbitrary) | reset cycle, not checked |
1 | 0 | 0x0 | 0x1 | A reset to 00; B's high bit reset, its low bit kept at 1 |
2 | 0 | 0x0 | 0x1 | the copies still differ |
3 | - | - | - | counterexample: |
// formal: bmc 3 expect pass slang top detpair
module detpair #(parameter BUG = 1) (
input wire clk,
input wire rst,
input wire en,
output wire [1:0] cnt_a,
output wire [1:0] cnt_b
);
reg [1:0] ra, rb;
assign cnt_a = ra;
assign cnt_b = rb;
always @(posedge clk) begin
if (rst) begin
ra <= 2'b00;
rb[1] <= 1'b0;
if (BUG == 0) rb[0] <= 1'b0; // BUG 1: the low bit of copy B has no reset clause
end else if (en) begin
ra <= ra + 2'd1;
rb <= rb + 2'd1;
end
end
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) d_equal: assert (cnt_a == cnt_b);
endmodule// formal: bmc 4 expect fail slang top detpair
module detpair #(parameter BUG = 1) (
input wire clk,
input wire rst,
input wire en,
output wire [1:0] cnt_a,
output wire [1:0] cnt_b
);
reg [1:0] ra, rb;
assign cnt_a = ra;
assign cnt_b = rb;
always @(posedge clk) begin
if (rst) begin
ra <= 2'b00;
rb[1] <= 1'b0;
if (BUG == 0) rb[0] <= 1'b0; // BUG 1: the low bit of copy B has no reset clause
end else if (en) begin
ra <= ra + 2'd1;
rb <= rb + 2'd1;
end
end
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) d_equal: assert (cnt_a == cnt_b);
endmoduleThe script below models the counter explicitly: every initial state of the second copy goes through the same reset cycle and the same enable sequence, and the end states must all agree with copy A. The correct counter ends every run in one state. The variant with the unreset low bit does not, and the script names a witness initial state:
def run(init, enables, reset_low_bit):
s = init
for t, en in enumerate(enables):
if t == 0: # the reset cycle
high = 0
low = 0 if reset_low_bit else s & 1
s = (high << 1) | low
elif en:
s = (s + 1) % 4
return s
enables = [1, 0, 1, 1, 0]
reference = run(0, enables, True)
ends_good = {run(i, enables, True) for i in range(4)}
assert ends_good == {reference}, ends_good
ends_bug = {run(i, enables, False) for i in range(4)}
assert len(ends_bug) == 2 and reference in ends_bug, ends_bug
witness = [i for i in range(4) if run(i, enables, False) != reference][0]
assert witness & 1 == 1, "the diverging initial states are the ones with the low bit set"
print("PASS: with the reset the copies end in one state; with the unreset low bit initial state", witness, "diverges")The harness compares after the reset cycle, never during it, and the comparison scope excludes correctly-unreset storage.
Initial values are free, not constrained to hide the defect: the only assumption is the reset sequence itself.
A determinism failure is fixed in the RTL reset structure, and the fix is confirmed by the same harness. The failing partner is run, not described.
First ask whether the compared signals are meant to be reset at all: data paths and memories are legitimately unreset, and comparing them is a harness bug. Narrow the comparison to control and re-run before touching the RTL; a failure on control names the flop, so check its reset clause.
Yes for control: the data registers are unreset by design, and nothing has been written yet. Compare data only after a write, which is the data-integrity lesson's job, not this one's.