		Search-engine friendly clone of the ACL2 documentation.

Replicate-insts

Vl-gateinst-origidx

Retrieve the Verilog-style name for this gate instance, like foo[3], if it was modified by the replicate transform.

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

Definitions and Theorems

Function: vl-gateinst-origidx

(defun vl-gateinst-origidx (x)
  (declare (xargs :guard (vl-gateinst-p x)))
  (let ((__function__ 'vl-gateinst-origidx))
    (declare (ignorable __function__))
    (b* (((vl-gateinst 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_ORIGNAME attribute: ~x0~%"
                 (cdr look))
          nil))
      (vl-resolved->val (cdr look)))))

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

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

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

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

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

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