The first symptom of a register bug is software reading nonsense: a status bit stuck, an ID that changed, a configuration register that forgot its value. The cause is usually not exotic logic but a mismatch between the documented map and the RTL: the table says read-only, the RTL accepts the write. Proving the table directly, rather than a hand-written abstraction of it, removes the mismatch by construction.
The register table names every register with its offset, reset value and access type. A generator emits one family of checks per row: a reset-value check from the reset column, read-back and isolation checks for read-write registers, clear semantics for write-1-to-clear bits, and constancy for read-only registers. The running block has four registers: a read-write control register, a status register with two write-1-to-clear bits set by hardware pulses, a read-only ID holding a constant, and a read-write data register with a non-zero reset value.
Offset | Name | Access | Reset | Notes |
|---|---|---|---|---|
0 | CTRL | read-write | 0x00 | writes visible next cycle |
1 | STATUS | W1C bits 0..1, upper bits read 0 | 0x00 | hardware set wins over clear |
2 | ID | read-only | 0xA5 | writes ignored |
3 | DATA | read-write | 0x3C | non-zero reset catches reset bugs |
The generator below emits, per row, the labels of the checks that row requires, using the property names of the proof block, and the script checks them against the real block. The expected count is computed from the access kinds, and it is thirteen: three for each read-write register (reset, read-back, isolation), six for the status register (reset, one clear check per W1C bit, written-zero keeps, hardware set, reserved bits read 0), one for the constant ID. Isolation checks exist only for the two read-write registers, because that is the rule the generator applies: one isolation check per read-write row. A typo in a reset value is caught because the reset check text no longer matches the proof:
# labels and reset lines of the real proof block (pasted from it)
PROOF_LABELS = [
"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",
]
RESET_LINES = [
"a_id_const: assert (addr != 2'd2 || rdata == 8'hA5);",
"a_rst_ctrl: assert (ctrl == 8'h00);",
"a_rst_status: assert (status == 2'b00);",
"a_rst_data: assert (data == 8'h3C);",
]
table = [
("CTRL", 0, "8'h00", "rw", []),
("STATUS", 1, "2'b00", "w1c", ["done", "err"]),
("ID", 2, "8'hA5", "ro", []),
("DATA", 3, "8'h3C", "rw", []),
]
def emit(row):
name, off, reset, kind, bits = row
n = name.lower()
if kind == "rw":
return ["a_rst_" + n, "a_%s_rw" % n, "a_isolate_" + n]
if kind == "w1c":
return ["a_rst_" + n] + ["a_w1c_" + b for b in bits] + ["a_w1c_zero", "a_hw_set", "a_status_hi"]
if kind == "ro":
return ["a_id_const"]
raise ValueError(kind)
COUNT = {"rw": lambda r: 3, "w1c": lambda r: 4 + len(r[4]), "ro": lambda r: 1}
def reset_ok(row):
name, off, reset, kind, bits = row
label = "a_id_const" if kind == "ro" else "a_rst_" + name.lower()
text = "== " + reset if kind == "ro" else "%s == %s" % (name.lower(), reset)
return any(label + ":" in line and text in line for line in RESET_LINES)
checks = [c for row in table for c in emit(row)]
assert sorted(checks) == sorted(PROOF_LABELS), "every generated check exists in the proof and vice versa"
assert len(checks) == sum(COUNT[r[3]](r) for r in table) == 13
assert all(reset_ok(r) for r in table)
assert sum(1 for c in checks if c.startswith("a_isolate")) == 2
typo = table[:3] + [("DATA", 3, "8'h00", "rw", [])]
assert not all(reset_ok(r) for r in typo), "a reset typo no longer matches the proof"
assert sorted(c for r in table[:3] for c in emit(r)) != sorted(PROOF_LABELS), "a dropped row leaves checks missing"
print("PASS: 13 checks from 4 rows, each found in the proof block; a reset typo and a dropped row are both caught")The generated set is the property set inside the register module, proved whole: every property holds from reset, with write data sampled in the cycle it is presented. The partner runs the same proof against a design whose DATA reset value is wrong, the effect of the table typo above surviving into RTL. The wrong value exists at step 1, the first step after the reset edge, but a property that looks back one cycle judges it at the closing edge, so the proof reports it at step 2. The cycle table shows the value and the reporting step side by side:
// formal: prove 4 expect pass slang top csr_block
`define FORMAL
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;
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);
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
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
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
endmoduleStep | rst | DATA register | Property | Outcome |
|---|---|---|---|---|
0 | 1 | arbitrary | none | reset cycle, not checked |
1 | 0 | 0x00, table says 0x3C |
| wrong value present |
2 | - | - |
| counterexample reported here |
Root cause: the reset value disagrees with the table. Fix the RTL to the table, never the reverse. The reporting convention is the one used throughout this course: a property that reads $past is judged at its closing edge and reported one step after the state it is about.
// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
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;
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);
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
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
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 table covers every offset including holes, and every bit including reserved ones, with their access types.
Isolation checks exist for every writable register: proving each register correct alone is not enough. State which rows have them.
The reset column is proved with a property that looks at the cycle after reset, not one disabled during reset.
A reset-value failure names the register and the step; compare against the table before opening the RTL. A read-back failure one cycle after a write usually means the sampling is off by one, which the next lesson covers. An isolation failure means the decode overlaps: check the address conditions.
A non-zero reset distinguishes a correct reset from a register that never resets or that resets to zero by accident. With an all-zero map, a missing reset clause passes every reset check.