Three planted register faults reach only four of the thirteen properties. The other nine, reset values, read-back, isolation, the read of the status bits and the race between a set and a clear, can only be trusted once a mutant has made each of them fail. This lesson gives the causes of the faults and then the nine mutants.
Variant | Cause in the listing | Fix | Fails (step), smallest depth |
|---|---|---|---|
W1 | The status update ORs the write data into the status instead of clearing the bits written as 1. |
|
|
W2 | The identification register is a flop that accepts writes. | Drive the read from the constant. |
|
W3 | The reset branch loads 0x00 into DATA. | Load 0x3C. |
|
W1 needs no hardware set: a write of 1 to the status register at step 1 leaves the bit set at step 2, and the clocked property reports it at step 3. W3 exists from step 1, right after the reset edge, and is reported at step 2: a reset check hidden behind a disable would miss it, so the properties use the history of the reset signal instead.
// formal: bmc 4 expect fail slang top csr_block define BUG=1
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block define BUG=2
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmoduleThe map says a hardware set wins over a clear in the same cycle. The cover c_set_collision is reached at step 2 in the cover run of stage 2 (a set pulse and a clear of the same bit together), and a_hw_set is the property that says who wins. The first block below shows why a window of one is not enough: the clocked properties read history, so the induction step fails at window 1 on nine of the eleven clocked properties.
// formal: prove 1 expect unproven slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmoduleEach mutant is the register listing with one edit, killed by the property named. Each is killed by its named property, and no other register property fails first; the race mutant is killed by a_hw_set only.
Mutant | Change | Killer | Smallest depth |
|---|---|---|---|
| bit 2 of the STATUS read value is stuck at 1 |
| 2 |
| CTRL resets to 0x01 |
| 3 |
| STATUS resets to 2'b01 |
| 3 |
| CTRL stores the written value with bit 0 inverted |
| 4 |
| DATA stores the written value with bit 7 forced to 1 |
| 4 |
| writing 0x00 to STATUS clears both bits |
| 5 |
| a write to the ID address also writes CTRL |
| 4 |
| a write to the ID address also writes DATA |
| 4 |
| a clear in the same cycle beats a hardware set |
| 4 |
// formal: bmc 2 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-status-hi: bit 2 of the STATUS read value is stuck at 1
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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) ? {5'b0, 1'b1, 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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-rst-ctrl: CTRL resets to 0x01
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h01;
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-rst-status: STATUS resets to 2'b01
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b01;
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 4 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-ctrl-rw: CTRL stores the written value with bit 0 inverted
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 ^ 8'h01;
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 4 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-data-rw: DATA stores the written value with bit 7 forced to 1
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 | 8'h80;
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 5 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-w1c-zero: writing 0x00 to STATUS clears both bits
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0] & ((wdata[1:0] == 2'b00) ? 2'b00 : 2'b11));
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 4 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-isolate-ctrl: a write to the ID address also writes CTRL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 || w_id) 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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 4 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-isolate-data: a write to the ID address also writes DATA
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 || w_id) 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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmodule// formal: bmc 4 expect fail slang top csr_block
`define FORMAL
// mutant csr-m-race: a clear in the same cycle beats a hardware set
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
// 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
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]) : (status & ~wdata[1:0]);
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 properties: true in every cycle after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
end
// ---- transition properties: they look one cycle back ----
always @(posedge clk) if (!init) begin
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
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
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]);
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
a_hw_set: assert (!$past(set_done) || status[0]);
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// ---- covers ----
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);
c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
end
`endif
endmoduleLISTING = {"a_id_const", "a_status_hi", "a_rst_ctrl", "a_rst_status", "a_rst_data", "a_ctrl_rw", "a_data_rw",
"a_w1c_done", "a_w1c_err", "a_w1c_zero", "a_hw_set", "a_isolate_ctrl", "a_isolate_data"}
FAILS_ON = {"a_id_const": "csr-W2", "a_status_hi": "csr-m-status-hi", "a_rst_ctrl": "csr-m-rst-ctrl", "a_rst_status": "csr-m-rst-status",
"a_rst_data": "csr-W3", "a_ctrl_rw": "csr-m-ctrl-rw", "a_data_rw": "csr-m-data-rw", "a_w1c_done": "csr-W1", "a_w1c_err": "csr-W1",
"a_w1c_zero": "csr-m-w1c-zero", "a_hw_set": "csr-m-race", "a_isolate_ctrl": "csr-m-isolate-ctrl", "a_isolate_data": "csr-m-isolate-data"}
assert set(FAILS_ON) == LISTING, "every register property has something that fails it"
planted = [m for m in FAILS_ON.values() if m.startswith("csr-W")]
assert sorted(set(planted)) == ["csr-W1", "csr-W2", "csr-W3"]
assert len(set(FAILS_ON.values())) == 12, "three planted faults and nine mutants; two properties share W1"
untested = LISTING - {p for p, m in FAILS_ON.items() if m.startswith("csr-W")}
assert len(untested) == 9, "nine of the thirteen properties need a mutant"
dropped = dict(FAILS_ON)
del dropped["a_hw_set"]
assert set(FAILS_ON) - set(dropped) == {"a_hw_set"} and set(dropped) != LISTING, "the check notices a property without a failure"
print("PASS: all 13 register properties have a failure of their own; nine of them need a mutant")Every register property fails on something, shown by a run: three planted faults and nine mutants.
The race is a property and a cover: the cover witnesses the collision, the property says the set wins.
A reset fault is reported one step after it appears.
A write-1-to-clear failure that needs a hardware set pulse in its trace is a reading of the map that gives the clear priority, not a design fault. A reset failure at step 2 means the value was already wrong at step 1: look at the reset branch, not at the write logic.
Clearing and setting in one cycle is the only case where the priority matters; the clear and read-back properties exclude it or never reach it.
The stuck bit is on the combinational read path, so the state property fails in the first cycle after reset, with no write needed.