X-detection or identity circuit.
(4v-xdet a) returns the value specified by the following truth table:
a | out -----+------- T | F F | F X | X Z | X -----+-------
This is a special operation that does not correspond to any sort of hardware circuit, but that is useful for efficiently implementing the x-detection semantics of Verilog's vector arithmetic operations.
(defthm 4v-xdet-truth-table (and (equal (4v-xdet (4vt)) (4vf)) (equal (4v-xdet (4vf)) (4vf)) (equal (4v-xdet (4vx)) (4vx)) (equal (4v-xdet (4vz)) (4vx))) :rule-classes nil)