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