When a connectivity proof fails, the clock is ticking: is the table wrong or is the wiring wrong? The trace answers that, but only if you read it as a table of steps against rows rather than as a waveform to admire. Three shapes cover most failures: a width truncation where a wide bus meets a narrow port, a swapped pair where two groups of bits cross, and a missing tie-off where an input is left undriven. Each has a characteristic trace signature, and each is run below on the six-row chain.
A linter catches the cheap mistakes before the tool runs: widths on both ends of every row, no (destination, condition) pair driven twice, every source named. What remains for the proof is then either a real wiring bug or a subtle table error. The trace tells the shape: a truncation fails only on values that use the lost bit, a swap fails whenever the swapped groups differ, and a missing tie-off fails with a value the solver chose, because an undriven input is a free input. For the address-map side of the same discipline, the memory-map alias lesson is the companion.
The linter below checks the three cheap properties over a small table. A destination may appear in several rows if their conditions differ, as the two FIFO write-data rows do. Each injected bad table is caught by exactly one rule, and the good table passes all three, so the check itself is shown able to fail:
def lint(rows, widths):
errors = []
seen = {}
for src, dst, src_w, dst_w, cond in rows:
if src_w != dst_w:
errors.append(("width", dst, src_w, dst_w))
if (dst, cond) in seen:
errors.append(("duplicate", dst, cond, src))
seen.setdefault((dst, cond), src)
if src not in widths and not src.startswith("const"):
errors.append(("undriven", src, dst, None))
return errors
widths = {"pipe_y": 8, "fifo_rdata": 8, "const0": 8}
good = [("pipe_y", "fifo_wdata", 8, 8, "mode0"),
("const0", "fifo_wdata", 8, 8, "mode1"),
("fifo_rdata", "bridge_in", 8, 8, "always")]
assert lint(good, widths) == [], "same destination under different conditions is legal"
trunc = [("pipe_y", "narrow_in", 8, 7, "always")]
assert lint(trunc, widths)[0][0] == "width"
dup = [("pipe_y", "fifo_wdata", 8, 8, "mode0"), ("fifo_rdata", "fifo_wdata", 8, 8, "mode0")]
assert lint(dup, widths)[0][0] == "duplicate"
float_in = [("mystery_sig", "fifo_wdata", 8, 8, "always")]
assert lint(float_in, widths)[0][0] == "undriven"
print("PASS: linter clears the good table, flags truncation, duplicate drive, undriven source")The faults below are options of the same wrapper, run against the same six generated checks. The first three were run to depth 4 and fail at step 1, the first checked step, which is why their tables are short; the last two are read after them, and the first of those needs traffic. The values are the ones the solver chose in the run; the argument depends on the shape, not on the particular value.
Truncation: the data hop drops bit 7, so the handshake stage receives an 8-bit word through a 7-bit connection with bit 7 forced to zero. The trace needs a word with bit 7 set, and a word without it passes:
Step | FIFO | handshake | Row 3 says | Outcome |
|---|---|---|---|---|
0 | - | - | - | reset cycle, not checked |
1 | 0x80 | 0x00 | equal | counterexample: |
// formal: bmc 4 expect fail slang top chain_top define FAULT=1
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmoduleSwap: the two nibbles of the data hop cross. It fails on any word whose nibbles differ, so the first trace is the smallest such word:
Step | FIFO | handshake | Row 3 says | Outcome |
|---|---|---|---|---|
1 | 0x01 | 0x10 | equal | counterexample: |
// formal: bmc 4 expect fail slang top chain_top define FAULT=2
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmoduleMissing tie-off: in test mode the FIFO write data comes from a wire nobody drives. The solver may choose any value for it, so the trace shows a value that looks arbitrary, and every non-zero value fails the same way. That is not a sign that the table is wrong: the cure is the tie-off in the RTL, or, if the specification really leaves the value open, a table row that says so. Diagnosing by how the data varies between runs is never the answer:
Step | mode | undriven wire | FIFO | Row 2 says | Outcome |
|---|---|---|---|---|---|
1 | 1 | 0x01 | 0x01 | 0x00 | counterexample: |
// formal: bmc 4 expect fail slang top chain_top define FAULT=3
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmoduleTwo more faults complete the set, so that every row is shown failing. Both are one-line wiring errors and they behave differently. Row 5 (pop only when the handshake stage can accept): the pop ignores the stage's ready. The wrong pop only matters once the stage is not ready while the FIFO still holds a word, and that state needs the skid register to fill first. The bound to 5 fails at step 4; the bound to 4 passes, so a shorter bound would have missed this fault. Connectivity checks do not always fail at the first checked step:
// formal: bmc 4 expect pass slang top chain_top define FAULT=4
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmodule// formal: bmc 5 expect fail slang top chain_top define FAULT=4
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmoduleRow 6 (top-level out_ready to the stage's out_ready): the stage's out_ready is tied high. Unlike row 5 it needs no traffic: the first checked step with out_ready low shows the tie, so it fails at step 1, and the bound that contains only the reset step passes:
// formal: bmc 1 expect pass slang top chain_top define FAULT=5
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmodule// formal: bmc 2 expect fail slang top chain_top define FAULT=5
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
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
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module chain_top #(parameter FAULT = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] pipe_y;
wire [7:0] fifo_rdata;
wire fifo_full, fifo_empty;
wire [2:0] fifo_count;
wire bridge_ready;
wire [7:0] tie; // never driven: this is the missing tie-off that FAULT 3 uses
pipe3 #(.CHECK(0)) u_pipe (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(pipe_y), .dbg_p());
// the wiring under proof; FAULT 0 is the intended wiring; FAULT 4 ignores the bridge's ready, FAULT 5 ties its out_ready high
wire [7:0] fifo_wdata = (mode == 1'b0) ? pipe_y : ((FAULT == 3) ? tie : 8'h00);
wire fifo_pop = (FAULT == 4) ? !fifo_empty : (!fifo_empty && bridge_ready);
wire [7:0] bridge_indata = (FAULT == 1) ? {1'b0, fifo_rdata[6:0]} :
(FAULT == 2) ? {fifo_rdata[3:0], fifo_rdata[7:4]} : fifo_rdata;
sync_fifo u_fifo (.clk(clk), .rst(rst), .push(!fifo_full), .wdata(fifo_wdata),
.pop(fifo_pop), .rdata(fifo_rdata), .full(fifo_full),
.empty(fifo_empty), .count(fifo_count));
hs_bridge u_bridge (.clk(clk), .rst(rst), .in_valid(!fifo_empty),
.in_ready(bridge_ready), .in_data(bridge_indata),
.out_valid(out_valid), .out_ready((FAULT == 5) ? 1'b1 : out_ready), .out_data(out_data));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// generated from the connection table: one line per row
always @(*) if (!init) begin
conn_pipe_to_fifo: assert (!(mode == 1'b0) || (u_fifo.wdata == (u_pipe.y)));
conn_tieoff_test: assert (!(mode == 1'b1) || (u_fifo.wdata == (8'h00)));
conn_fifo_to_bridge_data: assert (!(1'b1) || (u_bridge.in_data == (u_fifo.rdata)));
conn_fifo_to_bridge_valid: assert (!(1'b1) || (u_bridge.in_valid == (!u_fifo.empty)));
conn_bridge_ready_to_pop: assert (!(1'b1) || (u_fifo.pop == (u_bridge.in_ready && !u_fifo.empty)));
conn_downstream_ready: assert (!(1'b1) || (u_bridge.out_ready == (out_ready)));
end
`endif
endmoduleThe trace reading names the row, the step, and the exact bits that disagree, not just the property label.
Width mismatches are fixed by sizing the row explicitly, never by masking the check down to the bits that pass.
A failure whose destination follows a free value is read as an undriven input first, and the tie-off is added in the RTL.
Decision order: run the linter, read the row the trace names, compare the row against the specification, and only then open the schematic. If the specification and the row agree and the wiring does not, the wiring is wrong; if the row matches nothing in the specification, the table is wrong. Either way the generator reruns and the proof reruns on the final table. A formal tool returns the same counterexample for the same model: when a value looks arbitrary it is because the model leaves it free, not because the failure is unstable.
Wiring: the specification says test mode ties the destination to zero, and the RTL leaves the input undriven, so the solver is free to choose. The fix is the tie-off, and the same proof must then pass.