4v-ite
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
Semantics
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 4v-ite and 4v-ite* differ,
is when:
- C is X or Z, and
- A and B share some Boolean value.
In this case,
- 4v-ite* (more conservatively) produces an X, whereas
- 4v-ite (less conservatively) produces the value shared by A and
B.
Comparison
It might be that the 4v-ite behavior is necessary when analyzing some
circuits. But we do not think this should be the case very frequently, and we
think you really should probably not design circuits this way.
But unless there is some special reason that 4v-ite is needed, we think
4v-ite* is usually the better way to go. There are two reasons for
this:
1. Modeling considerations
Some mux implementations, specifically those based on pass transistors, may
not produce a good value on their output when the select is undriven. The
4v-ite semantics are totally wrong for such muxes.
The 4v-ite* semantics are safer, but do not entirely address the
problem because, when the select is undriven, such circuits can have "backward
flow" where their output drives the input. We have no way to model this.
Of course, gate-based mux implementations do not have this problem. If a
mux is implemented along the lines of (C & A) | (~C & B), then any Boolean
value of C will give us the shared answer as 4v-ite produces, so either
implementation is probably okay.
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.
2. Symbolic simulation performance.
The 4v-ite* semantics may permit faster symbolic simulations. In
particular, suppose we are interested in analyzing a small part of a large
circuit, and we have set many signals we think are irrelevant to X.
Furthermore, suppose one of these Xed out signals is C, i.e., it is being used
as the select for some mux.
With a 4v-ite mux, the resulting expression for the output wire will be
some function that involves checking whether the expressions for A and B have
the same value. This resulting expression will contain the expressions for A
and B, so if these input expressions are large, the resulting expression will
be large.
But with a 4v-ite* mux, regardless of the expressions on A and B the
result is simply the constant function X.
In other words, 4v-ite* based muxes have a very nice property: if the
select is X, the output expression is just X and all of the presumably
irrelevant logic driving the mux is discarded, whereas 4v-ite muxes don't
get to carry out this kind of optimization.
Definitions and Theorems
Function: 4v-ite
(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: 4v-ite*
(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: 4v-equiv-implies-equal-4v-ite-3
(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: 4v-equiv-implies-equal-4v-ite-2
(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: 4v-equiv-implies-equal-4v-ite-1
(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: 4v-equiv-implies-equal-4v-ite*-3
(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: 4v-equiv-implies-equal-4v-ite*-2
(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: 4v-equiv-implies-equal-4v-ite*-1
(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))
