		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-tristate

Four-valued semantics for tri-state buffers.

This is our model of a simple tri-state buffer:

        A
        |
     ___|___
     \     /
C ----\   /
       \ /
        V
        |
       Out

(4v-tristate c a) returns:

A when its inputs are Boolean and C is T, or
Z when C is known to be false, or
X otherwise.

This exactly matches the Verilog semantics for:

wire c = sel ? a : 1'bz;

Such buffers are typically used to model muxes with multiple selectors. See also 4v-res.

Definitions and Theorems

Function: 4v-tristate

(defun 4v-tristate (c a)
       (declare (xargs :guard t))
       (mbe :logic (4vcases c (t (4v-unfloat a))
                            (f (4vz))
                            (& (4vx)))
            :exec (cond ((eq c (4vf)) (4vz))
                        ((and (eq c (4vt))
                              (or (eq a (4vt)) (eq a (4vf))))
                         a)
                        (t (4vx)))))

Theorem: 4v-equiv-implies-equal-4v-tristate-2

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

Theorem: 4v-equiv-implies-equal-4v-tristate-1

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