Every contract in the previous lessons was true because someone ran its proof. A table that lists a contract and a status that nobody checks is the same promise in a different file. Job of this lesson: the contract table, and a checker that reads the assertion labels of the real text and the results of the proof runs on this page, so that a row cannot be marked proved without a run behind it.
Column | Content | Checked against |
|---|---|---|
Assumption | The statement, and where it is assumed | The consumer's text |
Owner | The block that must keep it | The neighbour's text |
Discharge | The assertion label on that block | The labels in the neighbour's file |
Status | Proven, fails or unproven | The proof run of the neighbour |
Two contracts: the decoder's assumption count <= 9, owed by the decade counter and discharged by its a_range; and the requester's two rules, r_req and r_dat, discharged on the requester block B. Each neighbour has a proof run on this page, one passing and one with a planted fault:
// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True, but NOT inductive on its own: the unreachable states
// 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever, so no k
// of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmodule// formal: bmc 11 expect fail slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True, but NOT inductive on its own: the unreachable states
// 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever, so no k
// of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmodule// 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));
endmoduleThe checker reads the assertion labels of each module from the real text, and the run results from the four runs above. A row is accepted only when its discharge is an assertion in the neighbour, the neighbour is not the consumer, and a proved status has a passing run. A fault in the neighbour turns the row to "fails", which the table must show.
import json
ASSERTS = json.loads('{"mod10_counter":["a_not15","a_range","a_tc","a_step","a_hold"],"hold_rule":["r_req","r_dat"]}') # labels of the assertions in each module
RESULTS = {"mod10_counter BUG=0":"pass","mod10_counter BUG=1":"fail","unitB BUG=0":"pass","unitB BUG=1":"fail"} # results of the runs above
def check(rows):
problems = []
for assumption, consumer, module, label, run, status in rows:
if module == consumer:
problems.append(assumption + ": discharged on the block that assumes it")
if label not in ASSERTS.get(module, []):
problems.append(assumption + ": " + label + " is not an assertion of " + module)
actual = RESULTS.get(run, "no run")
if status == "proven" and actual != "pass":
problems.append(assumption + ": marked proven, run says " + actual)
if status == "fails" and actual == "pass":
problems.append(assumption + ": marked fails, run passes")
return problems
good = [("count <= 9", "decode10", "mod10_counter", "a_range", "mod10_counter BUG=0", "proven"),
("req holds until grant", "unitA", "hold_rule", "r_req", "unitB BUG=0", "proven"),
("data holds until grant", "unitA", "hold_rule", "r_dat", "unitB BUG=1", "fails")]
assert check(good) == [], check(good)
bad = [("count <= 9", "decode10", "decode10", "a_range", "mod10_counter BUG=0", "proven"),
("req holds", "unitA", "hold_rule", "a_does_not_exist", "unitB BUG=0", "proven"),
("data holds", "unitA", "hold_rule", "r_dat", "unitB BUG=1", "proven")]
found = check(bad)
assert any("on the block that assumes" in p for p in found), found
assert any("not an assertion" in p for p in found) and any("run says fail" in p for p in found), found
assert len(found) == 4, found
print("PASS: the table is checked against the real labels and the run results; bad rows rejected")The last row of good is the honest status of a faulty neighbour: the table says "fails" and the run agrees. A table that said "proven" for the same run is the third rejected row.
Every assumption in every unit proof appears once in the table, with the assertion that discharges it.
No row is discharged on the block that assumes it, and none points at an assumption instead of an assertion.
The table is part of signoff: an open row blocks the sign-off, whatever the unit proofs say.
When the checker rejects a row, read its message. "Discharged on the block that assumes it" is the circular case, "not an assertion of" a module means the label was renamed or never written, and "run says fail" means the neighbour is faulty and the row must say fails. After any change to a neighbour, rerun its proof and the check together: a stale proven status is what the check exists to catch. The bad table above shows four different rejections, so the checker is itself seen to fail.
A typed status can say proven for a neighbour whose proof fails or was never run. The run result is the only thing that can contradict it.