		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-replicated-instnames

Generate the new names that we'll use for replicated instances.

Signature
(vl-replicated-instnames instname instrange nf ctx warnings) → (mv warnings names nf)
Arguments: instname — Name of the instance array we are replicating.
Guard (maybe-stringp instname).; instrange — Its associated range.
Guard (vl-range-p instrange).; nf — For generating fresh names.
Guard (vl-namefactory-p nf).; ctx — Context for warnings.
Guard (vl-modelement-p ctx).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; names — The names to be used for the new instances.
Type (string-listp names).; nf — Type (vl-namefactory-p nf).

This function is responsible for naming the new gate or module instances that are going to be created when we split up an instance array. We really want these new names to correspond to the original instance name and the instance numbers, since otherwise it can be hard to understand the relationship of the transformed module's state to the original module.

Suppose we are transforming an instance like this:

type foo [N:0] (arg1, arg2, ..., argM);

We produce a list of N+1 names that are to be used as the instance names for the split up arguments. We try to use names of the form instname_index if they are available, e.g., for the above we would generate names like foo_N, ..., foo_0.

We want to return the names so that the name corresponding to the most significant bits comes first. If the range is like [N:0], then we return foo_N, ..., foo_0. If the range goes the other way, i.e., [0:N], then we return foo_0, ..., foo_N.

Definitions and Theorems

Function: vl-replicated-instnames

(defun vl-replicated-instnames (instname instrange nf ctx warnings)
 (declare (xargs :guard (and (maybe-stringp instname)
                             (vl-range-p instrange)
                             (vl-namefactory-p nf)
                             (vl-modelement-p ctx)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (vl-range-resolved-p instrange)))
 (let ((__function__ 'vl-replicated-instnames))
  (declare (ignorable __function__))
  (b* ((instname (maybe-string-fix instname))
       (ctx (vl-modelement-fix ctx))
       (left (vl-resolved->val (vl-range->msb instrange)))
       (right (vl-resolved->val (vl-range->lsb instrange)))
       (low (min left right))
       (high (max left right))
       (instname (or instname "unnamed"))
       (names-low-to-high
            (vl-preferred-replicate-names low high instname))
       (names-msb-first (if (>= left right)
                            (reverse names-low-to-high)
                          names-low-to-high))
       ((mv fresh nf)
        (vl-namefactory-plain-names names-msb-first nf))
       ((when (equal names-msb-first fresh))
        (mv (ok) names-msb-first nf))
       ((mv fresh nf)
        (vl-bad-replicate-names (+ 1 (- high low))
                                (cat "vl_badname_" instname)
                                nf)))
   (mv
    (warn
     :type :vl-warn-replicate-name
     :msg
     "~a0: preferred names for instance array ~s1 are not ~
                    available, so using lousy vl_badname_* naming scheme ~
                    instead.  This conflict is caused by ~&2."
     :args (list ctx instname
                 (difference (mergesort names-msb-first)
                             (mergesort fresh))))
    (rev fresh)
    nf))))

Theorem: vl-warninglist-p-of-vl-replicated-instnames.warnings

(defthm vl-warninglist-p-of-vl-replicated-instnames.warnings
  (b*
    (((mv ?warnings ?names ?nf)
      (vl-replicated-instnames instname instrange nf ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-replicated-instnames.names

(defthm string-listp-of-vl-replicated-instnames.names
  (b*
    (((mv ?warnings ?names ?nf)
      (vl-replicated-instnames instname instrange nf ctx warnings)))
    (string-listp names))
  :rule-classes :rewrite)

Theorem: vl-namefactory-p-of-vl-replicated-instnames.nf

(defthm vl-namefactory-p-of-vl-replicated-instnames.nf
  (b*
    (((mv ?warnings ?names ?nf)
      (vl-replicated-instnames instname instrange nf ctx warnings)))
    (vl-namefactory-p nf))
  :rule-classes :rewrite)

Theorem: len-of-vl-replicated-instnames

(defthm len-of-vl-replicated-instnames
 (implies
  (and (force (vl-range-resolved-p instrange))
       (force (vl-namefactory-p nf)))
  (equal
   (len
    (mv-nth
      1
      (vl-replicated-instnames instname instrange nf ctx warnings)))
   (vl-range-size instrange))))

Theorem: vl-replicated-instnames-of-maybe-string-fix-instname

(defthm vl-replicated-instnames-of-maybe-string-fix-instname
 (equal
      (vl-replicated-instnames (maybe-string-fix instname)
                               instrange nf ctx warnings)
      (vl-replicated-instnames instname instrange nf ctx warnings)))

Theorem: vl-replicated-instnames-maybe-string-equiv-congruence-on-instname

(defthm
  vl-replicated-instnames-maybe-string-equiv-congruence-on-instname
 (implies
   (maybe-string-equiv instname instname-equiv)
   (equal
        (vl-replicated-instnames instname instrange nf ctx warnings)
        (vl-replicated-instnames instname-equiv
                                 instrange nf ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-replicated-instnames-of-vl-range-fix-instrange

(defthm vl-replicated-instnames-of-vl-range-fix-instrange
 (equal
      (vl-replicated-instnames instname (vl-range-fix instrange)
                               nf ctx warnings)
      (vl-replicated-instnames instname instrange nf ctx warnings)))

Theorem: vl-replicated-instnames-vl-range-equiv-congruence-on-instrange

(defthm
     vl-replicated-instnames-vl-range-equiv-congruence-on-instrange
 (implies
   (vl-range-equiv instrange instrange-equiv)
   (equal
        (vl-replicated-instnames instname instrange nf ctx warnings)
        (vl-replicated-instnames instname
                                 instrange-equiv nf ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-replicated-instnames-of-vl-namefactory-fix-nf

(defthm vl-replicated-instnames-of-vl-namefactory-fix-nf
 (equal
      (vl-replicated-instnames instname
                               instrange (vl-namefactory-fix nf)
                               ctx warnings)
      (vl-replicated-instnames instname instrange nf ctx warnings)))

Theorem: vl-replicated-instnames-vl-namefactory-equiv-congruence-on-nf

(defthm
      vl-replicated-instnames-vl-namefactory-equiv-congruence-on-nf
 (implies
   (vl-namefactory-equiv nf nf-equiv)
   (equal
        (vl-replicated-instnames instname instrange nf ctx warnings)
        (vl-replicated-instnames instname
                                 instrange nf-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-replicated-instnames-of-vl-modelement-fix-ctx

(defthm vl-replicated-instnames-of-vl-modelement-fix-ctx
 (equal
      (vl-replicated-instnames instname
                               instrange nf (vl-modelement-fix ctx)
                               warnings)
      (vl-replicated-instnames instname instrange nf ctx warnings)))

Theorem: vl-replicated-instnames-vl-modelement-equiv-congruence-on-ctx

(defthm
      vl-replicated-instnames-vl-modelement-equiv-congruence-on-ctx
 (implies
   (vl-modelement-equiv ctx ctx-equiv)
   (equal
        (vl-replicated-instnames instname instrange nf ctx warnings)
        (vl-replicated-instnames instname
                                 instrange nf ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-replicated-instnames-of-vl-warninglist-fix-warnings

(defthm vl-replicated-instnames-of-vl-warninglist-fix-warnings
 (equal
      (vl-replicated-instnames instname instrange
                               nf ctx (vl-warninglist-fix warnings))
      (vl-replicated-instnames instname instrange nf ctx warnings)))

Theorem: vl-replicated-instnames-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-replicated-instnames-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal
        (vl-replicated-instnames instname instrange nf ctx warnings)
        (vl-replicated-instnames instname
                                 instrange nf ctx warnings-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-bad-replicate-names: Fallback names in case our preferred names aren't available. Only called if there is a name conflict that prevents us from using good names.
Vl-preferred-replicate-names: Preferred names from low to high, inclusive, e.g., (foo_3 foo_4 foo_5)