xprop - formal x propagation

yosys> help xprop

xprop [options] [selection]

This pass transforms the circuit into an equivalent circuit that explicitly
encodes the propagation of x values using purely 2-valued logic. On the
interface between xprop-transformed and non-transformed parts of the design,
appropriate conversions are inserted automatically.

-split-inputs

-split-outputs

-split-ports

Replace each input/output/port with two new ports, one carrying the
defined values (named <portname>_d) and one carrying the mask of which
bits are x (named <portname>_x). When a bit in the <portname>_x is set
the corresponding bit in <portname>_d is ignored for inputs and
guaranteed to be 0 for outputs.

-split-public

Replace each public non-port wire with two new wires, one carrying the
defined values (named <wirename>_d) and one carrying the mask of which
bits are x (named <wirename>_x). When a bit in the <portname>_x is set
the corresponding bit in <wirename>_d is guaranteed to be 0 for
outputs.

-assume-encoding

Add encoding invariants as assumptions. This can speed up formal
verification tasks.

-assert-encoding

Add encoding invariants as assertions. Used for testing the xprop
pass itself.

-assume-def-inputs

Assume all inputs are fully defined. This adds corresponding
assumptions to the design and uses these assumptions to optimize the
xprop encoding.

-required

Produce a runtime error if any encountered cell could not be encoded.

-formal

Produce a runtime error if any encoded cell uses a signal that is

neither known to be non-x nor driven by another encoded cell.

-debug-asserts

Add assertions checking that the encoding used by this pass never
produces x values within the encoded signals.