A proof failed on a correct skid stage with a trace that began with the accepted and delivered counters disagreeing with the words held, so the conservation check failed in its first checked cycle. The harness had left every register free and said nothing about reset. The fix was one line: assume reset at step 0. Every harness here is built on that line; this lesson shows what breaks without it and with too much of it.
Job of this lesson: show that an unconstrained start is any state, build the one-reset-sequence harness, and demonstrate the two failure modes at the edges: no reset assumption, and reset held forever.
The engine treats each initial register as a free choice unless the harness constrains it. Step 0 is a power-up state with arbitrary contents and reset asserted; step 1 is the first state after a reset edge. Assertions are guarded by !init, so step 0 is never checked; an unguarded assertion fails at step 0 on the arbitrary start. Two mistakes bracket the right answer.
Harness | Line in the file | Result on the skid stage |
|---|---|---|
Reset once, at step 0 |
| Proves; stall and skid covers are reached. |
No reset assumption | line removed | The good design fails at step 1, the first checked step. |
Reset in every step |
| Everything proves, including the buggy design; the traffic cover is unreachable. |
The design is a valid/ready skid stage with 18 state bits and 3 reachable control states. The good harness proves at depth 4, and the covers confirm real traffic: a stall and a skid use are reached within depth 5.
// formal: prove 4 expect pass slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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// formal: cover 5 expect reached slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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
endmoduleThe planted bug drops a word under backpressure: the skid never captures, so a second word is accepted into nowhere and accepted-minus-delivered no longer equals the words held. It fails at step 3 with the correct harness.
// formal: bmc 4 expect fail slang top hs_bridge define BUG=1
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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
endmoduleNow remove the reset assumption. The good design fails at depth 2: step 0 is any state, so the counters can disagree with the registers they count, and step 1, the first checked step, shows it (depth 1 checks only the guarded step 0 and passes). Three properties fail; the trace below is one the solver returned.
// formal: bmc 2 expect fail slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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;
// no reset assumption at all: step 0 is any state
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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
endmoduleStep | rst | ovld | svld | acc | dlv | Note |
|---|---|---|---|---|---|---|
0 | 0 | 0 | 0 | 15 | 0 | Arbitrary start; nothing held, yet the counters disagree. |
1 | - | 1 | 0 | 0 | 0 | A word was accepted and acc wrapped to 0: acc - dlv = 0, one word held, so a_conserve fails. |
Now hold reset in every step. Every assertion proves, the buggy design passes too (bounded to 8), and the stall cover cannot be reached: under permanent reset nothing is accepted. The assumption list shows why: assume (rst) for all steps.
// formal: prove 4 expect pass slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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;
// reset assumed in every cycle, not only at step 0
always @(*) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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// formal: bmc 8 expect pass slang top hs_bridge define BUG=1
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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;
// reset assumed in every cycle, not only at step 0
always @(*) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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// formal: cover 5 expect fail slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
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
// output holds; a new input is parked in the skid register
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
// output empty or consumed this cycle
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;
// reset assumed in every cycle, not only at step 0
always @(*) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
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); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
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));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* 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; // the tracked word has been accepted and not yet delivered
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
// where the tracked word lives: output stage if it is next to leave, else skid
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
// ---- covers ----
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“Not reached within 5” is inconclusive in general; here the assumption explains it, and the earlier run reaches the same cover.
One reset sequence at the start, the init guard on every assertion, and the reset assumption listed once, not held in every step.
Traffic covers are reached; an unreachable cover fails the harness, not just the property.
Read the first counterexample's first step: illegal register values there mean the harness, not the design, is wrong. Check the polarity of the reset assumption against the documented reset, and cover the first post-reset activity.
A traffic cover: no activity can happen under permanent reset, so the cover is unreachable, and a planted bug passes as well.
Harness bug: that start is not a state reset can produce. Add the reset assumption before touching the design.