		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-unfloat

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 in is Z, the behavior of these transistors can't be accurately predicted. Hence, we should treat a Z as if it were an X. The situation for other kinds of ordinary logic gates (ands, ors, xors) is similar. So, when we define operations like 4v-not and 4v-and that are intended to model gates, we generally apply 4v-unfloat to the inputs so that any Z values are treated as X.

Definitions and Theorems

Function: 4v-unfloat$inline

(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: 4v-unfloat-truth-table

(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: 4v-equiv-implies-equal-4v-unfloat-1

(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))