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