Helpers compose: pointer consistency carries occupancy, occupancy carries the transition rules. Each lemma is proven first and used next, which turns one hard proof into a stack of easy ones. The stack is sound only with its audit: every lemma used must be proven, and the dependency graph must have no cycle, because a cycle is two properties assuming each other, which proves nothing.
A lemma stack orders the proof bottom-up. Level 1 proves the state consistency that needs no help: the FIFO range, flags, exclusion and pointer relation close at k equal to 1. Level 2 proves the transition rules, which read the previous cycle, with the level-1 properties used as assumptions. That is sound only because the level-1 run proved them for the same design. The first two runs below are the stack. The next two show what the audit is for. Run level 2 on the FIFO variant that accepts a push when full, with the level-1 properties still assumed, and it passes, because the assumed range property forbids the overflow state. Run level 1 on that variant and it fails at depth 7, so level 1 is not proven for this design, the stack is not sound, and the pass above it is a false pass.
// formal: prove 1 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.
// This copy keeps the control properties only: no data-integrity harness.
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));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
`endif
endmoduleLevel 1, asserted: range, flags, exclusion and the pointer relation prove at k equal to 1 on the good design.
// 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.
// This copy keeps the control properties only: no data-integrity harness.
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);
// ---- level-1 lemmas, USED as assumptions (sound only because a separate run proved them) ----
always @(*) if (!init) begin
u_range: assume (count <= 3'd4); // no overflow, no underflow wrap
u_flags: assume (full == (count == 3'd4) && empty == (count == 3'd0));
u_not_both: assume (!(full && empty));
// occupancy equals pointer distance (mod 4)
u_ptr: assume (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
`endif
endmoduleLevel 2: the transition rules prove, with the level-1 properties assumed. The assumptions are sound here, because the previous run proved them.
// formal: bmc 12 expect pass 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.
// This copy keeps the control properties only: no data-integrity harness.
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);
// ---- level-1 lemmas, USED as assumptions (sound only because a separate run proved them) ----
always @(*) if (!init) begin
u_range: assume (count <= 3'd4); // no overflow, no underflow wrap
u_flags: assume (full == (count == 3'd4) && empty == (count == 3'd0));
u_not_both: assume (!(full && empty));
// occupancy equals pointer distance (mod 4)
u_ptr: assume (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
`endif
endmoduleThe same level-2 run on the push-when-full variant also passes to depth 12. This is the false pass of an unproven lemma: nothing in the run says that the assumed range property is false for this design.
// 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.
// This copy keeps the control properties only: no data-integrity harness.
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));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
`endif
endmoduleLevel 1 on the variant fails at depth 7, as it should. This is the evidence the audit needs: the lemma is not proven for this design, so everything stacked on it is conditional.
def audit(lemmas):
for name, l in lemmas.items():
if not l["proven"]:
raise ValueError("unproven lemma: " + name)
for u in l["uses"]:
if u not in lemmas:
raise ValueError("unknown lemma: " + u)
order, marks = [], {}
def visit(n, stack):
if marks.get(n) == "done":
return
if n in stack:
raise ValueError("cycle through: " + n)
stack.add(n)
for u in lemmas[n]["uses"]:
visit(u, stack)
stack.discard(n)
marks[n] = "done"
order.append(n)
for n in lemmas:
visit(n, set())
return order
def stack(level1_proven):
return {"L1_state": {"uses": [], "proven": level1_proven},
"L2_transitions": {"uses": ["L1_state"], "proven": True}}
# good design: level 1 was proven by the first run
assert audit(stack(True)) == ["L1_state", "L2_transitions"]
# push-when-full variant: the level-1 run failed, so the stack is rejected although level 2 "passes"
caught_open = False
try:
audit(stack(False))
except ValueError as e:
caught_open = "L1_state" in str(e)
assert caught_open, "audit missed the unproven level-1 lemma"
# a circular pair is rejected too
cyclic = {"L_a": {"uses": ["L_b"], "proven": True}, "L_b": {"uses": ["L_a"], "proven": True}}
caught_cycle = False
try:
audit(cyclic)
except ValueError:
caught_cycle = True
assert caught_cycle, "audit missed the circular pair"
# a lemma used but not listed is rejected
caught_unknown = False
try:
audit({"L2": {"uses": ["L1"], "proven": True}})
except ValueError:
caught_unknown = True
assert caught_unknown, "audit missed the unknown lemma"
print("PASS: stack ordered; unproven level, cycle and unknown lemma rejected")Lemmas are listed bottom-up with each level proven before use, and the dependency graph is filed.
The audit rejects cycles and unproven lemmas mechanically, not by inspection, and is rerun for every design variant.
Every lemma states a design truth a reviewer can read, not a proof artefact.
Rerun the audit on every proof change: a new helper that uses an unproven lemma fails the audit before it wastes a run. Rerun the lower levels on every bug variant too: a stack proven on the good design says nothing about the design it was not proven on. When the stack grows past three levels, check whether two levels state the same relation differently and merge them: deep stacks often hide one duplicated idea.
No: the proof is conditional on an unchecked claim. Prove the lemma first or remove the use; the audit exists precisely because inspection misses exactly this ordering fault.