Cone coverage says the proofs looked at the logic; assumption tables say what they leaned on. Neither says the checks bite. Mutation closes that gap by breaking the design on purpose: each injected fault must make at least one property fail. A mutant that survives, with every property still passing, is uncovered behaviour wearing a passing report.
A mutant is the design with one small fault: a missing full check, a cleared bit, a forgotten term. The property set scores the fraction killed, meaning at least one property fails on the mutant within the stated bound. The gate is strict: every surviving mutant either gains a new property that kills it or a written explanation with an owner. Mutation is also how a skipped behaviour is found: the FIFO bug that miscounts simultaneous push and pop never trips the range and flag properties, and is caught first by the internal pointer-consistency check, one step before the count-transition check sees it, which is exactly the property a surviving mutant would have demanded.
Three one-line faults in the four-entry FIFO, each caught by the full property set within small bounds. The first accepts a push into a full FIFO and overflows the count at step 6, so depth 7 catches it. The second accepts a pop when empty and fails at step 2. The third corrupts bit 7 of every written word and fails the data check at step 2. Each block below carries the complete module; only the fault parameter changes.
// 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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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);
`endif
endmodule// formal: bmc 3 expect fail slang top sync_fifo define BUG=2
`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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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);
`endif
endmodule// formal: bmc 3 expect fail slang top sync_fifo define BUG=5
`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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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);
`endif
endmoduleNotice what each mutant teaches: the overflow needs the full depth because four pushes must fill the FIFO first, while the empty-pop and the bit corruption show at once. Depth is part of the mutation result, and a mutant killed only past the sign-off bound is still a gap.
Now the harder case: a three-bit counter that skips the value 6. A bound check passes on the buggy design because the count never exceeds 7, so the mutant survives the suite. The surviving mutant is the finding: it exposes the missing step property. Adding the transition check kills it.
// formal: bmc 10 expect pass top skip_cnt define BUG=1
module skip_cnt #(parameter BUG = 0) (input wire clk, input wire rst, output reg [2:0] cnt);
always @(posedge clk) begin
if (rst) cnt <= 3'd0;
else cnt <= (BUG == 1 && cnt == 3'd5) ? 3'd7 : cnt + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_bound: assert (cnt <= 3'd7);
end
`endif
endmodule// formal: bmc 10 expect fail top skip_cnt define BUG=1
module skip_cnt #(parameter BUG = 0) (input wire clk, input wire rst, output reg [2:0] cnt);
always @(posedge clk) begin
if (rst) cnt <= 3'd0;
else cnt <= (BUG == 1 && cnt == 3'd5) ? 3'd7 : cnt + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_bound: assert (cnt <= 3'd7);
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (cnt == $past(cnt) + 3'd1);
end
`endif
endmoduleThe first block is a documented survivor: bounded to 10, the bound check passes on the buggy design. The second block adds the step property, which fails when the counter jumps from 5 to 7. The lesson for the suite: every counter needs its step property, and the survivor list is what tells you which one is missing.
The script below is the gate: it scores killed over total and fails while any mutant is unexplained. Run it over the sign-off ledger, not over a slide.
# mutation-score gate. The kills are COMPUTED: each mutant is a small model run on a
# fixed stimulus and each property is a function of the trace (illustrative models that
# mirror the FIFO mutants and the counter skip above; the proofs above are the real evidence).
def fifo_run(mut):
mem, wp, rp, count, gold, counts, bad_data = [0] * 4, 0, 0, 0, [], [], False
stim = [(0, 1, 0)] + [(1, 0, 0x80 | i) for i in range(5)] + [(0, 1, 0)] * 5 # (push, pop, data)
for push, pop, d in stim:
full, empty = count == 4, count == 0
do_push = push and (not full or mut == "fifo-ovf")
do_pop = pop and (not empty or mut == "fifo-undr")
if do_pop and gold and mem[rp] != gold[0]: bad_data = True
if do_pop and gold: gold.pop(0)
if do_push:
mem[wp] = d & 0x7F if mut == "fifo-bit7" else d
gold.append(d); wp = (wp + 1) % 4
if do_pop: rp = (rp + 1) % 4
count = (count + do_push - do_pop) % 8
counts.append(count)
return {"counts": counts, "bad_data": bad_data}
def cnt_run(mut):
c, seq = 0, []
for _ in range(12):
seq.append(c)
c = 7 if (mut == "cnt-skip" and c == 5) else (c + 1) % 8
return {"seq": seq}
PROPS = {"a_range": lambda t: all(x <= 4 for x in t["counts"]),
"a_data": lambda t: not t["bad_data"],
"a_bound": lambda t: all(x <= 7 for x in t["seq"]),
"a_step": lambda t: all(b == (a + 1) % 8 for a, b in zip(t["seq"], t["seq"][1:]))}
FIFO_PROPS, CNT_PROPS = ("a_range", "a_data"), ("a_bound", "a_step")
MUTANTS = {"fifo-ovf": fifo_run, "fifo-undr": fifo_run, "fifo-bit7": fifo_run, "cnt-skip": cnt_run}
def killed_by(active):
out = {}
for m, run in MUTANTS.items():
trace = run(m)
out[m] = [n for n in active if n in (FIFO_PROPS if run is fifo_run else CNT_PROPS) and not PROPS[n](trace)]
return out
assert all(PROPS[n](fifo_run("none")) for n in FIFO_PROPS) and all(PROPS[n](cnt_run("none")) for n in CNT_PROPS)
before = killed_by(["a_range", "a_data", "a_bound"])
survivors = [m for m in MUTANTS if not before[m]]
assert survivors == ["cnt-skip"], survivors # 3 of 4 killed: the gate fails
assert before["fifo-bit7"] == ["a_data"] and "a_range" in before["fifo-ovf"] and "a_range" in before["fifo-undr"]
after = killed_by(list(PROPS))
assert all(after[m] for m in MUTANTS) and after["cnt-skip"] == ["a_step"]
print("PASS: computed kills, 3/4 with survivor cnt-skip, 4/4 after adding a_step")The mutation set covers every property class: control, flags, data, and transitions each have a mutant aimed at them.
Each kill names the failing property, the bound, and the cycle; kills past the sign-off bound are flagged.
No mutant survives without an owner and a date; the survivor list is empty or worked.
Grow the mutant set whenever a bug escapes to silicon or simulation: the escape becomes a mutant first, then the property that kills it becomes permanent. Prefer mutants that mirror real failure shapes, such as a forgotten term or a masked bit, over random flips. And keep the suite fast enough to run the whole set on every change, because a gate too slow to run is a gate that gets skipped.
No. The kill is evidence the property can see the fault, but the sign-off bound cannot reach it. Either justify the deeper bound for that property or treat the mutant as surviving within the signed-off region.