		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-zif

Unusual semantics for a multiplexor, used mainly to implement composition features in esim

A ZIF module is in some ways similar to a pass-gate based multiplexor, but is probably not the sort of thing you would actually want to use to model a mux. It is very similar to an 4v-ite* but does not 4v-unfloat its inputs. We include this mainly as a way to implement experimental composition features in esim.

Definitions and Theorems

Function: 4v-zif

(defun 4v-zif (c a b)
  (declare (xargs :guard t))
  (mbe :logic (4vcases c (t (4v-fix a))
                       (f (4v-fix b))
                       (& (4vx)))
       :exec (cond ((eq c (4vt)) (4v-fix a))
                   ((eq c (4vf)) (4v-fix b))
                   (t (4vx)))))

Theorem: 4v-equiv-implies-equal-4v-zif-3

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

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

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

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

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