		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-make-ordinary-implicit-wires

Generate net declarations for one-bit implicit wires.

Signature
(vl-make-ordinary-implicit-wires loc names) → nets
Arguments: loc — Guard (vl-location-p loc).; names — Guard (string-listp names).
Returns: nets — Type (vl-vardecllist-p nets).

We are given x, a string list that should initially contain the names of some implicit wires that we are supposed to introduce, and loc, a vl-location-p that should be the minloc for the module. We produce a list of one-bit vl-vardecl-ps, one for each name in x.

Definitions and Theorems

Function: vl-make-ordinary-implicit-wires

(defun vl-make-ordinary-implicit-wires (loc names)
 (declare (xargs :guard (and (vl-location-p loc)
                             (string-listp names))))
 (let ((__function__ 'vl-make-ordinary-implicit-wires))
   (declare (ignorable __function__))
   (if (consp names)
       (cons (make-vl-vardecl :name (car names)
                              :type *vl-plain-old-wire-type*
                              :nettype :vl-wire
                              :loc loc
                              :atts (list (cons "VL_IMPLICIT" nil)))
             (vl-make-ordinary-implicit-wires loc (cdr names)))
     nil)))

Theorem: vl-vardecllist-p-of-vl-make-ordinary-implicit-wires

(defthm vl-vardecllist-p-of-vl-make-ordinary-implicit-wires
  (b* ((nets (vl-make-ordinary-implicit-wires loc names)))
    (vl-vardecllist-p nets))
  :rule-classes :rewrite)

Theorem: vl-vardecllist->names-of-vl-make-ordinary-implicit-wires

(defthm vl-vardecllist->names-of-vl-make-ordinary-implicit-wires
  (equal (vl-vardecllist->names
              (vl-make-ordinary-implicit-wires loc names))
         (string-list-fix names)))

Theorem: vl-make-ordinary-implicit-wires-of-vl-location-fix-loc

(defthm vl-make-ordinary-implicit-wires-of-vl-location-fix-loc
  (equal (vl-make-ordinary-implicit-wires (vl-location-fix loc)
                                          names)
         (vl-make-ordinary-implicit-wires loc names)))

Theorem: vl-make-ordinary-implicit-wires-vl-location-equiv-congruence-on-loc

(defthm
 vl-make-ordinary-implicit-wires-vl-location-equiv-congruence-on-loc
 (implies (vl-location-equiv loc loc-equiv)
          (equal (vl-make-ordinary-implicit-wires loc names)
                 (vl-make-ordinary-implicit-wires loc-equiv names)))
 :rule-classes :congruence)

Theorem: vl-make-ordinary-implicit-wires-of-string-list-fix-names

(defthm vl-make-ordinary-implicit-wires-of-string-list-fix-names
  (equal
       (vl-make-ordinary-implicit-wires loc (string-list-fix names))
       (vl-make-ordinary-implicit-wires loc names)))

Theorem: vl-make-ordinary-implicit-wires-string-list-equiv-congruence-on-names

(defthm
 vl-make-ordinary-implicit-wires-string-list-equiv-congruence-on-names
 (implies (str::string-list-equiv names names-equiv)
          (equal (vl-make-ordinary-implicit-wires loc names)
                 (vl-make-ordinary-implicit-wires loc names-equiv)))
 :rule-classes :congruence)