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.
(defun 4v-xdet$inline (a) (declare (xargs :guard t)) (4vcases a (t (4vf)) (f (4vf)) (& (4vx))))
(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)
(defthm 4v-equiv-implies-equal-4v-xdet-1 (implies (4v-equiv a a-equiv) (equal (4v-xdet a) (4v-xdet a-equiv))) :rule-classes (:congruence))