		Search-engine friendly clone of the ACL2 documentation.

Adding-z-drivers

Vl-make-z-occ

Generate an instance of ACL2::*esim-z* to drive an otherwise-undriven output bit.

Definitions and Theorems

Function: vl-make-z-occ

(defun vl-make-z-occ (name out)
       (declare (xargs :guard (and (vl-emodwire-p out) name)))
       (list :u name
             :op acl2::*esim-z*
             :i nil
             :o (list (list out))))

Theorem: good-esim-occp-of-vl-make-z-occ

(defthm good-esim-occp-of-vl-make-z-occ
        (implies (and (force (vl-emodwire-p out))
                      (force name))
                 (good-esim-occp (vl-make-z-occ name out))))