Four-valued semantics for a pullup resistor.
(4v-pullup a) acts just like a buffer except that, if its input is floating, it instead produces true. That is, it returns the value specified by the following truth table:
a | out -----+------- F | F T | T X | X Z | T
(defun 4v-pullup (a) (declare (xargs :guard t)) (4vcases a (t (4vt)) (z (4vt)) (f (4vf)) (& (4vx))))
(defthm 4v-equiv-implies-equal-4v-pullup-1 (implies (4v-equiv a a-equiv) (equal (4v-pullup a) (4v-pullup a-equiv))) :rule-classes (:congruence))