Covers catch dead triggers, but a subtler vacuity survives them: the trigger fires, the property passes, and still nothing is checked, because the check is not tied to the behaviour it claims. The classic shape is a data-integrity check that shadows the implementation expression instead of the specification, so corrupting the data corrupts the shadow identically and the comparison still matches.
Sensitivity is the test: mutate the design or the property and require a failure. A property that survives a bug in exactly what it claims to check is vacuous in effect, however lively its trigger. The acceptance gate is therefore a small mutation set per property: invert a term, shift by one, drop a conjunct. Every mutant must be caught by at least one property, and any surviving mutant is reported with the same seriousness as a counterexample. Mutation here is the same idea simulation coverage uses to check its own checks, linked below.
A one-stage pipeline register with a planted bug that clears bit 7 of the data. The first check below, run on the native front end (no front-end option in its header), compares the output against a shadow that reimplements the same buggy expression, so it passes on the buggy design: the corruption is invisible to it. The second check states the specification, that the output equals last cycle's input, and it fails.
// formal: bmc 6 expect pass top tag_loose define BUG=1
module tag_loose #(parameter BUG = 0) (input wire clk, input wire rst, input wire [7:0] d, output reg [7:0] q);
always @(posedge clk) begin
if (rst) q <= 8'd0;
else q <= (BUG == 1) ? {1'b0, d[6:0]} : d;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// shadow reimplements the implementation expression, bug included
reg [7:0] shadow;
always @(posedge clk) begin
if (rst) shadow <= 8'd0;
else shadow <= (BUG == 1) ? {1'b0, d[6:0]} : d;
end
always @(*) if (!init) begin
a_match: assert (q == shadow);
end
`endif
endmodule// formal: bmc 6 expect fail top tag_loose define BUG=1
module tag_loose #(parameter BUG = 0) (input wire clk, input wire rst, input wire [7:0] d, output reg [7:0] q);
always @(posedge clk) begin
if (rst) q <= 8'd0;
else q <= (BUG == 1) ? {1'b0, d[6:0]} : d;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// specification form: the output is last cycle's input, whatever it was
always @(posedge clk) if (!init && !$past(rst)) begin
a_pipe: assert (q == $past(d));
end
`endif
endmoduleRead the failing trace: drive input byte with bit 7 set in some cycle after reset, and the output in the next cycle shows bit 7 clear while the check demands last cycle's input. Root cause is the mask in the data path; fix is writing the full byte. The passing block above is kept in the lesson as the warning: a self-referential check is a tautology with a waveform.
One surviving mutant is an anecdote; a matrix is a process. The script below scores a tiny property set against four injected bugs and fails loudly while any mutant survives. The rule it enforces is the sign-off rule: every mutant killed, or the survivor is explained and given an owner.
# illustrative: a toy model (a wrapping counter and a data register) with injected faults.
# The kills are COMPUTED by running each mutant against each property, not typed in.
def count_next(c, mut):
if mut == "skip6" and c == 5: return 7
if mut == "stuck3" and c == 3: return 3
if mut == "no-wrap" and c == 7: return 8
return (c + 1) % 8
def run(mut, steps=12):
c, counts, pairs, prev = 0, [], [], 0
for i in range(steps):
d = (i * 37 + 129) % 256 # input bytes, some with bit 7 set
q = (prev & 0x7F) if mut == "mask-bit-7" else prev
pairs.append((prev, q)) # (what the register should show, what it shows)
counts.append(c)
c, prev = count_next(c, mut), d
return counts, pairs
PROPS = {
"a_bound": lambda t: all(x <= 7 for x in t[0]),
"a_step": lambda t: all(b == (a + 1) % 8 for a, b in zip(t[0], t[0][1:])),
"a_data": lambda t: all(want == got for want, got in t[1]),
}
MUTANTS = ["skip6", "stuck3", "no-wrap", "mask-bit-7"]
def kills(props):
return {m: [n for n, f in props.items() if not f(run(m))] for m in MUTANTS}
assert all(f(run("none")) for f in PROPS.values()), "every property holds on the good model"
weak = {n: PROPS[n] for n in ("a_bound", "a_step")}
k_weak, k_full = kills(weak), kills(PROPS)
survivors = [m for m in MUTANTS if not k_weak[m]]
assert survivors == ["mask-bit-7"], survivors # the gate fails: 3 of 4 killed
assert k_weak["no-wrap"] == ["a_bound", "a_step"]
assert not [m for m in MUTANTS if not k_full[m]] # adding a_data kills the last one
assert k_full["mask-bit-7"] == ["a_data"]
print("PASS: computed kills, gate fails at 3/4 (survivor mask-bit-7), passes at 4/4 with a_data")Each property has a mutation set, and the report shows every mutant killed or explicitly owned.
Data checks compare against the specification or an independent model, never against a copy of the logic.
The surviving-mutant list is empty or each entry names the added property that will kill it.
When a property never fails, suspect the check before celebrating the design. Invert one term of the property and rerun: if it still passes, the property is disconnected from the design. Then corrupt the data path with a one-line bug and rerun: if the data check still passes, it shadows the implementation. Both probes take minutes and each has saved sign-offs from a vacuous suite.
The check shadows the implementation instead of the specification, or it compares against a value derived from the corrupted path. Mutation with a bit-7 fault is the probe; an independent shadow or a symbolic tag is the fix.