X-propagation, security and post-silicon debug

X-propagation

Registers without reset start as X (unknown). Simulation treats X optimistically or pessimistically depending on the construct — an if (x) takes the else branch, hiding problems. An X-propagation app models X as "could be 0 or 1" and checks that unknown values cannot reach important places, such as outputs qualified by a valid signal:

// The data path is intentionally not reset (saves area) ...
always_ff @(posedge clk) if (load) data_q <= data_in;

// ... so we must prove the unknown value never escapes while it matters
a_no_x_out: assert property (@(posedge clk) disable iff (rst) out_valid |-> !$isunknown(out_data));

In simulation, $isunknown catches X directly. Formal X-prop apps implement the same intent by comparing two copies of the design whose uninitialised values may differ: if the outputs can differ while valid, an X can leak.

Security and information flow

Security apps ask questions such as "can the secret key ever influence the debug bus?" or "can user-mode software observe a value written in secure mode?". Technically this is again a two-copy comparison: run two copies of the design with identical inputs except for the secret; if any observable output can differ, information flows from the secret to that output.

Post-silicon debug

When a chip fails in the lab, engineers typically have only a few clues: a hung interface, an error register value, a scan dump of some flops. Simulation struggles to reproduce such failures because nobody knows which stimulus triggered them. Formal turns the problem around: encode the symptoms as a cover and ask the tool to find any trace that reaches them.

1. Pick the smallest block that can explain the symptom.
2. Write the observed state as a cover, e.g. cover property (err_code == 4'h9 && fifo_full && !pop).
3. Add assumptions for everything known about the lab setup (modes, clock ratios, register settings).
4. If the cover is reachable, the trace is a candidate root cause — confirm it, fix it, and use the cover as a regression check.
5. If unreachable, either the block choice or an assumption is wrong — broaden step by step.

Chapter takeaways