		Search-engine friendly clone of the ACL2 documentation.

Esim-primitives

esim-cmos

Primitive E module for a kind of cmos gate.

We use this to implement vl2014::*vl-1-bit-cmos*.

Definition:

Definition: *esim-cmos*

(defconst *esim-cmos*
  '(:n *esim-cmos*
       :x (:out ((|out| res (zif |nctrl| |data| (z))
                        (zif |pctrl| (z) |data|))))
       :i ((|data|) (|nctrl|) (|pctrl|))
       :o ((|out|))))