An engineer wrote the end-to-end data-integrity property first and received a counterexample starting in a state the design can never reach after reset. Two days went into reading it before anyone checked the reset harness. The property was fine; the foundation was missing. Bring-up has an order.
Job of this lesson: bring a harness up in six stages, each with a runnable check and a gate that says the stage is done.
Each stage removes one class of false failure before the next may fail: reset first, so no trace starts illegally; interface assumptions, so the environment obeys the protocol; covers, so traffic is known reachable; then protocol properties, end-to-end properties and complexity work. A failure at stage N is read only after the stages below pass:
Stage | What it proves and covers | Stage done means | Evidence below |
|---|---|---|---|
1. Reset and initial state | First cycle is reset; the state after it is legal | Reset cover reached; no failure at step 0 or 1 | Cover block; partner without the reset assumption |
2. Interface assumptions | The environment obeys the input rules | Each assumption reviewed and owed by a neighbour | Review, no run: only the reset here |
3. Basic covers | Traffic exists: stall, skid, flow | Every required cover reached | Same cover block |
4. Protocol properties | Hold rules, ready behaviour | Bounded check passes | Proof block; planted-bug partner |
5. End-to-end properties | Conservation, data integrity | Proven, or bounded with a justification | Same proof block |
6. Complexity work | Helpers, abstraction | Induction holds; runtime in budget | Same proof block |
The first run covers stages 1 and 3 together on the skid stage. This copy adds one cover to the design's own four, c_reset_released, true in the first cycle after a reset cycle. All five are reached within depth 5: reset at step 1, stall and flow at step 2, parked word and low ready at step 3. Stage 2 has no block: the only assumption is the reset at step 0, and the stage has no input rules.
// formal: cover 5 expect reached slang top hs_bridge
`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
reg rst_q;
always @(posedge clk) rst_q <= rst;
always @(*) if (!init) c_reset_released: cover (rst_q && !rst);
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
endmoduleStage 1 needs its failing partner, the opening mistake. With the reset assumption deleted the stage starts from an arbitrary state and three properties fail at step 1 on a correct design (depth 1 passes, depth 2 fails):
// formal: bmc 4 expect fail slang top hs_bridge
`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;
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
endmoduleStep | rst | acc | dlv | ovld | svld | Which condition breaks |
|---|---|---|---|---|---|---|
0 | 0 | 15 | 0 | 0 | 0 | Not checked: step 0 is the power-up state, and nothing forced it to be a reset |
1 | 0 | 0 | 0 | 1 | 0 | Conservation: acc - dlv is 0 but ovld + svld is 1; the tracked-word helper |
Root cause: with no reset assumption the state before the first edge is arbitrary, here a counter at 15 and an output register already full. The design is innocent. Fix: restore assume (rst) at step 0 and keep the reset cover. Stages 4 to 6 then run on a correct harness: prove 4 is the bounded check to depth 4 plus the induction step with k = 4, and the file carries the three helper invariants of stage 6, so one run covers protocol rules, conservation and data integrity:
// formal: prove 4 expect pass slang top hs_bridge
`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
endmoduleWith the planted data-loss bug conservation fails at step 3: a word accepted at step 1, the output stalled, a second word accepted into nowhere at step 2. The covers passed, so the trace starts legally and the failure is real:
// formal: bmc 4 expect fail slang top hs_bridge define BUG=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
endmoduleThe stage gate is mechanical. The script holds each stage's gate as a function of recorded outcomes, credits stages in order and stops at the first failed gate: end-to-end marked done while a cover is unreached is not credited.
stages = ["reset", "interfaces", "covers", "protocol", "end_to_end", "complexity"]
def gate_ok(stage, o):
if stage == "reset":
return o["reset_cover"] and not o["step0_failure"]
if stage == "interfaces":
return o["assumptions_reviewed"] and not o["orphan_assumption"]
if stage == "covers":
return o["required_covers_reached"] == o["required_covers"]
if stage == "protocol":
return o["protocol_bounded_pass"]
if stage == "end_to_end":
return o["end_to_end_ok"]
if stage == "complexity":
return o["induction_closed"] and o["in_budget"]
raise ValueError(stage)
def advance(o):
done = []
for s in stages:
if not gate_ok(s, o):
break
done.append(s)
return done
ok = {"reset_cover": True, "step0_failure": False, "assumptions_reviewed": True,
"orphan_assumption": False, "required_covers": 5, "required_covers_reached": 5,
"protocol_bounded_pass": True, "end_to_end_ok": True,
"induction_closed": True, "in_budget": True}
assert advance(ok) == stages
# one cover unreached while every later flag still says done: nothing after "interfaces" is credited
skipped = dict(ok, required_covers_reached=4)
assert advance(skipped) == ["reset", "interfaces"]
assert advance(dict(ok, step0_failure=True)) == []
assert advance(dict(ok, orphan_assumption=True)) == ["reset"]
assert advance(dict(ok, in_budget=False)) == stages[:-1]
print("PASS: stages are credited in order; an unreached cover stops the climb")Reset evidence exists before interface assumptions are trusted.
Every end-to-end failure on record postdates passing covers.
Stage gates are recorded per stage, not once at the end.
When an end-to-end property fails on the first run, rerun the covers before reading the trace. An unreached cover makes the failure a harness gap until proven otherwise; if all covers fire and the first cycle is legal, the trace is worth reading.
At the harness, not the design: without a stall there is no legal way to break conservation, so the trace starts illegally or the environment never stalls. Fix the covers before reading the failure.