Less-conservative four-valued semantics for a multiplexor (mux).

We have two possible semantics for modeling muxes:

`(4v-ite c a b)`is a less-conservative semantics, whereas`(4v-ite* c a b)`is a more-conservative version.

In both versions, C is the selector, and A/B are data inputs. The mux we are modeling would typically be drawn as:

A B | | ___|_____|___ \ / C ---\ / \_______/ | | Out

Both versions agree exactly in most cases:

- When all of these inputs are Boolean, we simply return A or B depending on the value of C.
- When C is Boolean but the selected value is X or Z, we do not know what the mux will produce so we return X; see 4v-unfloat for an explanation of the Z case.
- When C is X or Z, it is sometimes clear that we must output X. For instance, suppose A = T while B = F. Then, since we do not know which value will be selected, we can only say that the output is X.

The trickiest case, and the one where

- C is X or Z, and
- A and B share some Boolean value.

In this case,

4v-ite* (more conservatively) produces an X, whereas4v-ite (less conservatively) produces the value shared by A and B.

It might be that the

But unless there is some special reason that

Some mux implementations, specifically those based on pass transistors, may
not produce a good value on their output when the select is undriven. The
**totally wrong** for such muxes.

The

Of course, gate-based mux implementations do not have this problem. If a
mux is implemented along the lines of

BOZO what about if C is Z? Are the less-conservative semantics okay in this case, even for a gate-based mux? This could be iffy.

The

With a

But with a

In other words,

**Function: **

(defun 4v-ite (c a b) (declare (xargs :guard t)) (mbe :logic (4vcases c (t (4v-unfloat a)) (f (4v-unfloat b)) (& (4vcases (4v-iff a b) (t a) (& (4vx))))) :exec (cond ((eq c (4vt)) (if (or (eq a (4vt)) (eq a (4vf))) a (4vx))) ((eq c (4vf)) (if (or (eq b (4vt)) (eq b (4vf))) b (4vx))) (t (4vcases (4v-iff a b) (t a) (& (4vx)))))))

**Function: **

(defun 4v-ite* (c a b) (declare (xargs :guard t)) (mbe :logic (4vcases c (t (4v-unfloat a)) (f (4v-unfloat b)) (& (4vx))) :exec (cond ((eq c (4vt)) (if (or (eq a (4vt)) (eq a (4vf))) a (4vx))) ((eq c (4vf)) (if (or (eq b (4vt)) (eq b (4vf))) b (4vx))) (t (4vx)))))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite-3 (implies (4v-equiv b b-equiv) (equal (4v-ite c a b) (4v-ite c a b-equiv))) :rule-classes (:congruence))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite-2 (implies (4v-equiv a a-equiv) (equal (4v-ite c a b) (4v-ite c a-equiv b))) :rule-classes (:congruence))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite-1 (implies (4v-equiv c c-equiv) (equal (4v-ite c a b) (4v-ite c-equiv a b))) :rule-classes (:congruence))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite*-3 (implies (4v-equiv b b-equiv) (equal (4v-ite* c a b) (4v-ite* c a b-equiv))) :rule-classes (:congruence))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite*-2 (implies (4v-equiv a a-equiv) (equal (4v-ite* c a b) (4v-ite* c a-equiv b))) :rule-classes (:congruence))

**Theorem: **

(defthm 4v-equiv-implies-equal-4v-ite*-1 (implies (4v-equiv c c-equiv) (equal (4v-ite* c a b) (4v-ite* c-equiv a b))) :rule-classes (:congruence))