X-Propagation

Three Ways to Read an Unknown

In four-state simulation the flop starts as X. The compare gives X, and an if on an X takes the else branch: the RTL hides the unknown, which is X-optimism. Gate-level simulation spreads the X instead, which is pessimism. A two-state simulator starts the flop at 0 and the bug never appears.

Formal is two-valued. A flop with no reset and no initial value is a free choice in the first step (F1.6). The solver picks mode = 3, and the enable fires before any firmware write: FAIL at reported step 3.

A Sampler Against the Full Set

The two-state run printed 0 early enables in 10000 cycles, and so did seeds 1, 2 and 3. Over 100 seeds, 11 started mode at 3. A random initial value is one draw per run; formal took all sixteen in one run of 491 ms.

Two Fixes, and the x You Write

The reset fixes the design. The assumption fixes only the proof: it says firmware always writes first, which is now a promise someone must keep and a line for the sign-off review. The k-induction attempt needs a helper or PDR, because an unreachable state with mode at 3 and no write looks fine for four steps.

An explicit x becomes a free value too. With SBY's default script the solver's model gains $anyseq cells where the RTL wrote 1'bx (2 here, none without it), so the assert on dbg fails at once. Commercial X-propagation apps model more than this; this page claims only what the open engine does.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) en |-> fw_seen);

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg fw_seen=0;   // firmware has written mode at least once (a write during reset counts too)
  always @(posedge clk) if (fw_wr) fw_seen <= 1;
  always @(posedge clk) if (!rst && en) assert(fw_seen);

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top xcmp
[files]
design.sv

1. Run the simulation twin

   Run the Verilator bench: 0 early enables. Which initial value did it use?

2. Run formal

   Run as it is: FAIL at reported step 3. Read mode at step 0 and look for a firmware write.

3. Add the reset

   Put rst in the mode branch and run: BMC PASS to depth 20.

4. Assume instead

   Remove the reset and add if ($initstate) assume(mode == 4'd0);: BMC PASS to depth 20. Where should that line be reviewed?

5. Write an x

   Add assign dbg = 1'bx; and assert(!dbg): FAIL at reported step 2.

Check Yourself

module xcmp(input clk, rst, fw_wr, input [3:0] fw_data, input start, output en);
  reg [3:0] mode;            // no reset: firmware writes it before start
  reg armed=0;
  always @(posedge clk) begin
    if (1'b0) mode <= 4'd0;   // FIX_RESET puts rst here
    else if (fw_wr) mode <= fw_data;
    if (rst) armed <= 0; else if (start) armed <= 1;
  end
  assign en = armed && mode == 4'd3;
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg fw_seen=0;   // firmware has written mode at least once (a write during reset counts too)
  always @(posedge clk) if (fw_wr) fw_seen <= 1;
  always @(posedge clk) if (!rst && en) assert(fw_seen);
`endif
endmodule