		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-assemble-modinsts

Build vl-modinst-p's from the sliced-up arguments.

Signature
(vl-assemble-modinsts names args idx idxincr modname str delay paramargs atts loc) → modinsts
Arguments: names — Names to give to each instance.
Guard (string-listp names).; args — Arguments to use for each instance.
Guard (vl-argumentlist-p args).; idx — Index number, used in attributes.
Guard (integerp idx).; idxincr — Typically +/-1, whether to count up or down.
Guard (integerp idxincr).; modname — Module being instantiated.
Guard (stringp modname).; str — Guard (vl-maybe-gatestrength-p str).; delay — Guard (vl-maybe-gatedelay-p delay).; paramargs — Guard (vl-paramargs-p paramargs).; atts — Guard (vl-atts-p atts).; loc — Guard (vl-location-p loc).
Returns: modinsts — Type (vl-modinstlist-p modinsts).

Definitions and Theorems

Function: vl-assemble-modinsts

(defun vl-assemble-modinsts
       (names args idx idxincr
              modname str delay paramargs atts loc)
  (declare (xargs :guard (and (string-listp names)
                              (vl-argumentlist-p args)
                              (integerp idx)
                              (integerp idxincr)
                              (stringp modname)
                              (vl-maybe-gatestrength-p str)
                              (vl-maybe-gatedelay-p delay)
                              (vl-paramargs-p paramargs)
                              (vl-atts-p atts)
                              (vl-location-p loc))))
  (declare (xargs :guard (same-lengthp names args)))
  (let ((__function__ 'vl-assemble-modinsts))
    (declare (ignorable __function__))
    (if (atom args)
        nil
      (cons (make-vl-modinst :instname (car names)
                             :modname modname
                             :str str
                             :delay delay
                             :atts (cons (cons "VL_REPLICATE_INDEX"
                                               (vl-make-index idx))
                                         atts)
                             :portargs (car args)
                             :paramargs paramargs
                             :loc loc)
            (vl-assemble-modinsts (cdr names)
                                  (cdr args)
                                  (+ idx idxincr)
                                  idxincr modname
                                  str delay paramargs atts loc)))))

Theorem: vl-modinstlist-p-of-vl-assemble-modinsts

(defthm vl-modinstlist-p-of-vl-assemble-modinsts
 (b*
  ((modinsts
       (vl-assemble-modinsts names args idx idxincr
                             modname str delay paramargs atts loc)))
  (vl-modinstlist-p modinsts))
 :rule-classes :rewrite)