		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-z-gateinst-p

Signature
(vl-lucid-z-gateinst-p x) → *
Arguments: x — Guard (vl-gateinst-p x).

Definitions and Theorems

Function: vl-lucid-z-gateinst-p

(defun vl-lucid-z-gateinst-p (x)
  (declare (xargs :guard (vl-gateinst-p x)))
  (let ((__function__ 'vl-lucid-z-gateinst-p))
    (declare (ignorable __function__))
    (b* (((vl-gateinst x) x))
      (member x.type
              '(:vl-cmos :vl-rcmos
                         :vl-bufif0 :vl-bufif1
                         :vl-notif0 :vl-notif1
                         :vl-nmos :vl-pmos
                         :vl-rnmos :vl-rpmos
                         :vl-tranif0 :vl-tranif1
                         :vl-rtranif1 :vl-rtranif0
                         :vl-tran :vl-rtran
                         :vl-pulldown :vl-pullup)))))

Theorem: vl-lucid-z-gateinst-p-of-vl-gateinst-fix-x

(defthm vl-lucid-z-gateinst-p-of-vl-gateinst-fix-x
  (equal (vl-lucid-z-gateinst-p (vl-gateinst-fix x))
         (vl-lucid-z-gateinst-p x)))

Theorem: vl-lucid-z-gateinst-p-vl-gateinst-equiv-congruence-on-x

(defthm vl-lucid-z-gateinst-p-vl-gateinst-equiv-congruence-on-x
  (implies (vl-gateinst-equiv x x-equiv)
           (equal (vl-lucid-z-gateinst-p x)
                  (vl-lucid-z-gateinst-p x-equiv)))
  :rule-classes :congruence)