A proof passed and gate-level simulation failed on the same block: the model the tool proved was not the model the bench simulated. A don't-care branch had silently become a fixed value in the proof and an unknown in simulation. Fidelity gaps like these are normal and cheap once named. This lesson names them and runs the ones that run.
Job of this lesson: list where the proved model differs from the simulated one, and say what each difference demands instead.
The formal model is two-state: there is no unknown, so an unreset register is an arbitrary zero or one, never unknown. A proof must hold for every initial value, so a passing proof is not the solver picking a helpful value; what two-state cannot show is X-pessimism and X-optimism, which only simulation with unknowns shows. Around that centre sit constructs that flows treat differently. The table says which rows were run in this lesson and which are only stated:
Construct | Formal model | Simulation | What to do |
|---|---|---|---|
Unwritten memory entry (run below) | One arbitrary value, the same on every read | Unknown or stale value | Prove read-after-write, or reset the memory. |
Undriven wire or read port (run below) | A free input: a new arbitrary value in every cycle | Unknown | Lint for undriven nets; never rely on them. |
Case without a default | A latch: holds the previous value, arbitrary at start | Latch behaviour | Assign every branch. |
Default branch that assigns a don't care (run below) | Becomes the constant 0 in both front ends | Stays unknown | Assign a defined default. |
Combinational loop | Tool-dependent; not run here | Oscillation | Remove loops; lint before running. |
Parallel and full-case pragmas (run below) | Ignored: the missing branch is not excluded, so the input value that selects it stays reachable | May differ by synthesis setting | Avoid; assert one-hot explicitly. |
Delays, random calls, forces | Not run here: a delay is rejected as an error by the front end named in the header and may be silently dropped by another | Active | Keep formal wrappers free of them. |
The branch default: y = 4'bx is a don't care in simulation. In the proof it became the constant 0: y == 0 at the don't-care input passes, in both front ends. With an explicit default of 5 the same assertion fails, so the pass was a property of the constant the front end chose, not of the RTL.
// formal: bmc 4 expect pass slang top case_demo
`define FORMAL
module case_demo (
input wire clk,
input wire rst,
input wire [1:0] sel,
input wire [3:0] a, b, c,
output reg [3:0] y
);
always @(*) begin
case (sel)
2'd0: y = a;
2'd1: y = b;
2'd2: y = c;
default: y = 4'bx;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// judged at the one input value that the case treats as don't care or as default
always @(*) if (!init && sel == 2'd3) a_dont_care: assert (y == 4'd0);
`endif
endmodule// formal: bmc 4 expect fail slang top case_demo
`define FORMAL
module case_demo (
input wire clk,
input wire rst,
input wire [1:0] sel,
input wire [3:0] a, b, c,
output reg [3:0] y
);
always @(*) begin
case (sel)
2'd0: y = a;
2'd1: y = b;
2'd2: y = c;
default: y = 4'd5;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// judged at the one input value that the case treats as don't care or as default
always @(*) if (!init && sel == 2'd3) a_dont_care: assert (y == 4'd0);
`endif
endmoduleAn unwritten memory entry is not a free choice per read: its content is arbitrary but fixed, so two reads return the same value (bounded to 8 below). A read port nobody drives is different: a new arbitrary value each cycle, and the stability claim fails within 8.
// formal: bmc 8 expect pass slang top mem_demo
`define FORMAL
module mem_demo #(parameter FREE = 0) (
input wire clk,
input wire rst,
input wire [1:0] ra,
input wire we,
input wire [1:0] wa,
input wire [7:0] wd,
input wire [7:0] free_rd
);
reg [7:0] m [0:3];
// FREE = 1 models a read port that nobody drives: a new arbitrary value in every cycle
wire [7:0] rd = FREE ? free_rd : m[ra];
always @(posedge clk) if (we) m[wa] <= wd;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// follow entry 1 until it is first written
reg dirty = 1'b0, got = 1'b0;
reg [7:0] first;
always @(posedge clk) begin
if (we && wa == 2'd1) dirty <= 1'b1;
if (!got && !dirty && !(we && wa == 2'd1) && ra == 2'd1) begin first <= rd; got <= 1'b1; end
end
// a later read of the unwritten entry returns the same value
always @(*) if (!init && got && !dirty && ra == 2'd1) a_stable: assert (rd == first);
`endif
endmodule// formal: bmc 8 expect fail slang top mem_demo define FREE=1
`define FORMAL
module mem_demo #(parameter FREE = 0) (
input wire clk,
input wire rst,
input wire [1:0] ra,
input wire we,
input wire [1:0] wa,
input wire [7:0] wd,
input wire [7:0] free_rd
);
reg [7:0] m [0:3];
// FREE = 1 models a read port that nobody drives: a new arbitrary value in every cycle
wire [7:0] rd = FREE ? free_rd : m[ra];
always @(posedge clk) if (we) m[wa] <= wd;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// follow entry 1 until it is first written
reg dirty = 1'b0, got = 1'b0;
reg [7:0] first;
always @(posedge clk) begin
if (we && wa == 2'd1) dirty <= 1'b1;
if (!got && !dirty && !(we && wa == 2'd1) && ra == 2'd1) begin first <= rd; got <= 1'b1; end
end
// a later read of the unwritten entry returns the same value
always @(*) if (!init && got && !dirty && ra == 2'd1) a_stable: assert (rd == first);
`endif
endmoduleThe pragmas are a different kind of surprise. They look like a promise that the missing branch never happens, and a formal tool could have read them as an assumption. It does not: the cover for the unlisted selector value is reached, so the proof still covers that input, and the missing branch is simply an unwritten value, not a guarantee.
// formal: cover 4 expect reached slang top pragma_demo
`define FORMAL
module pragma_demo (
input wire clk,
input wire rst,
input wire [1:0] sel,
output reg [3:0] y
);
always @(*) begin
(* full_case, parallel_case *)
case (sel)
2'd0: y = 4'd1;
2'd1: y = 4'd2;
2'd2: y = 4'd3;
endcase
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// if the pragma were read as "sel is never 3", this cover could not be reached
always @(*) if (!init) c_sel3: cover (sel == 2'd3);
`endif
endmoduleX questions are answered by reset-determinism proofs (the state after reset does not depend on the free initial values) and by an X-aware analysis outside two-state formal: see X-Propagation in Formal.
The signoff states the two-state limit and where X questions are answered instead.
No simulation-only constructs; memories reset or covered by read-after-write; case statements have defined defaults.
Lint the formal wrappers for unsupported constructs before the first run, and diff wrapper against bench on every construct in the table. When formal and simulation disagree, read the model difference first: the usual cause is a value the RTL left undefined that the front end turned into a constant, or a two-state proof against a simulation that kept an unknown.
Both, for their own models: the proof holds for every initial value of the memory, while simulation keeps an unknown. Believe the system only after a read-after-write proof or initialisation removes the difference.
The front end turned the don't care into the constant 0, so the assertion checked that constant. An explicit default of 5 makes the same assertion fail.