A proof of an eight-bit datapath is slow, and someone narrows the data to two bits. It passes, and a corruption that only appears for particular bit patterns ships. The common explanation is that tracking one bit missed the pattern. It did not. Job of this lesson: tell the two abstractions apart with runs: tracking one bit of the full-width model, which finds the fault, and narrowing the datapath, which hides it.
Data independence says the design moves data without letting it steer control. Then following one free bit (a bit position the tool chooses, and the value written there) proves the property for every bit and every value. It keeps the full-width model: every other bit is still there and still free, so a corruption that depends on a pattern across bits is reachable and the chosen bit can sit where it shows. Narrowing removes the other bits. A fault whose condition reads the removed bits no longer exists in the model.
Abstraction | Keeps | Drops | Can hide a pattern fault? |
|---|---|---|---|
Track one bit of the full-width model | All bits, one watched bit | Nothing of the model | No: the tool chooses the bit and the pattern |
Narrow the datapath | Fewer bits | Bits and the logic that reads them | Yes |
Remove the datapath | Control only | All data | Yes, and data integrity is not checked at all |
A small datapath register flips bit 0 of the written word when the top two bits are both set. One free tracked bit tb and its shadow tsd watch q[tb]. On the full eight-bit model the proof of the good design passes at depth 4, and the faulty design fails at step 2 (depth 3; depth 2 passes). The tool picked bit 0 and a word with both top bits set.
// formal: prove 4 expect pass slang top dpath define BUG=0 define W=8
`define FORMAL
module dpath #(parameter W = 8, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire [W-1:0] wdata, output reg [W-1:0] q, output reg qv);
wire hit = (W >= 8) && (BUG == 1) && (wdata[W-1:W-2] == 2'b11);
always @(posedge clk) begin
if (rst) qv <= 1'b0;
else if (push) begin qv <= 1'b1; q <= hit ? {wdata[W-1:1], ~wdata[0]} : wdata; end
end
`ifdef FORMAL
reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
(* anyconst *) wire [2:0] tb; reg [2:0] tb_q; always @(posedge clk) tb_q <= tb;
always @(*) if (!init) assume (tb == tb_q);
always @(*) if (!init) assume (tb < W);
reg tsd; reg tv;
always @(posedge clk) if (rst) tv <= 1'b0; else if (push) begin tv <= 1'b1; tsd <= wdata[tb]; end
always @(*) if (!init && tv) a_bit: assert (q[tb] == tsd);
always @(*) if (!init) c_tracked: cover (tv);
`endif
endmodule// formal: bmc 3 expect fail slang top dpath define BUG=1 define W=8
`define FORMAL
module dpath #(parameter W = 8, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire [W-1:0] wdata, output reg [W-1:0] q, output reg qv);
wire hit = (W >= 8) && (BUG == 1) && (wdata[W-1:W-2] == 2'b11);
always @(posedge clk) begin
if (rst) qv <= 1'b0;
else if (push) begin qv <= 1'b1; q <= hit ? {wdata[W-1:1], ~wdata[0]} : wdata; end
end
`ifdef FORMAL
reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
(* anyconst *) wire [2:0] tb; reg [2:0] tb_q; always @(posedge clk) tb_q <= tb;
always @(*) if (!init) assume (tb == tb_q);
always @(*) if (!init) assume (tb < W);
reg tsd; reg tv;
always @(posedge clk) if (rst) tv <= 1'b0; else if (push) begin tv <= 1'b1; tsd <= wdata[tb]; end
always @(*) if (!init && tv) a_bit: assert (q[tb] == tsd);
always @(*) if (!init) c_tracked: cover (tv);
`endif
endmoduleNow the same fault with the datapath narrowed to two bits. The condition reads bits 7 and 6, which no longer exist, so the faulty design proves:
// formal: prove 4 expect pass slang top dpath define BUG=1 define W=2
`define FORMAL
module dpath #(parameter W = 8, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire [W-1:0] wdata, output reg [W-1:0] q, output reg qv);
wire hit = (W >= 8) && (BUG == 1) && (wdata[W-1:W-2] == 2'b11);
always @(posedge clk) begin
if (rst) qv <= 1'b0;
else if (push) begin qv <= 1'b1; q <= hit ? {wdata[W-1:1], ~wdata[0]} : wdata; end
end
`ifdef FORMAL
reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
(* anyconst *) wire [2:0] tb; reg [2:0] tb_q; always @(posedge clk) tb_q <= tb;
always @(*) if (!init) assume (tb == tb_q);
always @(*) if (!init) assume (tb < W);
reg tsd; reg tv;
always @(posedge clk) if (rst) tv <= 1'b0; else if (push) begin tv <= 1'b1; tsd <= wdata[tb]; end
always @(*) if (!init && tv) a_bit: assert (q[tb] == tsd);
always @(*) if (!init) c_tracked: cover (tv);
`endif
endmoduleRun | Result | Reading |
|---|---|---|
W = 8, good | Proven at depth 4 | The tracked bit stands for all eight bits |
W = 8, faulty, one tracked bit | Counterexample at step 2 | Tracked bit 0, word with bits 7 and 6 set |
W = 2, faulty | Proven at depth 4 | The fault's condition was abstracted away |
The third row is a proof of a different design. It is sound only if the removed bits cannot influence the checked behaviour, and here they can.
A written data-independence argument: which signals the control reads, and that none comes from the data path.
Narrowing, where used, comes with the argument that the removed bits feed no condition. A planted fault in the removed bits must still fail something.
One tracked bit or word is chosen by the tool, never pinned to a convenient position.
Before trusting a narrowed proof, plant a fault that reads the removed bits and confirm it fails somewhere. If the model must shrink, keep the bits that steer control, or any bit a condition reads, and narrow only the rest.
The other bits are still in the model and still free, so the solver can choose a word with both set and watch bit 0 flip. Narrowing deletes those bits.