A hold property failed at step 2 on a correct skid stage, pointing at a cycle where nothing had happened yet. The property compared the output with its previous value, but the previous cycle was the power-up step with arbitrary values: there was no yesterday. The repair was a one-term gate. Every property that looks back needs it.
Job of this lesson: show that past values have no real history in the first cycles, gate them, and re-qualify the gate after a mid-run reset.
A one-cycle look-back reads the previous cycle. In the first cycles the previous cycle is the reset cycle with whatever inputs it had, so the comparison fails falsely or passes silently on arbitrary history. The pattern guards every history property twice: the harness skips step 0, and the property skips the cycle after reset with a past of reset. For deeper history a counter of clean cycles since reset does the same, and it must clear on every reset, not only the first.
The third argument of the past function is a gating expression, not a window: $past(x, 1, 8) reads one cycle back, exactly like $past(x, 1), because the constant 8 is just a true gate. A check over the last N cycles needs a shift register or a counter.
// not-run: the open front end rejects the gating argument of the past function
// assert (req || $past(req, 1, 8) == ...); // NOT a window of 8 cycles: same as $past(req, 1)The skid stage's hold checks (a stalled output keeps valid and data) read $past. With the gate they prove:
// 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
endmoduleRemove the gate and the good design fails at step 2 (depth 3; at depth 2 it passes). The solver's trace: at step 0, a power-up state, the output is valid and stalled; reset empties the output at step 1; the hold check compares step 1 with step 0, sees a stalled word vanish, and reports it at step 2.
How to read it: one slot is one step, so slot 1 is step 0. In step 0 out_valid is high and out_ready is low: a stalled word, the power-up state the solver chose (the testbench starts the stage in that state). rst is high in step 0, so the first clock edge empties the output and out_valid reads 0 in step 1. Between step 0 and step 1 a stalled valid has vanished, which is what the hold check looks for. ungated_fail is the result of that check without the history gate: it is 0 in step 1 and 1 in step 2, one step after the comparison it judges, which is where the proof tool reports the failure. gated_fail is the same check with the past-of-reset term: it is 0 in every slot, because the term switches the comparison off in the step after a reset step. rst is high again in step 2, and out_valid reads 1 in step 2 and 0 in step 3.
// formal: bmc 3 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;
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) 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
endmoduleIn the concurrent Boolean form that the front end named in the header accepts, disable iff (rst || init) alone is not the gate: it switches the property off while reset is high, but the first cycle after reset is not a reset cycle. The gate is $past(rst) || inside the property. Same check, two forms:
// 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 ----
a_valid_hold: assert property (@(posedge clk) disable iff (rst || init) $past(rst) || !($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert property (@(posedge clk) disable iff (rst || init) $past(rst) || !($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ---- 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 3 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;
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 ----
a_valid_hold: assert property (@(posedge clk) disable iff (rst || init) !($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert property (@(posedge clk) disable iff (rst || init) !($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ---- 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
endmoduleA mid-run reset needs the same care. hist counts clean cycles since the last reset edge, and the history read is judged only when hist is not 0. If a later reset does not clear hist, the property compares a post-reset output with pre-reset history. Both versions below are the same file with BUG changed; the bug variant fails at depth 5 and passes at depth 4.
// formal: prove 4 expect pass slang top hold_demo
`define FORMAL
module hold_demo #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q
);
always @(posedge clk) if (rst) q <= 4'd0; else if (en) q <= d;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since the last reset edge and saturates at 2
reg [1:0] hist = 2'd0;
always @(posedge clk) begin
if (init || (rst && BUG == 0)) hist <= 2'd0; // BUG 1: later resets do not clear it
else if (hist != 2'd2) hist <= hist + 2'd1;
end
// $past is read only when the previous cycle was a clean one (hist is not 0)
always @(posedge clk) if (!init && hist != 2'd0) a_hold: assert ($past(en) || q == $past(q));
`endif
endmodule// formal: bmc 5 expect fail slang top hold_demo define BUG=1
`define FORMAL
module hold_demo #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire en,
input wire [3:0] d,
output reg [3:0] q
);
always @(posedge clk) if (rst) q <= 4'd0; else if (en) q <= d;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since the last reset edge and saturates at 2
reg [1:0] hist = 2'd0;
always @(posedge clk) begin
if (init || (rst && BUG == 0)) hist <= 2'd0; // BUG 1: later resets do not clear it
else if (hist != 2'd2) hist <= hist + 2'd1;
end
// $past is read only when the previous cycle was a clean one (hist is not 0)
always @(posedge clk) if (!init && hist != 2'd0) a_hold: assert ($past(en) || q == $past(q));
`endif
endmoduleLast, the window: “req was high in at least one of the last three cycles”, written once with a shift register and once with two $past calls, must agree. The mutant that uses a single $past(req), which is what the gating argument would have given, disagrees.
// formal: prove 4 expect pass slang top window_demo
`define FORMAL
module window_demo (
input wire clk,
input wire rst,
input wire req
);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] recent; // recent[i] is req seen i+1 cycles ago
always @(posedge clk) recent <= rst ? 3'd0 : {recent[1:0], req};
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 2'd0; else if (hist != 2'd2) hist <= hist + 2'd1;
always @(posedge clk) if (!init && hist == 2'd2) a_window: assert ((req || recent[0] || recent[1]) == (req || $past(req) || $past(req, 2)));
`endif
endmodule// formal: bmc 6 expect fail slang top window_demo
`define FORMAL
module window_demo (
input wire clk,
input wire rst,
input wire req
);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] recent; // recent[i] is req seen i+1 cycles ago
always @(posedge clk) recent <= rst ? 3'd0 : {recent[1:0], req};
reg [1:0] hist;
always @(posedge clk) if (rst) hist <= 2'd0; else if (hist != 2'd2) hist <= hist + 2'd1;
always @(posedge clk) if (!init && hist == 2'd2) a_window: assert ((req || recent[0] || recent[1]) == (req || $past(req)));
`endif
endmoduleEvery property that reads history skips step 0 and the cycle after every reset, and says which property is gated.
History counters clear on every reset, including mid-run resets.
Covers use the same gate as the properties they witness.
When a history property fails at step 2 on a good design, the gate is missing: remove it on purpose and confirm the step-2 failure, then restore it. For mid-run resets, let reset assert in the middle of the run and confirm the history counter clears.
The history gate is missing: the property compares the first real cycle with the reset cycle. Add the past-of-reset guard and confirm the failure disappears.
An ungated cover can be reached by reset-cycle behaviour the property never judges, so the witness would vouch for a check that never ran.