		Search-engine friendly clone of the ACL2 documentation.

Argument-partitioning

Vl-assemble-gateinsts

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

Signature
(vl-assemble-gateinsts names args idx idxincr type strength delay atts loc) → gates
Arguments: names — Names to give to the new gate instances.
Guard (string-listp names).; args — The arguments for each instance, already reoriented; see vl-partition-plainarglist and vl-reorient-partitioned-args.
Guard (vl-plainarglistlist-p args).; idx — Current index, used only for annotations.
Guard (integerp idx).; idxincr — How to compute the next index, typically +/-1 depending on whether this is an MSB-first or LSB-first range.
Guard (integerp idxincr).; type — Guard (vl-gatetype-p type).; strength — Guard (vl-maybe-gatestrength-p strength).; delay — Guard (vl-maybe-gatedelay-p delay).; atts — Guard (vl-atts-p atts).; loc — Guard (vl-location-p loc).
Returns: gates — Type (vl-gateinstlist-p gates).

Definitions and Theorems

Function: vl-assemble-gateinsts

(defun vl-assemble-gateinsts
       (names args idx
              idxincr type strength delay atts loc)
  (declare (xargs :guard (and (string-listp names)
                              (vl-plainarglistlist-p args)
                              (integerp idx)
                              (integerp idxincr)
                              (vl-gatetype-p type)
                              (vl-maybe-gatestrength-p strength)
                              (vl-maybe-gatedelay-p delay)
                              (vl-atts-p atts)
                              (vl-location-p loc))))
  (declare (xargs :guard (same-lengthp names args)))
  (let ((__function__ 'vl-assemble-gateinsts))
    (declare (ignorable __function__))
    (if (atom args)
        nil
      (cons (make-vl-gateinst :type type
                              :name (car names)
                              :range nil
                              :strength strength
                              :delay delay
                              :args (car args)
                              :atts (cons (cons "VL_REPLICATE_INDEX"
                                                (vl-make-index idx))
                                          atts)
                              :loc loc)
            (vl-assemble-gateinsts (cdr names)
                                   (cdr args)
                                   (+ idx idxincr)
                                   idxincr
                                   type strength delay atts loc)))))

Theorem: vl-gateinstlist-p-of-vl-assemble-gateinsts

(defthm vl-gateinstlist-p-of-vl-assemble-gateinsts
 (b*
  ((gates
      (vl-assemble-gateinsts names args idx
                             idxincr type strength delay atts loc)))
  (vl-gateinstlist-p gates))
 :rule-classes :rewrite)