		Search-engine friendly clone of the ACL2 documentation.

Adding-z-drivers

Vl-make-z-occs

Generate instances of ACL2::*esim-z* to drive undriven output bits.

Signature: (vl-make-z-occs idx outs) returns a list of occurrences.

idx is a name index used for fresh name generation. We expect that it is initially set to the highest index of any emodwire in the module whose basename is vl_zdrive. We increment it whenever we need to create a new, fresh occurrence name.
outs are an vl-emodwirelist-p that should include all of the output bits that weren't driven by the preliminary occurrences.

Definitions and Theorems

Function: vl-make-z-occs

(defun vl-make-z-occs (idx outs)
  (declare (xargs :guard (and (natp idx)
                              (vl-emodwirelist-p outs))))
  (b* (((when (atom outs)) nil)
       (idx (+ 1 idx))
       (fresh (make-vl-emodwire :basename "vl_zdrive"
                                :index idx)))
    (cons (vl-make-z-occ fresh (car outs))
          (vl-make-z-occs idx (cdr outs)))))

Theorem: good-esim-occsp-of-vl-make-z-occs

(defthm good-esim-occsp-of-vl-make-z-occs
  (implies (and (force (natp idx))
                (force (vl-emodwirelist-p outs)))
           (good-esim-occsp (vl-make-z-occs idx outs))))