A pair proof compares two copies that start in different arbitrary states, so the induction step must be told which parts of the two states are equal. Without that, it fails on a state the pair can never reach. This lesson gives the helper assertions, shows each failing partner failing for its own reason, and checks the chain from its table.
The compared output shows one register at a time, so two copies can differ in a register that nobody is reading, for any number of cycles. A window of any length starts in such a state and is followed by a read of the register that differs. The helper states the equality of the whole register state of both copies; with it the step closes.
def step(d1, d2, wr, v):
return (v, v) if wr else (d1, d2) # a write reaches both copies; without a write the state stays
def cti_exists(k, helper):
"""Two copies of a one-register store (2 bits each). The compared output is the register only in a cycle that reads it.
Is there a window of k states, each fine in itself, followed by a state in which the copies differ and the register is read?"""
ok = (lambda s: s[0] == s[1]) if helper else (lambda s: True)
cur = {(a, b) for a in range(4) for b in range(4) if ok((a, b))} # the step starts from any state
for _ in range(k - 1):
cur = {step(a, b, wr, v) for a, b in cur for wr in (0, 1) for v in range(4) if ok(step(a, b, wr, v))}
return any(a != b for a, b in cur)
assert all(cti_exists(k, helper=False) for k in range(1, 13)), "no window closes the step without the helper"
assert not any(cti_exists(k, helper=True) for k in range(1, 13)), "with the equality helper the first window closes it"
print("PASS: without the equality helper every window has a counterexample to the step; with it none does")// formal: prove 4 expect pass slang top csr_reset_pair
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// set_err (a set wins over a clear in the same cycle); bits 7:2 read 0; reset 0x00
// addr 2 ID read-only constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) : (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule
// lesson-local wrapper: two copies of csr_block with identical inputs
module csr_reset_pair (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata1,
output wire [7:0] rdata2
);
csr_block u1 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata1));
csr_block u2 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata2));
`ifdef FORMAL
reg c_init = 1'b1;
always @(posedge clk) c_init <= 1'b0;
always @(*) if (c_init) assume (rst);
always @(*) if (!c_init) a_det: assert (rdata1 == rdata2);
// helper assertion: the whole register state of the two copies is equal, not only the register that is read
always @(*) if (!c_init) h_state: assert (u1.ctrl == u2.ctrl && u1.status == u2.status && u1.data == u2.data);
always @(*) if (!c_init) c_pair_write: cover (wr_en && addr == 2'd3);
`endif
endmoduleThe partner removes the reset assignment of DATA from the register block, and switches off the block's own assertions so that only the pair can notice. It fails at depth 2, through the helper and the compared output together.
// formal: bmc 4 expect fail slang top csr_reset_pair
`define FORMAL
// the design's own assertions are switched off and the reset of DATA is removed, so only the pair can notice
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// set_err (a set wins over a clear in the same cycle); bits 7:2 read 0; reset 0x00
// addr 2 ID read-only constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) : (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
x_a_id_const: cover (addr != 2'd2 || rdata == 8'hA5);
x_a_status_hi: cover (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
if ($past(rst)) begin
x_a_rst_ctrl: cover (ctrl == 8'h00);
x_a_rst_status: cover (status == 2'b00);
end
if (!$past(rst)) begin
x_a_ctrl_rw: cover (!($past(w_ctrl)) || ctrl == $past(wdata));
x_a_data_rw: cover (!($past(w_data)) || data == $past(wdata));
x_a_w1c_done: cover (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
x_a_w1c_err: cover (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
x_a_w1c_zero: cover (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
x_a_hw_set: cover (!$past(set_done) || status[0]);
x_a_isolate_ctrl: cover ($past(w_ctrl) || ctrl == $past(ctrl));
x_a_isolate_data: cover ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule
// lesson-local wrapper: two copies of csr_block with identical inputs
module csr_reset_pair (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata1,
output wire [7:0] rdata2
);
csr_block u1 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata1));
csr_block u2 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
.set_done(set_done), .set_err(set_err), .rdata(rdata2));
`ifdef FORMAL
reg c_init = 1'b1;
always @(posedge clk) c_init <= 1'b0;
always @(*) if (c_init) assume (rst);
always @(*) if (!c_init) a_det: assert (rdata1 == rdata2);
// helper assertion: the whole register state of the two copies is equal, not only the register that is read
always @(*) if (!c_init) h_state: assert (u1.ctrl == u2.ctrl && u1.status == u2.status && u1.data == u2.data);
always @(*) if (!c_init) c_pair_write: cover (wr_en && addr == 2'd3);
`endif
endmoduleThe control pair proves without a helper: reset defines both stage flags. Its partner removes the reset of the output valid, and fails at depth 2. The data pair, which compares the output word, fails at depth 2 for a different reason: the output data register is never reset, so the copies start different. The refined claim compares the data only after a word has been accepted; its step needs four helper assertions: the stage flags agree, an output valid implies a word was accepted, the skid words agree, and after an accepted word the output words agree.
// formal: bmc 2 expect fail slang top hs_reset_pair_ctrl
`define FORMAL
// the design's own assertions are switched off and the reset of the output valid is removed, so only the pair can notice
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
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
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);
// ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
x_a_skid_needs_out: cover (!svld || ovld);
x_a_conserve: cover (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: history-based, so skip the cycle after reset ----
always @(posedge clk) if (!init && !$past(rst)) begin
x_a_valid_hold: cover (!($past(out_valid) && !$past(out_ready)) || out_valid);
x_a_data_hold: cover (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
x_a_no_ready_comb: cover (in_ready == !svld);
end
// ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) x_a_data: cover (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
x_h_in_out: cover (!(tv && dlv == tn) || (ovld && odat == td));
x_h_in_skid: cover (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
x_h_pos: cover (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
c_tracked_out: cover (out_xfer && tv && dlv == tn);
end
`endif
endmodule
// lesson-local wrapper: two identical hs_bridge copies with identical inputs
module hs_reset_pair_ctrl (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready,
output wire in_ready1,
output wire in_ready2,
output wire out_valid1,
output wire out_valid2
);
hs_bridge u1 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready1),
.in_data(in_data), .out_valid(out_valid1), .out_ready(out_ready), .out_data());
hs_bridge u2 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready2),
.in_data(in_data), .out_valid(out_valid2), .out_ready(out_ready), .out_data());
`ifdef FORMAL
reg c_init = 1'b1;
always @(posedge clk) c_init <= 1'b0;
always @(*) if (c_init) assume (rst);
always @(*) if (!c_init) a_det_ctrl: assert (in_ready1 == in_ready2 && out_valid1 == out_valid2);
always @(*) if (!c_init) c_pair_flow: cover (in_valid && in_ready1 && out_ready);
`endif
endmodule// formal: prove 4 expect pass slang top hs_reset_pair_written
`define FORMAL
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
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);
// ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: history-based, so skip the cycle after reset ----
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
// ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
c_tracked_out: cover (out_xfer && tv && dlv == tn);
end
`endif
endmodule
// lesson-local wrapper: two identical hs_bridge copies with identical inputs
module hs_reset_pair_written (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready,
output wire [7:0] out_data1,
output wire [7:0] out_data2
);
wire ready1;
hs_bridge u1 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(ready1),
.in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data1));
hs_bridge u2 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(),
.in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data2));
`ifdef FORMAL
reg c_init = 1'b1;
always @(posedge clk) c_init <= 1'b0;
always @(*) if (c_init) assume (rst);
reg seen = 1'b0; // a word has been accepted since the last reset
always @(posedge clk) begin
if (rst) seen <= 1'b0;
else if (in_valid && ready1) seen <= 1'b1;
end
always @(*) if (!c_init) a_det_written: assert (!seen || out_data1 == out_data2);
// helper assertions for the induction step
always @(*) if (!c_init) begin
h_ctl: assert (u1.ovld == u2.ovld && u1.svld == u2.svld);
h_seen: assert (!u1.ovld || seen);
h_sk: assert (!u1.svld || u1.sdat == u2.sdat);
h_od: assert (!seen || u1.odat == u2.odat);
end
always @(*) if (!c_init) c_pair_written: cover (seen && out_data1 == 8'hA5);
`endif
endmoduleThe chain feeds the bridge from the FIFO in mode 0 and from an external port in mode 1. The assertions are generated from the rows of the table, one per row, each under its mode condition. The module is called fifo_bridge_chain here and is not the chain of the connectivity section.
Row | Mode | Destination | Source | Meaning |
|---|---|---|---|---|
d0 | 0 |
|
| bridge data comes from the FIFO read data |
d1 | 1 |
|
| bridge data comes from the external port |
v0 | 0 |
|
| bridge valid comes from the FIFO not being empty |
v1 | 1 |
|
| bridge valid comes from the external valid |
Variant 1 swaps the two data sources; variant 2 swaps the two valid sources. Each fails at depth 2 through its own row: a_row_d1 fails because with the swap the bridge sees the FIFO's unwritten memory word in mode 1, which needs no push. The chain cover shows a FIFO word reaching the bridge in mode 0.
// formal: bmc 2 expect fail slang top fifo_bridge_chain define BUG=1
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
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
// ---- harness: the first cycle is a reset, the state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties (after the reset cycle) ----
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
// ---- transition properties (they read history, so skip the cycle after reset) ----
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
// ---- data integrity by tracked-slot abstraction: one free slot, one shadow value ----
// The free constant is an anyconst wire that is also assumed equal to its one-cycle-old copy;
// this form works in both front ends, while a clocked assume of stability lags one step.
(* 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; // the tracked slot holds a word we are watching
reg [7:0] td; // the value that should be there
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
// ---- covers: the triggers of the properties can happen ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
c_tracked_read: cover (tv && !empty && rptr == tslot);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
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);
// ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: history-based, so skip the cycle after reset ----
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
// ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
c_tracked_out: cover (out_xfer && tv && dlv == tn);
end
`endif
endmodule
// lesson-local wrapper: FIFO into bridge, with a mode that selects the bridge source (the connectivity table is below)
module fifo_bridge_chain #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire push,
input wire [7:0] wdata,
input wire ext_valid,
input wire [7:0] ext_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] frdata;
wire ffull, fempty;
wire [2:0] fcount;
wire bin_valid, bin_ready;
wire [7:0] bin_data;
wire take = bin_valid && bin_ready;
sync_fifo u_f (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(take && !mode), .rdata(frdata), .full(ffull), .empty(fempty), .count(fcount));
assign bin_valid = (BUG == 2) ? (mode ? !fempty : ext_valid) : (mode ? ext_valid : !fempty);
assign bin_data = (BUG == 1) ? (mode ? frdata : ext_data) : (mode ? ext_data : frdata);
hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(bin_valid), .in_ready(bin_ready),
.in_data(bin_data), .out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
reg d_init = 1'b1;
always @(posedge clk) d_init <= 1'b0;
always @(*) if (d_init) assume (rst);
// one assertion per row of the table, under the row's mode condition
always @(*) if (!d_init) begin
a_row_d0: assert (mode != 1'b0 || bin_data == frdata);
a_row_d1: assert (mode != 1'b1 || bin_data == ext_data);
a_row_v0: assert (mode != 1'b0 || bin_valid == !fempty);
a_row_v1: assert (mode != 1'b1 || bin_valid == ext_valid);
end
always @(*) if (!d_init) c_chain_fifo_word: cover (!mode && bin_valid && bin_data == 8'hA5);
`endif
endmodule// formal: bmc 2 expect fail slang top fifo_bridge_chain define BUG=2
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
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
// ---- harness: the first cycle is a reset, the state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties (after the reset cycle) ----
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
// ---- transition properties (they read history, so skip the cycle after reset) ----
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
// ---- data integrity by tracked-slot abstraction: one free slot, one shadow value ----
// The free constant is an anyconst wire that is also assumed equal to its one-cycle-old copy;
// this form works in both front ends, while a clocked assume of stability lags one step.
(* 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; // the tracked slot holds a word we are watching
reg [7:0] td; // the value that should be there
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
// ---- covers: the triggers of the properties can happen ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
c_tracked_read: cover (tv && !empty && rptr == tslot);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
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);
// ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: history-based, so skip the cycle after reset ----
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
// ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
c_tracked_out: cover (out_xfer && tv && dlv == tn);
end
`endif
endmodule
// lesson-local wrapper: FIFO into bridge, with a mode that selects the bridge source (the connectivity table is below)
module fifo_bridge_chain #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire push,
input wire [7:0] wdata,
input wire ext_valid,
input wire [7:0] ext_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] frdata;
wire ffull, fempty;
wire [2:0] fcount;
wire bin_valid, bin_ready;
wire [7:0] bin_data;
wire take = bin_valid && bin_ready;
sync_fifo u_f (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(take && !mode), .rdata(frdata), .full(ffull), .empty(fempty), .count(fcount));
assign bin_valid = (BUG == 2) ? (mode ? !fempty : ext_valid) : (mode ? ext_valid : !fempty);
assign bin_data = (BUG == 1) ? (mode ? frdata : ext_data) : (mode ? ext_data : frdata);
hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(bin_valid), .in_ready(bin_ready),
.in_data(bin_data), .out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
reg d_init = 1'b1;
always @(posedge clk) d_init <= 1'b0;
always @(*) if (d_init) assume (rst);
// one assertion per row of the table, under the row's mode condition
always @(*) if (!d_init) begin
a_row_d0: assert (mode != 1'b0 || bin_data == frdata);
a_row_d1: assert (mode != 1'b1 || bin_data == ext_data);
a_row_v0: assert (mode != 1'b0 || bin_valid == !fempty);
a_row_v1: assert (mode != 1'b1 || bin_valid == ext_valid);
end
always @(*) if (!d_init) c_chain_fifo_word: cover (!mode && bin_valid && bin_data == 8'hA5);
`endif
endmodule// formal: cover 6 expect reached slang top fifo_bridge_chain
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
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
// ---- harness: the first cycle is a reset, the state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state properties (after the reset cycle) ----
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
// ---- transition properties (they read history, so skip the cycle after reset) ----
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
// ---- data integrity by tracked-slot abstraction: one free slot, one shadow value ----
// The free constant is an anyconst wire that is also assumed equal to its one-cycle-old copy;
// this form works in both front ends, while a clocked assume of stability lags one step.
(* 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; // the tracked slot holds a word we are watching
reg [7:0] td; // the value that should be there
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
// ---- covers: the triggers of the properties can happen ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
c_tracked_read: cover (tv && !empty && rptr == tslot);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
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);
// ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld);
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: history-based, so skip the cycle after reset ----
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
// ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
c_tracked_out: cover (out_xfer && tv && dlv == tn);
end
`endif
endmodule
// lesson-local wrapper: FIFO into bridge, with a mode that selects the bridge source (the connectivity table is below)
module fifo_bridge_chain #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire mode,
input wire push,
input wire [7:0] wdata,
input wire ext_valid,
input wire [7:0] ext_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
wire [7:0] frdata;
wire ffull, fempty;
wire [2:0] fcount;
wire bin_valid, bin_ready;
wire [7:0] bin_data;
wire take = bin_valid && bin_ready;
sync_fifo u_f (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(take && !mode), .rdata(frdata), .full(ffull), .empty(fempty), .count(fcount));
assign bin_valid = (BUG == 2) ? (mode ? !fempty : ext_valid) : (mode ? ext_valid : !fempty);
assign bin_data = (BUG == 1) ? (mode ? frdata : ext_data) : (mode ? ext_data : frdata);
hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(bin_valid), .in_ready(bin_ready),
.in_data(bin_data), .out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
reg d_init = 1'b1;
always @(posedge clk) d_init <= 1'b0;
always @(*) if (d_init) assume (rst);
// one assertion per row of the table, under the row's mode condition
always @(*) if (!d_init) begin
a_row_d0: assert (mode != 1'b0 || bin_data == frdata);
a_row_d1: assert (mode != 1'b1 || bin_data == ext_data);
a_row_v0: assert (mode != 1'b0 || bin_valid == !fempty);
a_row_v1: assert (mode != 1'b1 || bin_valid == ext_valid);
end
always @(*) if (!d_init) c_chain_fifo_word: cover (!mode && bin_valid && bin_data == 8'hA5);
`endif
endmoduleEach proof has a partner that fails because of the removed reset, not because of different stimulus.
A helper assertion is stated as a fact about the state of both copies and is itself proved.
A connectivity proof is generated from the table and fails in the row that is wrong.
If a pair partner fails through the wrong property, switch off the block's own assertions in your copy: only the pair's properties may fail. For a failing row, read the mode condition first.
Reset defines the stage flags only. The output data register is arbitrary after reset, so two copies disagree until a word has been written.
The row is asserted outside its mode condition, or the sources agree in the cycles checked. Check the mode condition, then give the two sources different values.