		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-replicate-arguments

Partition arguments for a module instance

Signature
(vl-replicate-arguments args port-widths insts ss elem warnings) → (mv successp warnings arg-lists)
Arguments: args — Arguments to a module instance. Should already be resolved, i.e. should be plainargs, and sized.
Guard (vl-arguments-p args).; port-widths — Widths of the corresponding ports.
Guard (pos-listp port-widths).; insts — Number of instances we're splitting these args into.
Guard (posp insts).; ss — Guard (vl-scopestack-p ss).; elem — Context for warnings.
Guard (vl-modelement-p elem).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; arg-lists — The new arguments to give to each (split up) module instance.
Type (and (vl-argumentlist-p arg-lists) (implies (and successp (equal len (pos-fix insts))) (equal (len arg-lists) len))) .

Definitions and Theorems

Function: vl-replicate-arguments

(defun vl-replicate-arguments
       (args port-widths insts ss elem warnings)
 (declare (xargs :guard (and (vl-arguments-p args)
                             (pos-listp port-widths)
                             (posp insts)
                             (vl-scopestack-p ss)
                             (vl-modelement-p elem)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-replicate-arguments))
  (declare (ignorable __function__))
  (b*
   ((insts (pos-fix insts))
    ((when (eq (vl-arguments-kind args)
               :vl-arguments-named))
     (mv
      nil
      (fatal
       :type :vl-bad-arguments
       :msg
       "~a0: Expected only plain argument lists, but found ~
                         named args instead."
       :args (list elem))
      nil))
    (actuals (vl-arguments-plain->args args))
    ((unless (same-lengthp actuals port-widths))
     (mv nil
         (fatal :type :vl-bad-arguments
                :msg "~a0: Expected ~x1 arguments but found ~x2."
                :args (list elem (len port-widths)
                            (len actuals)))
         nil))
    ((mv successp warnings slices)
     (vl-partition-plainarglist actuals
                                port-widths insts ss elem warnings))
    ((unless successp)
     (mv nil warnings nil))
    (transpose (vl-reorient-partitioned-args slices insts))
    (arg-lists (vl-plainarglists-to-arguments transpose)))
   (mv t (ok) arg-lists))))

Theorem: booleanp-of-vl-replicate-arguments.successp

(defthm booleanp-of-vl-replicate-arguments.successp
 (b* (((mv ?successp ?warnings ?arg-lists)
       (vl-replicate-arguments args
                               port-widths insts ss elem warnings)))
   (booleanp successp))
 :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-replicate-arguments.warnings

(defthm vl-warninglist-p-of-vl-replicate-arguments.warnings
 (b* (((mv ?successp ?warnings ?arg-lists)
       (vl-replicate-arguments args
                               port-widths insts ss elem warnings)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-replicate-arguments.arg-lists

(defthm return-type-of-vl-replicate-arguments.arg-lists
 (b* (((mv ?successp ?warnings ?arg-lists)
       (vl-replicate-arguments args
                               port-widths insts ss elem warnings)))
   (and (vl-argumentlist-p arg-lists)
        (implies (and successp (equal len (pos-fix insts)))
                 (equal (len arg-lists) len))))
 :rule-classes :rewrite)