		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-make-initial-wireinfo-alist

Create an initial wireinfo alist by we associating each wire with a new vl-wireinfo entry.

Signature
(vl-make-initial-wireinfo-alist x) → alist
Arguments: x — Names of all wires declared in a module.
Guard (string-listp x).
Returns: alist — Type (vl-wireinfo-alistp alist), given the guard.

Definitions and Theorems

Function: vl-make-initial-wireinfo-alist

(defun vl-make-initial-wireinfo-alist (x)
  (declare (xargs :guard (string-listp x)))
  (let ((__function__ 'vl-make-initial-wireinfo-alist))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (hons-acons (car x)
                  (make-vl-wireinfo :usedp nil :setp nil)
                  (vl-make-initial-wireinfo-alist (cdr x))))))

Theorem: vl-wireinfo-alistp-of-vl-make-initial-wireinfo-alist

(defthm vl-wireinfo-alistp-of-vl-make-initial-wireinfo-alist
  (implies (and (force (string-listp x)))
           (b* ((alist (vl-make-initial-wireinfo-alist x)))
             (vl-wireinfo-alistp alist)))
  :rule-classes :rewrite)