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.
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.
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.
Add encoding invariants as assumptions. This can speed up formal verification tasks.
Add encoding invariants as assertions. Used for testing the xprop pass itself.
Assume all inputs are fully defined. This adds corresponding assumptions to the design and uses these assumptions to optimize the xprop encoding.
Produce a runtime error if any encountered cell could not be encoded.
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.
Add assertions checking that the encoding used by this pass never produces x values within the encoded signals.