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