Get the expressions from a module instance, for making implicit wires.
(vl-modinst-exprs-for-implicit-wires x) → (mv main other)
Function:
(defun vl-modinst-exprs-for-implicit-wires (x) (declare (xargs :guard (vl-modinst-p x))) (let ((__function__ 'vl-modinst-exprs-for-implicit-wires)) (declare (ignorable __function__)) (b* (((vl-modinst x) x) ((mv main other) (vl-collect-exprs-for-implicit-wires-from-portargs x.portargs))) (mv main (append other (vl-maybe-range-allexprs x.range) (vl-paramargs-allexprs x.paramargs) (vl-maybe-gatedelay-allexprs x.delay))))))
Theorem:
(defthm vl-exprlist-p-of-vl-modinst-exprs-for-implicit-wires.main (b* (((mv ?main ?other) (vl-modinst-exprs-for-implicit-wires x))) (vl-exprlist-p main)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-modinst-exprs-for-implicit-wires.other (b* (((mv ?main ?other) (vl-modinst-exprs-for-implicit-wires x))) (vl-exprlist-p other)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinst-exprs-for-implicit-wires-mvtypes-0 (true-listp (mv-nth 0 (vl-modinst-exprs-for-implicit-wires x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-modinst-exprs-for-implicit-wires-mvtypes-1 (true-listp (mv-nth 1 (vl-modinst-exprs-for-implicit-wires x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-modinst-exprs-for-implicit-wires-complete (let ((ret (vl-modinst-exprs-for-implicit-wires x))) (set-equiv (append (mv-nth 0 ret) (mv-nth 1 ret)) (vl-modinst-allexprs x))))
Theorem:
(defthm vl-modinst-exprs-for-implicit-wires-of-vl-modinst-fix-x (equal (vl-modinst-exprs-for-implicit-wires (vl-modinst-fix x)) (vl-modinst-exprs-for-implicit-wires x)))
Theorem:
(defthm vl-modinst-exprs-for-implicit-wires-vl-modinst-equiv-congruence-on-x (implies (vl-modinst-equiv x x-equiv) (equal (vl-modinst-exprs-for-implicit-wires x) (vl-modinst-exprs-for-implicit-wires x-equiv))) :rule-classes :congruence)