		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-modinst-origidx

Retrieve the original index of a module instance if it was modified by the replicate transform.

Signature
(vl-modinst-origidx x) → index
Arguments: x — Guard (vl-modinst-p x).
Returns: index — Type (maybe-natp index).

Definitions and Theorems

Function: vl-modinst-origidx

(defun vl-modinst-origidx (x)
  (declare (xargs :guard (vl-modinst-p x)))
  (let ((__function__ 'vl-modinst-origidx))
    (declare (ignorable __function__))
    (b* (((vl-modinst x) x)
         (look (assoc-equal "VL_REPLICATE_INDEX" x.atts))
         ((when (not (cdr look))) nil)
         ((when (not (vl-expr-resolved-p (cdr look))))
          (raise "Malformed VL_REPLICATE_INDEX attribute: ~x0~%"
                 (cdr look))
          nil))
      (vl-resolved->val (cdr look)))))

Theorem: maybe-natp-of-vl-modinst-origidx

(defthm maybe-natp-of-vl-modinst-origidx
  (b* ((index (vl-modinst-origidx x)))
    (maybe-natp index))
  :rule-classes :type-prescription)

Theorem: vl-modinst-origidx-of-vl-modinst-fix-x

(defthm vl-modinst-origidx-of-vl-modinst-fix-x
  (equal (vl-modinst-origidx (vl-modinst-fix x))
         (vl-modinst-origidx x)))

Theorem: vl-modinst-origidx-vl-modinst-equiv-congruence-on-x

(defthm vl-modinst-origidx-vl-modinst-equiv-congruence-on-x
  (implies (vl-modinst-equiv x x-equiv)
           (equal (vl-modinst-origidx x)
                  (vl-modinst-origidx x-equiv)))
  :rule-classes :congruence)