Integration bugs are wiring bugs: the right blocks, the wrong connections. A block-level testbench drives the FIFO with hand-picked data and never notices that in the system its write port is fed by the wrong source in test mode. The symptom is corruption no block owner can reproduce, because every block is correct in isolation. A connectivity proof closes that gap structurally: it states every intended connection once, in a table, and proves each one over all values.
The table is the specification. Each row names a source, a destination, a condition (usually a mode) and a label. A short generator turns each row into one check, so the proof block always matches the table. Each check reads the instance's destination port by name, so it sees what the port receives, not a wrapper alias. Reading a port by hierarchical name works with the front end the proof header selects and is rejected by the default one, so the checks live in a wrapper that instantiates the chain, not in a bound checker. The proof then covers all input values and all modes at once, which no directed test list can do. For background on tables as source of truth and on the structural checker view, see the SoC lessons on connectivity tables and the Python checker.
The chain under proof is the helper wrapper chain_top, lesson-local to this topic: the arithmetic pipeline feeds the FIFO, the FIFO feeds the handshake stage, and the FIFO is popped only when the handshake stage can accept. The pipeline runs with its own properties switched off, and the FIFO and handshake stage keep theirs, so every failure below is a wiring failure. Six rows cover the two sources of FIFO write data (one per mode), the data hop, the valid hop, the backpressure hop and the downstream ready:
Row | Source | Destination | Condition |
|---|---|---|---|
1 | pipeline output | FIFO | mode 0 (normal) |
2 | constant 0x00 | FIFO | mode 1 (test) |
3 | FIFO | handshake | always |
4 | FIFO not empty | handshake | always |
5 | handshake | FIFO | always |
6 | top-level | handshake | always |
The generator below takes the same six rows and emits one check per row. The text of the real proof block is pasted into the script as SV_LINES, so the script asserts that what it generates is exactly what the proof runs, that every (destination, condition) pair has exactly one check (rows 1 and 2 share a destination and differ in condition), and that a dropped row or a typo in a row changes the output. A generator nobody compares with the block is just a second copy of the intent:
rows = [
("u_pipe.y", "u_fifo.wdata", "mode == 1'b0", "pipe_to_fifo"),
("8'h00", "u_fifo.wdata", "mode == 1'b1", "tieoff_test"),
("u_fifo.rdata", "u_bridge.in_data", "1'b1", "fifo_to_bridge_data"),
("!u_fifo.empty", "u_bridge.in_valid", "1'b1", "fifo_to_bridge_valid"),
("u_bridge.in_ready && !u_fifo.empty", "u_fifo.pop", "1'b1", "bridge_ready_to_pop"),
("out_ready", "u_bridge.out_ready", "1'b1", "downstream_ready"),
]
SV_LINES = [
"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)));",
]
def emit(row):
src, dst, cond, label = row
return "conn_%s: assert (!(%s) || (%s == (%s)));" % (label, cond, dst, src)
generated = [emit(r) for r in rows]
assert generated == SV_LINES, "generated text must equal the proof block"
assert len(generated) == len(rows) == 6
assert len({(r[1], r[2]) for r in rows}) == len(rows), "one check per (destination, condition)"
assert len({r[3] for r in rows}) == len(rows), "labels are unique, so a failure names its row"
dropped = [emit(r) for r in rows[:-1]]
assert dropped != SV_LINES, "a dropped row must change the block"
typo = list(rows)
typo[1] = ("8'hFF", typo[1][1], typo[1][2], typo[1][3])
assert [emit(r) for r in typo] != SV_LINES and "8'hFF" in emit(typo[1])
print("PASS: 6 rows generate the 6 checks of the proof block; a dropped row and a typo are both visible")The wrapper wires the three running designs together and holds the six generated checks. The passing proof covers all values of data and both modes, and the base case and induction step both pass: proven for this model, which has the reset cycle at step 0 and checks from step 1. Its partner changes one thing, the table: row 2 is typed with the constant 0xFF while the wiring still ties the destination to 0x00. Every table typo has this shape, and the proof names the row at the first checked step.
// formal: prove 4 expect pass slang top chain_top
`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
endmoduleIn the typo run the proof stops at step 1, the first checked step, with conn_tieoff_test failing:
Step | mode | FIFO | Row 2 expects | Outcome |
|---|---|---|---|---|
0 | 1 | 0x00 | - | reset cycle, not checked |
1 | 1 | 0x00 | 0xFF | counterexample: |
// formal: bmc 4 expect fail slang top chain_top
`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'hFF)));
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
endmoduleRoot cause: the table row names a value that the specification does not. Here the specification says the test-mode tie-off is zero, so the table is wrong and the fix is to the table. Which side is wrong is decided from the specification, never from whichever side is easier to edit; the next lesson gives the decision order.
The table lists every hop including tie-offs and the backpressure path, not just the glamorous data path.
Each generated check names its row, so a failure points at the table, not at an anonymous assertion.
Each check reads the destination port, not a wrapper alias: a check that compares a wire with the signal it was declared equal to cannot fail.
Every mode has a cover: an unreached mode is either a missing test or a dead configuration, and both need an owner (next lesson).
When a row fails, read the trace: which step, which mode, what the source held, what the destination saw. Then decide from the specification whether the row or the wiring is wrong; editing the check to match the wiring turns the proof into a description of the bug. The wrapper must be sound too: it pops the FIFO only when the handshake stage can accept, because a wrapper that pops regardless loses words under backpressure and makes every later proof about a broken harness.
When the FIFO-to-handshake hop is only valid in some modes, for example if test mode loops the handshake input back to a pattern generator. An always-on check on a sometimes-off path fails spuriously, which is the next lesson.