X-Propagation and Unreachable Code

Two more standard questions are often answered with formal apps. X-propagation asks whether an unknown value, from a register without a reset or an uninitialized memory, can reach an output that matters. Unreachable code asks which parts of the RTL can never execute, such as a case branch for an input value that never arrives. This article answers both with plain property checks: the first with two copies of a design, the second with meant-to-fail checks for each branch.

8 min read | Intermediate

What You'll Learn

• Explain the X-propagation problem and why simulation handles it badly
• Check that unknown start values cannot reach the outputs, with two copies of a design
• Find code that can never execute under the environment assumptions
• Decide what to do with unreachable code

The X Problem

In simulation, a register without a reset starts as X, meaning unknown. Simulators propagate X through logic, but not exactly: an if (x) with an X condition takes the else branch, and some operators turn X into 0 or 1. So simulation can hide an X that would be a real random value in silicon, or report an X that cannot matter. This is called X-optimism and X-pessimism, and it is why X-propagation apps exist.

Formal has no X: every register has a real 0 or 1 value, chosen freely if there is no reset. That is a precise model of silicon. To ask "can an unknown start value matter?", compare two copies of the design that start with different free values.

The Two-Copy Check

Two instances of the design get the same inputs and the same reset. The formal tool gives the registers of each instance their own free start values. If, after the reset, any output can differ between the copies, then that output depends on a value the reset does not set.

module xprop_two (input clk, input rst, input in_valid, input [7:0] in_data);
  // two copies of the same design, same inputs; registers without a reset start at independent free values
  wire v_a, v_b; wire [7:0] d_a, d_b;
  valid_pipe u_a (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .out_valid(v_a), .out_data(d_a));
  valid_pipe u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .out_valid(v_b), .out_data(d_b));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // after reset, the start values must not matter: valid outputs agree, and so does valid data
  always @(*) if (!init && !rst) assert (v_a == v_b);
  always @(*) if (!init && !rst && v_a && v_b) assert (d_a == d_b);
`endif
endmodule

Applied to the pipeline from the reset and initial state article, whose second valid bit has no reset, the check fails at step 1: one copy shows a valid output right after reset, the other does not. The data registers have no reset either, but that is fine: the second assertion only compares data when it is valid. With the valid bit added to the reset, the check passes.

Unreachable Code

Code that can never execute is either dead logic, which wastes area and confuses readers, or a sign of a bug: a condition that was meant to happen but cannot. Simulation coverage reports such code as "not covered" without saying whether it ever could be. Formal answers the question.

This decoder has a branch for a reserved opcode that the upstream block never sends:

module dec_dead (input clk, input rst, input [1:0] op, input [7:0] x, output reg [7:0] y);
  always @(posedge clk)
    if (rst) y <= 8'd0;
    else case (op)
      2'd0: y <= x;
      2'd1: y <= x + 8'd1;
      2'd2: y <= x << 1;
      2'd3: y <= 8'hFF;                       // reserved opcode: upstream never sends it
    endcase
endmodule

With the environment assumption op != 3, a meant-to-fail check per branch shows which are reachable:

always @(*) assume (op != 2'd3);                         // environment: opcode 3 is reserved
always @(*) if (!init && !rst) assert (op != 2'd2);       // branch 2: fails, so reachable
always @(*) if (!init && !rst) assert (op != 2'd3);       // branch 3: passes, so unreachable

Branch 2 fails at step 1: reachable. Branch 3 passes: under the assumptions, it can never execute. An unreachable-code app does this for every branch, condition and expression automatically.

What to Do With Unreachable Code

• Intended defensive code, such as a reserved-opcode branch or a default recovery, stays, and is excluded from coverage with a note.
• Dead code left from an older version is removed.
• Code that should be reachable points to a bug, or to an over-constraining assumption, and must be investigated.

Running It in ChipVerify Lab

The example contains the pipeline with the missing reset and the two-copy check. Set the top module to xprop_two and run: it fails at step 1. The decoder example from this article is included as a second file; set the top module to dec_dead to run it.

Common Mistakes