A team wrote the valid/ready stability rule as an assertion and instantiated it on both faces of the bridge. On the good bridge the proof failed at step 4: the upstream face is a free input and nothing keeps its promise. Job of this lesson: one checker module with a role, the cycle-after-reset guard it needs, and the wrapper that places it.
The rule: once vld is high and rdy is low, in the next cycle vld stays high and dat stays equal. The checker records the previous cycle in registers (its checks sit in a combinational block, where $past is not allowed), and a stall counts only if the previous cycle was not a reset cycle. A role parameter decides the form: ASSUME=1 states the rule, ASSUME=0 asserts it. The wrapper instantiates the bridge and two checkers: the upstream face as an assumption, the downstream face as an assertion.
// not-run: implication operators are not accepted by the front end used here
// a_hold_v: assert property (@(posedge clk) disable iff (rst) (vld && !rdy) |=> vld);
// a_hold_d: assert property (@(posedge clk) disable iff (rst) (vld && !rdy) |=> (dat == $past(dat)));
// Each checks the cycle after a stall: the stalled cycle is the antecedent, the next cycle the consequent.
// The runnable form below checks the same cycle, with a guard for the cycle after reset that disable iff does not give.The front end the lessons select accepts both bind and hierarchical references; the default front end rejects them, and commercial tools differ in checker and bind support. These checkers sit in a module and a wrapper, so the same text runs on both.
// formal: prove 4 expect pass slang top wr_top define UP_ASSUME=1 define BUG=0
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
module vr_checker #(parameter W = 8, parameter ASSUME = 0) (
input wire clk, input wire rst, input wire vld, input wire rdy, input wire [W-1:0] dat);
reg started = 1'b0; reg pv = 1'b0, pr = 1'b0, prst = 1'b1; reg [W-1:0] pd = {W{1'b0}};
always @(posedge clk) begin started <= 1'b1; pv <= vld; pr <= rdy; prst <= rst; pd <= dat; end
wire stalled_before = started && !rst && !prst && pv && !pr;
generate if (ASSUME) begin : g_a
always @(*) if (stalled_before) begin a_hold_v: assume (vld); a_hold_d: assume (dat == pd); end
end else begin : g_s
always @(*) if (stalled_before) begin a_hold_v: assert (vld); a_hold_d: assert (dat == pd); end
end endgenerate
endmodule
module wr_top #(parameter UP_ASSUME = 1, parameter BUG = 0) (
input wire clk, input wire rst, input wire in_valid, input wire [7:0] in_data, input wire out_ready);
wire in_ready, out_valid; wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .in_ready(in_ready),
.out_valid(out_valid), .out_data(out_data), .out_ready(out_ready));
vr_checker #(.W(8), .ASSUME(UP_ASSUME)) u_up (.clk(clk), .rst(rst), .vld(in_valid), .rdy(in_ready), .dat(in_data));
vr_checker #(.W(8), .ASSUME(0)) u_dn (.clk(clk), .rst(rst), .vld(out_valid), .rdy(out_ready), .dat(out_data));
endmoduleUpstream assumed, downstream asserted: the good bridge proves. Now the role mistake, then two faults seen on the downstream face:
// formal: bmc 5 expect fail slang top wr_top define UP_ASSUME=0 define BUG=0
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
module vr_checker #(parameter W = 8, parameter ASSUME = 0) (
input wire clk, input wire rst, input wire vld, input wire rdy, input wire [W-1:0] dat);
reg started = 1'b0; reg pv = 1'b0, pr = 1'b0, prst = 1'b1; reg [W-1:0] pd = {W{1'b0}};
always @(posedge clk) begin started <= 1'b1; pv <= vld; pr <= rdy; prst <= rst; pd <= dat; end
wire stalled_before = started && !rst && !prst && pv && !pr;
generate if (ASSUME) begin : g_a
always @(*) if (stalled_before) begin a_hold_v: assume (vld); a_hold_d: assume (dat == pd); end
end else begin : g_s
always @(*) if (stalled_before) begin a_hold_v: assert (vld); a_hold_d: assert (dat == pd); end
end endgenerate
endmodule
module wr_top #(parameter UP_ASSUME = 1, parameter BUG = 0) (
input wire clk, input wire rst, input wire in_valid, input wire [7:0] in_data, input wire out_ready);
wire in_ready, out_valid; wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .in_ready(in_ready),
.out_valid(out_valid), .out_data(out_data), .out_ready(out_ready));
vr_checker #(.W(8), .ASSUME(UP_ASSUME)) u_up (.clk(clk), .rst(rst), .vld(in_valid), .rdy(in_ready), .dat(in_data));
vr_checker #(.W(8), .ASSUME(0)) u_dn (.clk(clk), .rst(rst), .vld(out_valid), .rdy(out_ready), .dat(out_data));
endmodule// formal: bmc 4 expect fail slang top wr_top define UP_ASSUME=1 define BUG=2
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
module vr_checker #(parameter W = 8, parameter ASSUME = 0) (
input wire clk, input wire rst, input wire vld, input wire rdy, input wire [W-1:0] dat);
reg started = 1'b0; reg pv = 1'b0, pr = 1'b0, prst = 1'b1; reg [W-1:0] pd = {W{1'b0}};
always @(posedge clk) begin started <= 1'b1; pv <= vld; pr <= rdy; prst <= rst; pd <= dat; end
wire stalled_before = started && !rst && !prst && pv && !pr;
generate if (ASSUME) begin : g_a
always @(*) if (stalled_before) begin a_hold_v: assume (vld); a_hold_d: assume (dat == pd); end
end else begin : g_s
always @(*) if (stalled_before) begin a_hold_v: assert (vld); a_hold_d: assert (dat == pd); end
end endgenerate
endmodule
module wr_top #(parameter UP_ASSUME = 1, parameter BUG = 0) (
input wire clk, input wire rst, input wire in_valid, input wire [7:0] in_data, input wire out_ready);
wire in_ready, out_valid; wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .in_ready(in_ready),
.out_valid(out_valid), .out_data(out_data), .out_ready(out_ready));
vr_checker #(.W(8), .ASSUME(UP_ASSUME)) u_up (.clk(clk), .rst(rst), .vld(in_valid), .rdy(in_ready), .dat(in_data));
vr_checker #(.W(8), .ASSUME(0)) u_dn (.clk(clk), .rst(rst), .vld(out_valid), .rdy(out_ready), .dat(out_data));
endmodule// formal: bmc 4 expect fail slang top wr_top define UP_ASSUME=1 define BUG=3
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmodule
module vr_checker #(parameter W = 8, parameter ASSUME = 0) (
input wire clk, input wire rst, input wire vld, input wire rdy, input wire [W-1:0] dat);
reg started = 1'b0; reg pv = 1'b0, pr = 1'b0, prst = 1'b1; reg [W-1:0] pd = {W{1'b0}};
always @(posedge clk) begin started <= 1'b1; pv <= vld; pr <= rdy; prst <= rst; pd <= dat; end
wire stalled_before = started && !rst && !prst && pv && !pr;
generate if (ASSUME) begin : g_a
always @(*) if (stalled_before) begin a_hold_v: assume (vld); a_hold_d: assume (dat == pd); end
end else begin : g_s
always @(*) if (stalled_before) begin a_hold_v: assert (vld); a_hold_d: assert (dat == pd); end
end endgenerate
endmodule
module wr_top #(parameter UP_ASSUME = 1, parameter BUG = 0) (
input wire clk, input wire rst, input wire in_valid, input wire [7:0] in_data, input wire out_ready);
wire in_ready, out_valid; wire [7:0] out_data;
hs_bridge #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .in_ready(in_ready),
.out_valid(out_valid), .out_data(out_data), .out_ready(out_ready));
vr_checker #(.W(8), .ASSUME(UP_ASSUME)) u_up (.clk(clk), .rst(rst), .vld(in_valid), .rdy(in_ready), .dat(in_data));
vr_checker #(.W(8), .ASSUME(0)) u_dn (.clk(clk), .rst(rst), .vld(out_valid), .rdy(out_ready), .dat(out_data));
endmoduleRun | Result | Reading |
|---|---|---|
Upstream assumed, downstream asserted | Proven, depth 4 | The role split the side rule asks for |
Upstream asserted too | Fails at step 4 (depth 4 passes) |
|
Valid dropped on a stall (fault 2) | Fails at step 3 (depth 3 passes) |
|
Data changes under a stall (fault 3) | Fails at step 3 (depth 3 passes) |
|
Step | in_valid, out_ready | out_valid | What the checker sees |
|---|---|---|---|
1 | 1, 0 | 0 | A word is accepted; the output will hold it |
2 | 0, 0 | 1 | The output stalls with valid high |
3 | - | 0 |
|
The checker has a role parameter, and each instance's role is the side rule: assume on what the block receives, assert on what it drives.
The previous-cycle guard skips the cycle after reset; a checker that only tests !rst fails on the first cycle after a reset.
Every checker instance is shown failing on a fault in the block that drives it.
If a checker instance fails on the good design in the first two cycles, check the reset guard. If it fails on a free input, its role is wrong. Plant a fault on each face and see the right instance fail.
$past?Its checks sit in a combinational block where $past is not allowed. The registers also let it carry the cycle-after-reset guard, which a reset disable alone does not give.