Retrieve the Verilog-style name for this module instance, like foo[3],
if it was modified by the
(vl-modinst-origname/idx x) → verilog-name
Function:
(defun vl-modinst-origname/idx (x) (declare (xargs :guard (vl-modinst-p x))) (let ((__function__ 'vl-modinst-origname/idx)) (declare (ignorable __function__)) (b* ((origname (vl-modinst-origname x)) ((unless origname) nil) (origidx (vl-modinst-origidx x))) (if origidx (cat origname "[" (natstr origidx) "]") origname))))
Theorem:
(defthm maybe-stringp-of-vl-modinst-origname/idx (b* ((verilog-name (vl-modinst-origname/idx x))) (maybe-stringp verilog-name)) :rule-classes :type-prescription)
Theorem:
(defthm vl-modinst-origname/idx-of-vl-modinst-fix-x (equal (vl-modinst-origname/idx (vl-modinst-fix x)) (vl-modinst-origname/idx x)))
Theorem:
(defthm vl-modinst-origname/idx-vl-modinst-equiv-congruence-on-x (implies (vl-modinst-equiv x x-equiv) (equal (vl-modinst-origname/idx x) (vl-modinst-origname/idx x-equiv))) :rule-classes :congruence)