A's unit proof passes under "data stays stable until grant". Integration fails. The neighbour B had never been asked to keep that rule. Job of this lesson: the assume-to-assert conversion: the same rule, the same text, assumed in A and asserted on the signals B drives.
The rule module has one body and two roles. Placed on A's inputs it is an assumption; placed on B's outputs it is an assertion that must be proved. The conversion is that one change, made at the integration level, and the assertion is the discharge. A miter that compares two implementations is a different tool: it does not convert assumptions.
B is a requester: it raises req with a word and holds both until granted. Its fault (BUG=1) takes a new word while waiting. The rule module, asserted on B's outputs, proves for the good B and fails for the faulty one at step 3 (depth 3 passes). A's own unit proof passes either way, because it assumes the rule. The system of A and B shows the consequence at step 4.
// formal: prove 6 expect pass slang top unitB define BUG=0
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: bmc 4 expect fail slang top unitB define BUG=1
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: prove 6 expect pass slang top unitA define ASSUME=1 define BUG=0
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: prove 6 expect pass slang top sysAB define BUG=0
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule// formal: bmc 5 expect fail slang top sysAB define BUG=1
`define FORMAL
module a_blk (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt,
output reg ov, output reg [3:0] out, output wire dbg_pend, output wire [3:0] dbg_held);
reg pend; reg [3:0] held;
assign dbg_pend = pend; assign dbg_held = held;
always @(posedge clk) begin
if (rst) begin pend <= 1'b0; ov <= 1'b0; end
else begin
ov <= req && gnt;
if (req && !gnt) pend <= 1'b1; else if (gnt) pend <= 1'b0;
if (req && !pend) held <= data;
out <= pend ? held : data;
end
end
endmodule
module hold_rule #(parameter ASSUME = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
reg init = 1'b1; reg pv = 1'b0, pg = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pv <= req; pg <= gnt; prst <= rst; pd <= data; end
wire waiting = !init && !rst && !prst && pv && !pg;
generate if (ASSUME == 2) begin : g_n
end else if (ASSUME) begin : g_a
always @(*) if (waiting) begin r_req: assume (req); r_dat: assume (data == pd); end
end else begin : g_s
always @(*) if (waiting) begin r_req: assert (req); r_dat: assert (data == pd); end
end endgenerate
endmodule
module a_spec (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt, input wire ov, input wire [3:0] out);
reg init = 1'b1; reg pgo = 1'b0, prst = 1'b1; reg [3:0] pd = 4'd0;
always @(posedge clk) begin init <= 1'b0; pgo <= req && gnt; prst <= rst; pd <= data; end
always @(*) if (!init && !prst && pgo) a_answer: assert (ov && out == pd);
always @(*) if (!init) c_wait_then_grant: cover (!prst && ov && out == pd && out != 4'd0);
endmodule
module unitA #(parameter ASSUME = 1, parameter BUG = 0) (input wire clk, input wire rst, input wire req, input wire [3:0] data, input wire gnt);
wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
reg qv = 1'b0, qg = 1'b0; always @(posedge clk) begin qv <= req; qg <= gnt; end
always @(*) if (!init0 && ASSUME == 1) h_hist: assert (!dp || rst || (qv && !qg));
always @(*) if (!init0 && ASSUME == 1) h_pend: assert (!dp || rst || dh == data);
hold_rule #(.ASSUME(ASSUME)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmodule
module b_req #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt,
output wire req, output wire [3:0] data);
reg busy; reg [3:0] d;
assign req = busy; assign data = d;
always @(posedge clk) begin
if (rst) busy <= 1'b0;
else begin
if (!busy && want) begin busy <= 1'b1; d <= nd; end
else if (busy && gnt) busy <= 1'b0;
else if (busy && BUG == 1 && want) d <= nd;
end
end
endmodule
module unitB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
hold_rule #(.ASSUME(0)) u_r (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt));
endmodule
module sysAB #(parameter BUG = 0) (input wire clk, input wire rst, input wire want, input wire [3:0] nd, input wire gnt);
wire req; wire [3:0] data; wire ov; wire [3:0] out; wire dp; wire [3:0] dh;
reg init0 = 1'b1; always @(posedge clk) init0 <= 1'b0; always @(*) if (init0) assume (rst);
b_req #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .want(want), .nd(nd), .gnt(gnt), .req(req), .data(data));
a_blk u_a (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out), .dbg_pend(dp), .dbg_held(dh));
always @(*) if (!init0 && BUG == 0) begin h_pend_req: assert (!dp || req); h_pend_held: assert (!dp || dh == data); end
a_spec u_s (.clk(clk), .rst(rst), .req(req), .data(data), .gnt(gnt), .ov(ov), .out(out));
endmoduleStep | B drives (req, data) and A sees gnt | What breaks |
|---|---|---|
2 | 1, 1; gnt 0 | B waits with word 1 |
3 | 1, 0; gnt 1 | B swapped in word 0 while waiting (the rule fails at this step in B's own proof); the grant arrives |
4 | - | A answers with the held word 1; |
The system proof for the good B passes with two helper assertions about A's internal state; they are asserted only when B is good, because they are not invariants of the faulty requester. The rule is now discharged: A is proved under X, B proves X, and the two together prove the specification.
Each assumption in a unit proof has a named assertion on the neighbour, in a table, with its proof result.
The rule text is shared between the assume and the assert, so the two cannot drift.
A neighbour fault is planted and shown to fail the assertion while the unit proof of the consumer still passes.
When integration fails and the unit proofs pass, list the assumptions of the failing block and look for the assertion that should discharge each. A row without an assertion, or with one that passes only because it is assumed, is the gap.
The system property is A's answer, which appears one cycle after the grant that uses B's changed word. B's assertion sees the changed word the cycle it appears.