A property set was reviewed rule by rule and still shipped a hole: a rule with an assertion and no cover for its antecedent. The tables below are the rule lists of the FIFO, the arbiter and the bridge. Job of this lesson: give each rule its role and the lesson that teaches it, and check mechanically that every implication-style rule has an assertion and a cover in the file.
Design | Rule | Role | Owning lesson |
|---|---|---|---|
FIFO | A full FIFO ignores a push ( | Assert; antecedent cover | Spec Sentence to Property |
FIFO | Reset empties it ( | Assert | Spec Sentence to Property |
FIFO | Words come out in order ( | Assert; antecedent cover | Symbolic Constants and Tracked Items |
Arbiter | At most one grant, grant implies request | Assert | This lesson |
Arbiter | Nobody waits more than 3 cycles ( | Assert; one requester per run is not proof of all | Parameterised Property Sets |
Bridge | Nothing lost or duplicated ( | Assert | Assumption Taxonomy and Ownership |
Bridge | Upstream holds valid until accepted | Assumed here; asserted in the upstream block | Checker Modules and Wrapper Harnesses |
Bridge | A stalled output holds valid and data | Assert | Checker Modules and Wrapper Harnesses |
Bridge | Tracked word is delivered intact ( | Assert with helpers; tracked-word pin assumed | Assumption Taxonomy and Ownership |
The checker below reads the assertion and cover labels of each design file, as they are in the text the proofs run on. A rule row names its assertion and, when it is an implication, the cover for its antecedent. It reports a rule whose assertion does not exist, whose cover does not exist, or that needs a cover and has none. On the shipped FIFO file four rules have no antecedent cover (three transition rules and the tracked-data rule); on the FIFO file with the covers added the set is complete.
import json
FILES = json.loads('{"fifo":{"asserts":["a_range","a_flags","a_not_both","a_ptr","a_push_inc","a_pop_dec","a_ovf_ign","a_both","a_data","a_tracked"],"covers":["c_full","c_empty_after_use","c_both"]},"fifo_reset":{"asserts":["a_range","a_flags","a_not_both","a_ptr","a_push_inc","a_pop_dec","a_ovf_ign","a_both","a_data","a_tracked","a_reset"],"covers":["c_full","c_empty_after_use","c_both"]},"fifo_plus":{"asserts":["a_range","a_flags","a_not_both","a_ptr","a_push_inc","a_pop_dec","a_ovf_ign","a_both","a_data","a_tracked"],"covers":["c_full","c_empty_after_use","c_both","c_push","c_pop","c_ovf","c_rd_tracked"]},"arbiter":{"asserts":["a_onehot0","a_no_phantom","a_work_cons","a_wt0","a_wt1","a_wt2","a_wt3","h_wt0","h_wt1","h_wt2","h_wt3"],"covers":["c_g0","c_g1","c_g2","c_g3","c_contend","c_idle"]},"bridge":{"asserts":["a_skid_needs_out","a_conserve","a_valid_hold","a_data_hold","a_no_ready_comb","a_data","h_in_out","h_in_skid","h_pos"],"covers":["c_stall","c_skid_used","c_backpress_full","c_flow"]}}')
def check(design, rules):
have = FILES[design]
problems = []
for rule, assertion, cover, needs_cover in rules:
if assertion not in have["asserts"]:
problems.append(rule + ": no assertion " + assertion)
if cover is not None and cover not in have["covers"]:
problems.append(rule + ": no cover " + cover)
if needs_cover and cover is None:
problems.append(rule + ": an implication with no antecedent cover")
return problems
fifo_rules = [("push alone adds one", "a_push_inc", "c_push", True),
("pop alone removes one", "a_pop_dec", "c_pop", True),
("full ignores a push", "a_ovf_ign", "c_ovf", True),
("push and pop together", "a_both", "c_both", True),
("words in order", "a_data", "c_rd_tracked", True)]
shipped = check("fifo", fifo_rules)
assert len(shipped) == 4 and all("no cover" in p for p in shipped), shipped
assert check("fifo_plus", fifo_rules) == []
assert check("fifo_reset", [("reset empties it", "a_reset", None, False)]) == [] # the reset rule lives in its own file
assert check("fifo", [("reset empties it", "a_reset", None, False)]) != [] # and is missing from the shipped one
assert check("fifo_plus", [("full ignores a push", "a_ovf_ign", None, True)]) != [] # no cover given
assert check("fifo_plus", [("bad", "a_does_not_exist", "c_ovf", True)]) != [] # no such assertion
assert check("bridge", [("stalled output holds", "a_valid_hold", "c_stall", True),
("data holds", "a_data_hold", "c_stall", True),
("nothing lost", "a_conserve", None, False)]) == []
assert check("arbiter", [("one grant", "a_onehot0", "c_g0", True),
("no phantom", "a_no_phantom", "c_idle", False),
("bounded wait", "a_wt3", "c_contend", True)]) == []
print("PASS: shipped FIFO set has 4 rules without a cover; with the covers added all 5 rules, and the bridge and arbiter sets, are complete")The checker found that four rules have no antecedent cover in the shipped file. The extended file adds them, and all covers are reached within depth 6; a cover not reached within N would be inconclusive, not unreachable:
// formal: cover 6 expect reached slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
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) ----
// free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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 value 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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
// antecedent covers for the rules above
always @(*) if (!init) begin
c_push: cover (push && !pop && !full);
c_pop: cover (pop && !push && !empty);
c_ovf: cover (push && !pop && full);
c_rd_tracked: cover (tv && !empty && rptr == tslot);
end
`endif
endmodule// formal: prove 4 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
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) ----
// free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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 value 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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
// antecedent covers for the rules above
always @(*) if (!init) begin
c_push: cover (push && !pop && !full);
c_pop: cover (pop && !push && !empty);
c_ovf: cover (push && !pop && full);
c_rd_tracked: cover (tv && !empty && rptr == tslot);
end
`endif
endmodule// formal: bmc 7 expect fail slang top sync_fifo define BUG=1
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
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) ----
// free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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 value 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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
// antecedent covers for the rules above
always @(*) if (!init) begin
c_push: cover (push && !pop && !full);
c_pop: cover (pop && !push && !empty);
c_ovf: cover (push && !pop && full);
c_rd_tracked: cover (tv && !empty && rptr == tslot);
end
`endif
endmoduleThe set still proves with the covers added and still fails on the overflow fault at step 6 (depth 7); the covers constrain nothing. The same rule lists drive the checkers of the bridge and the arbiter.
A table per design, with every rule's role. A rule listed as assumed has an assertion on the neighbour named in the contract table.
Every implication-style rule has a cover that the checker finds in the file, and that a run reaches.
The set is run in two sizes or modes where the design has them, and the planted faults of the design fail the rules the table says they fail.
Rerun the completeness check whenever a rule or a file changes, and read its output as a list of work: on the shipped FIFO file it names four rules without an antecedent cover, and with the extended file it names none. A rule whose label is not in the file means a rename broke the table. Then run the covers: each must be reached, and the set must still prove and still fail the overflow fault at depth 7, which shows the added covers constrain nothing.
For a state property that is not an implication, such as at most one grant: it holds at every step with no trigger to reach. For an implication a missing cover is a failure.