Converts floating (undriven) values to X.
(4v-unfloat a) is a helper routine that is used in the definitions of many other 4v-operations. It just coerces Z values into X, while leaving any other 4-valued logic constants alone.
What is this function for? Z values have a special role in a few specific operations, like 4v-res, 4v-pullup, and 4v-tristate. But most of the time, e.g., in 4v-not, 4v-and, etc., a Z value on an input should just be regarded as an X.
To see why, let us consider a simple inverter.
power | ___| || +-----o|| | ||___ | | in ------+ +--------- out | ___| | || +------|| ||___ | | ground
When
Function:
(defun 4v-unfloat$inline (a) (declare (xargs :guard t)) (mbe :logic (4vcases a (z (4vx)) (& (4v-fix a))) :exec (if (or (eq a (4vt)) (eq a (4vf))) a (4vx))))
Theorem:
(defthm 4v-unfloat-truth-table (and (equal (4v-unfloat (4vt)) (4vt)) (equal (4v-unfloat (4vf)) (4vf)) (equal (4v-unfloat (4vx)) (4vx)) (equal (4v-unfloat (4vz)) (4vx))) :rule-classes nil)
Theorem:
(defthm 4v-equiv-implies-equal-4v-unfloat-1 (implies (4v-equiv a a-equiv) (equal (4v-unfloat a) (4v-unfloat a-equiv))) :rule-classes (:congruence))