		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-replicate-gateinst

Convert a gate array instance into a list of gates (if necessary).

Signature
(vl-replicate-gateinst x nf ss warnings) → (mv warnings new-gateinsts nf)
Arguments: x — Some gate, which may or may not be an instance array.
Guard (vl-gateinst-p x).; nf — For fresh name generation.
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-gateinsts — New gates that will replace x.
Type (vl-gateinstlist-p new-gateinsts).; nf — Type (vl-namefactory-p nf).

If x has a range, i.e., it is an array of gate instances, then we try to split it into a list of nil-ranged, simple gates. The new-gateinsts should replace x in the module.

Definitions and Theorems

Function: vl-replicate-gateinst

(defun vl-replicate-gateinst (x nf ss warnings)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-namefactory-p nf)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-replicate-gateinst))
  (declare (ignorable __function__))
  (b*
   ((x (vl-gateinst-fix x))
    (nf (vl-namefactory-fix nf))
    ((vl-gateinst x) x)
    ((unless x.range) (mv (ok) (list x) nf))
    ((unless (vl-range-resolved-p x.range))
     (mv
      (fatal
       :type :vl-bad-gate
       :msg
       "~a0: expected range of instance array to be ~
                         resolved, but found ~a1."
       :args (list x x.range))
      (list x)
      nf))
    (x.atts (cons (list "VL_FROM_GATE_ARRAY")
                  x.atts))
    (size (vl-range-size x.range))
    (port-widths (replicate (len x.args) 1))
    ((mv successp warnings slices)
     (vl-partition-plainarglist
          x.args port-widths size ss x warnings))
    ((unless successp)
     (mv warnings (list x) nf))
    (transpose (vl-reorient-partitioned-args slices size))
    ((mv warnings names nf)
     (vl-replicated-instnames x.name x.range nf x warnings))
    (new-atts
     (if x.name (cons (cons "VL_REPLICATE_ORIGNAME"
                            (make-vl-atom :guts (vl-string x.name)))
                      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-gates
     (vl-assemble-gateinsts names transpose left-idx idx-incr x.type
                            x.strength x.delay new-atts x.loc)))
   (mv warnings new-gates nf))))

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

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

Theorem: vl-gateinstlist-p-of-vl-replicate-gateinst.new-gateinsts

(defthm vl-gateinstlist-p-of-vl-replicate-gateinst.new-gateinsts
  (b* (((mv ?warnings ?new-gateinsts ?nf)
        (vl-replicate-gateinst x nf ss warnings)))
    (vl-gateinstlist-p new-gateinsts))
  :rule-classes :rewrite)

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

(defthm vl-namefactory-p-of-vl-replicate-gateinst.nf
  (b* (((mv ?warnings ?new-gateinsts ?nf)
        (vl-replicate-gateinst x nf ss warnings)))
    (vl-namefactory-p nf))
  :rule-classes :rewrite)

Theorem: vl-replicate-gateinst-mvtypes-1

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

Theorem: vl-replicate-gateinst-of-vl-gateinst-fix-x

(defthm vl-replicate-gateinst-of-vl-gateinst-fix-x
  (equal (vl-replicate-gateinst (vl-gateinst-fix x)
                                nf ss warnings)
         (vl-replicate-gateinst x nf ss warnings)))

Theorem: vl-replicate-gateinst-vl-gateinst-equiv-congruence-on-x

(defthm vl-replicate-gateinst-vl-gateinst-equiv-congruence-on-x
  (implies (vl-gateinst-equiv x x-equiv)
           (equal (vl-replicate-gateinst x nf ss warnings)
                  (vl-replicate-gateinst x-equiv nf ss warnings)))
  :rule-classes :congruence)

Theorem: vl-replicate-gateinst-of-vl-namefactory-fix-nf

(defthm vl-replicate-gateinst-of-vl-namefactory-fix-nf
  (equal (vl-replicate-gateinst x (vl-namefactory-fix nf)
                                ss warnings)
         (vl-replicate-gateinst x nf ss warnings)))

Theorem: vl-replicate-gateinst-vl-namefactory-equiv-congruence-on-nf

(defthm vl-replicate-gateinst-vl-namefactory-equiv-congruence-on-nf
  (implies (vl-namefactory-equiv nf nf-equiv)
           (equal (vl-replicate-gateinst x nf ss warnings)
                  (vl-replicate-gateinst x nf-equiv ss warnings)))
  :rule-classes :congruence)

Theorem: vl-replicate-gateinst-of-vl-scopestack-fix-ss

(defthm vl-replicate-gateinst-of-vl-scopestack-fix-ss
  (equal (vl-replicate-gateinst x nf (vl-scopestack-fix ss)
                                warnings)
         (vl-replicate-gateinst x nf ss warnings)))

Theorem: vl-replicate-gateinst-vl-scopestack-equiv-congruence-on-ss

(defthm vl-replicate-gateinst-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-replicate-gateinst x nf ss warnings)
                  (vl-replicate-gateinst x nf ss-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-replicate-gateinst-of-vl-warninglist-fix-warnings

(defthm vl-replicate-gateinst-of-vl-warninglist-fix-warnings
  (equal
       (vl-replicate-gateinst x nf ss (vl-warninglist-fix warnings))
       (vl-replicate-gateinst x nf ss warnings)))

Theorem: vl-replicate-gateinst-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-replicate-gateinst-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-replicate-gateinst x nf ss warnings)
                  (vl-replicate-gateinst x nf ss warnings-equiv)))
  :rule-classes :congruence)