A team pointed formal at a 32-bit multiplier and a firmware boot sequence, waited weeks, and concluded formal does not work, yet never pointed it at the arbiter that starved a requester in silicon. The failure was the selection, not the engine: formal is strong on control, protocol and register rules over all input sequences, and weak on wide arithmetic and long system flows.
Job of this lesson: decide, per requirement, whether it gets a formal obligation, and show what the obligation looks like when it does.
A requirement is formal-shaped when control state and interface rules decide it within a bounded neighbourhood of cycles, and simulation-shaped when it needs deep arithmetic, long histories, software or analogue behaviour:
The requirement is decided by... | Method | Example |
|---|---|---|
Control and protocol rules over all input sequences | Formal |
|
A bounded neighbourhood of cycles after a trigger | Formal |
|
Register access types and reset values | Formal |
|
Equality of two structures, or connectivity under a mode | Formal |
|
Wide arithmetic, or a long history | Simulation | A 32-bit multiplier |
Throughput over long traffic, software, analogue | Simulation |
|
Applied to the register block and the skid stage, the plan rows follow. Every formal row has a trigger cover, because a property whose trigger never fires proves nothing:
Id | Requirement | Method | Property | Trigger cover | Owner |
|---|---|---|---|---|---|
CSR-1 | ID register always reads 0xA5 | Formal |
|
| Block owner |
CSR-2 | Write-1-to-clear clears a set bit unless hardware sets it | Formal |
|
| Block owner |
CSR-3 | Reset values after reset | Formal |
|
| Block owner |
HS-1 | Nothing lost or duplicated under backpressure | Formal |
|
| Block owner |
HS-2 | A stalled output holds valid and data | Formal |
|
| Block owner |
HS-3 | Ready has no combinational path from the output | Formal |
|
| Block owner |
HS-4 | One word per cycle sustained | Simulation | Throughput measurement | Sustained traffic | Performance team |
The register block has a read-write control register, a two-bit write-1-to-clear status with hardware set pulses, a read-only constant and a data register. The first run proves all 13 assertions: prove 4 is the bounded check to depth 4 plus the induction step with k = 4, and both pass, so the result is proven for this model with reset assumed at step 0:
// 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
endmoduleThe failing partner injects the planted write-1-to-clear bug, where writing 1 sets the bit instead of clearing it. The bounded check fails at depth 4 on a_w1c_err:
// formal: bmc 4 expect fail slang top csr_block define BUG=1
`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
endmoduleRead the trace from reset: at step 1 a write of 1 reaches the status register with no hardware set; at step 2 the bit reads 1; at step 3 the clocked property reports it. Root cause is the inverted clear term; the fix restores the mask. A proof is worth its triggers, so the third block reaches the covers on the good design. This copy adds two covers to the design's own three, c_reset_released and c_ctrl_write, which rows CSR-3 and CSR-4 need; they are additions of this lesson, and the capstone lab adds a different fourth cover to its own copy. All five are reached within depth 4: the write and reset covers at step 1, c_w1c_clear and c_both_bits at step 2.
// formal: cover 4 expect reached 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
reg rst_q;
always @(posedge clk) rst_q <= rst;
always @(*) if (!init) begin
c_reset_released: cover (rst_q && !rst);
c_ctrl_write: cover (w_ctrl);
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
endmoduleEvery formal row names a requirement, a property, a trigger cover and an owner.
Simulation rows say why formal was refused.
No row claims a proof where only a bounded run exists; the run and depth are on the row.
Ask of each row which input sequences the method examines: formal answers all of them, simulation the sampled ones. A formal row with no trigger cover gets one before the pass is believed; a simulation row that keeps failing on control logic moves to formal.
Simulation: it is a throughput claim over long traffic, not a control rule over all sequences. The loss-and-duplication rule beside it goes to formal.