		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-replicate-modinst

Convert a module instance into a list of simpler instances, if necessary.

Signature
(vl-replicate-modinst x nf ss warnings) → (mv warnings new-modinsts nf)
Arguments: x — A module instance, perhaps an instance array.
Guard (vl-modinst-p x).; nf — For generating fresh names.
Guard (vl-namefactory-p nf).; ss — Guard (vl-scopestack-p ss).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-modinsts — Replacements for x.
Type (vl-modinstlist-p new-modinsts), given the guard.; nf — Type (vl-namefactory-p nf), given the guard.

If x has a range, i.e., it is an array of module instances, then we try to split it into a list of nil-ranged, simple instances. If x is a regular (non-array) instance, we just keep it.

Definitions and Theorems

Function: vl-replicate-modinst

(defun vl-replicate-modinst (x nf ss warnings)
 (declare (xargs :guard (and (vl-modinst-p x)
                             (vl-namefactory-p nf)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-replicate-modinst))
  (declare (ignorable __function__))
  (b*
   (((vl-modinst x) x)
    ((unless x.range) (mv (ok) (list x) nf))
    ((unless (vl-range-resolved-p x.range))
     (mv
       (fatal :type :vl-bad-instance
              :msg "~a0: instance array with unresolved range: ~a1."
              :args (list x x.range))
       (list x)
       nf))
    ((unless (vl-paramargs-empty-p x.paramargs))
     (mv
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: instance array still has parameters?  This ~
                         should have been taken care of during ~
                         unparameterization."
       :args (list x))
      (list x)
      nf))
    (x.atts (cons (list "VL_FROM_INST_ARRAY")
                  x.atts))
    (size (vl-range-size x.range))
    (target (vl-scopestack-find-definition x.modname ss))
    ((unless (and target (eq (tag target) :vl-module)))
     (mv (fatal :type :vl-bad-instance
                :msg "~a0: instance of undefined module ~m1."
                :args (list x x.modname))
         (list x)
         nf))
    ((mv successp warnings port-widths)
     (vl-module-port-widths (vl-module->ports target)
                            x warnings))
    ((unless successp)
     (mv warnings (list x) nf))
    ((mv successp warnings new-args)
     (vl-replicate-arguments x.portargs
                             port-widths size ss x warnings))
    ((unless successp)
     (mv warnings (list x) nf))
    ((mv warnings names nf)
     (vl-replicated-instnames x.instname x.range nf x warnings))
    (new-atts
        (if x.instname
            (cons (cons "VL_REPLICATE_ORIGNAME"
                        (make-vl-atom :guts (vl-string x.instname)))
                  x.atts)
          x.atts))
    (left-idx (vl-resolved->val (vl-range->msb x.range)))
    (right-idx (vl-resolved->val (vl-range->lsb x.range)))
    (idx-incr (if (>= left-idx right-idx) -1 1))
    (new-modinsts
         (vl-assemble-modinsts names new-args
                               left-idx idx-incr x.modname x.str
                               x.delay x.paramargs new-atts x.loc)))
   (mv warnings new-modinsts nf))))

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

(defthm vl-warninglist-p-of-vl-replicate-modinst.warnings
  (b* (((mv ?warnings ?new-modinsts ?nf)
        (vl-replicate-modinst x nf ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-modinstlist-p-of-vl-replicate-modinst.new-modinsts

(defthm vl-modinstlist-p-of-vl-replicate-modinst.new-modinsts
  (implies (and (force (vl-modinst-p x))
                (force (vl-namefactory-p nf))
                (force (vl-scopestack-p ss))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?new-modinsts ?nf)
                 (vl-replicate-modinst x nf ss warnings)))
             (vl-modinstlist-p new-modinsts)))
  :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-replicate-modinst.nf

(defthm vl-namefactory-p-of-vl-replicate-modinst.nf
  (implies (and (force (vl-modinst-p x))
                (force (vl-namefactory-p nf))
                (force (vl-scopestack-p ss))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?new-modinsts ?nf)
                 (vl-replicate-modinst x nf ss warnings)))
             (vl-namefactory-p nf)))
  :rule-classes :rewrite)

Theorem: vl-replicate-modinst-mvtypes-1

(defthm vl-replicate-modinst-mvtypes-1
  (true-listp (mv-nth 1
                      (vl-replicate-modinst x nf ss warnings)))
  :rule-classes :type-prescription)