The register proof passes, and nobody knows whether it checks anything. The only evidence that a property can fail is a failure: an injected bug it catches. Without that, the suite is a collection of tautologies with good timing. This lesson's one job is the mutation gate: every property must kill its mutants, and the score must count every mutant.
A mutation set per property inverts a term, shifts by one, or removes a term: set instead of clear, writable instead of read-only, wrong reset value. The strong suite kills all three, each at the step its shortest trace needs. A weak suite, here the same file with the two write-1-to-clear checks left out, runs clean on the first mutant, which is exactly the gap the score must show. Dropping the survivor from the denominator inflates the score to perfect, the oldest lie in coverage arithmetic.
Steps are counted from the reset step as step 0, and a run of depth D checks steps 0 to D minus 1. A mutant whose run fails at depth D and passes at depth D minus 1 therefore fails first at step D minus 1.
The register block carries thirteen assertions over its four registers. The listing is the running register block with one lesson-local parameter, WEAK, that drops the two write-1-to-clear checks. On the good design the whole set is proved:
// formal: prove 4 expect pass slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleWriting one to a status bit sets it instead of clearing it. The two write-1-to-clear checks catch the inversion at depth 4; the run one depth shorter passes, so the first failing step is 3:
// formal: bmc 4 expect fail slang top csr_block define BUG=1
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule// formal: bmc 3 expect pass slang top csr_block define BUG=1
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleThe read-only identifier accepts writes. The constant check catches the very first read after a write, at depth 3, first failing step 2:
// formal: bmc 3 expect fail slang top csr_block define BUG=2
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule// formal: bmc 2 expect pass slang top csr_block define BUG=2
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleThe data register resets to zero instead of its specified value. The reset-value check, which looks back at the reset edge rather than hiding behind a disable, catches it on the first cycle after reset, at depth 3, first failing step 2:
// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule// formal: bmc 2 expect pass slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleNow the weak property set, the same file with WEAK set to 1, against the first mutant. The run reaches depth 10 with no counterexample: the mutant survives. The other two mutants still fail under the weak set, because the checks that catch them (the constant ID check and the reset-value check) are not among the ones removed, as the next two runs show:
// formal: bmc 10 expect pass slang top csr_block define BUG=1 define WEAK=1
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleThe other two mutants, run against the same weak set, are still killed:
// formal: bmc 3 expect fail slang top csr_block define BUG=2 define WEAK=1
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block define BUG=3 define WEAK=1
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
// Lesson-local parameter: WEAK=1 leaves out the two write-1-to-clear checks (a weaker property set).
module csr_block #(parameter BUG = 0, parameter HELPER = 1, parameter WEAK = 0) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
if (WEAK == 0) begin
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
end
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleThe score below counts the kills. Its depths are the headers of the runs above, and it turns them into steps by the rule stated in the core idea. The last lines catch the inflation: dropping the surviving mutant from the denominator returns a perfect score over fewer mutants:
import json
# [name, BUG, depth that fails, depth one shorter that passes] and [BUG, depth, result] are the headers of the runs above.
KILLS = json.loads('[["w1c-set-instead-of-clear",1,4,3],["id-writable",2,3,2],["data-reset-value",3,3,2]]')
WEAK = json.loads('[[1,10,"pass"],[2,3,"fail"],[3,3,"fail"]]')
def first_step(fail_depth, pass_depth):
# step 0 is the reset step; a run of depth D checks steps 0 to D - 1, so a kill at depth D is first seen at step D - 1
if pass_depth != fail_depth - 1:
raise ValueError("the run one depth shorter must pass: the kill depth is not the first failing depth")
return fail_depth - 1
strong = {name: first_step(f, p) for name, bug, f, p in KILLS}
assert strong == {"w1c-set-instead-of-clear": 3, "id-writable": 2, "data-reset-value": 2}
names = {bug: name for name, bug, f, p in KILLS}
weak = {names[bug]: (first_step(d, d - 1) if result == "fail" else None) for bug, d, result in WEAK}
assert weak == {"w1c-set-instead-of-clear": None, "id-writable": 2, "data-reset-value": 2}
def score(table):
killed = sum(1 for s in table.values() if s is not None)
return killed, len(table)
assert score(strong) == (3, 3) and score(weak) == (2, 3)
# a kill depth with a wrong partner depth is refused, so the steps cannot be typed in by hand
try:
first_step(4, 2)
raise SystemExit("FAIL: an inconsistent pair of depths was accepted")
except ValueError:
pass
dropped = {m: s for m, s in weak.items() if s is not None}
assert score(dropped) == (2, 2) and len(dropped) < len(weak) # inflated: perfect, over fewer mutants
assert len(weak) == len(strong) # the honest check: the denominator never shrinks
print("PASS: strong kills 3 of 3; weak 2 of 3; dropped-mutant inflation caught")Every property has a mutation set: invert a term, shift by one, remove a term, and the property fails each variant.
The score counts every mutant in the denominator: a surviving mutant lowers the score, never disappears from it.
Each kill names its step: the shortest trace is quoted, read from a run one depth shorter that passes, so a kill at an unexpected depth gets investigated, not celebrated.
Rerun the mutants on every RTL change: a property that killed its mutants last week may check nothing this week if its cone moved. When a new mutant survives, read it as a specification gap first: is the behaviour it exhibits actually forbidden, and by which sentence? If no sentence forbids it, the specification needs the sentence before the property needs the term.
A surviving mutant was dropped from the count instead of fixed or waived with a reason. The score now measures a smaller suite. Restore the mutant to the table and either kill it or record why it is out of scope.