(vl-portinfo-to-svex-assign-or-alias x instname range) → (mv warnings assigns aliases)
Function:
(defun vl-portinfo-to-svex-assign-or-alias (x instname range) (declare (xargs :guard (and (vl-portinfo-p x) (stringp instname) (vl-maybe-range-p range)))) (declare (xargs :guard (and (sv::svarlist-addr-p (vl-portinfo-vars x)) (vl-maybe-range-resolved-p range)))) (let ((__function__ 'vl-portinfo-to-svex-assign-or-alias)) (declare (ignorable __function__)) (b* ((instname (string-fix instname)) (range (vl-maybe-range-fix range)) (warnings nil)) (vl-portinfo-case x :bad (mv (ok) nil nil) :regular (b* (((when (and (not x.conn-expr) (not x.port-lhs))) (mv (ok) nil nil)) (xwidth (if (and range (not x.replicatedp)) (* x.port-size (vl-range-size range)) x.port-size)) (lhsp (sv::lhssvex-bounded-p xwidth x.conn-svex)) ((when (and (not lhsp) x.interfacep)) (mv (fatal :type :vl-interfaceport-bad-connection :msg "Non-LHS connection on interfaceport: .~s0(~a1)" :args (list x.portname x.conn-expr)) nil nil)) (warnings (if (and (not lhsp) (eq x.port-dir :vl-output)) (warn :type :vl-port-direction-mismatch :msg "Non-LHS expression ~a1 on output port ~s0" :args (list x.portname x.conn-expr)) (ok))) ((when (not x.port-lhs)) (mv (ok) (and lhsp (list (cons (sv::svex->lhs-bound xwidth x.conn-svex) (sv::make-driver :value (sv::svex-z))))) nil)) ((unless (equal x.port-size (sv::lhs-width x.port-lhs))) (mv (fatal :type :vl-port-resolution-programming-error :msg "On port ~s0: Port size ~a1 didn't match port expression width ~a2" :args (list x.portname x.port-size (sv::lhs-width x.port-lhs))) nil nil)) (alias? (and lhsp x.conn-expr)) (conn (if alias? (sv::svex->lhs-bound xwidth x.conn-svex) (sv::make-driver :value x.conn-svex)))) (if range (b* ((size (vl-range-size range)) (lsb (vl-resolved->val (vl-range->lsb range))) (incr (if (vl-range-revp range) -1 1))) (if x.replicatedp (if alias? (mv (ok) nil (vl-instarray-replicated-port-aliases x.port-lhs instname conn lsb size incr)) (mv (ok) (vl-instarray-replicated-port-assigns x.port-lhs instname conn lsb size incr) nil)) (b* ((port-lhs (vl-instarray-nonreplicated-port-lhs x.port-lhs instname lsb size incr))) (if alias? (mv (ok) nil (list (cons conn port-lhs))) (mv (ok) (list (cons port-lhs conn)) nil))))) (b* ((port-lhs (sv::lhs-add-namespace instname x.port-lhs))) (if alias? (mv (ok) nil (list (cons port-lhs conn))) (mv (ok) (list (cons port-lhs conn)) nil)))))))))
Theorem:
(defthm vl-warninglist-p-of-vl-portinfo-to-svex-assign-or-alias.warnings (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfo-to-svex-assign-or-alias x instname range))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-portinfo-to-svex-assign-or-alias.assigns (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfo-to-svex-assign-or-alias x instname range))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-portinfo-to-svex-assign-or-alias.aliases (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfo-to-svex-assign-or-alias x instname range))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm var-of-vl-portinfo-to-svex-assign-or-alias (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfo-to-svex-assign-or-alias x instname range))) (implies (sv::svarlist-addr-p (vl-portinfo-vars x)) (and (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))))
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-mvtypes-1 (true-listp (mv-nth 1 (vl-portinfo-to-svex-assign-or-alias x instname range))) :rule-classes :type-prescription)
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-mvtypes-2 (true-listp (mv-nth 2 (vl-portinfo-to-svex-assign-or-alias x instname range))) :rule-classes :type-prescription)
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-of-vl-portinfo-fix-x (equal (vl-portinfo-to-svex-assign-or-alias (vl-portinfo-fix x) instname range) (vl-portinfo-to-svex-assign-or-alias x instname range)))
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-vl-portinfo-equiv-congruence-on-x (implies (vl-portinfo-equiv x x-equiv) (equal (vl-portinfo-to-svex-assign-or-alias x instname range) (vl-portinfo-to-svex-assign-or-alias x-equiv instname range))) :rule-classes :congruence)
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-of-str-fix-instname (equal (vl-portinfo-to-svex-assign-or-alias x (str-fix instname) range) (vl-portinfo-to-svex-assign-or-alias x instname range)))
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-portinfo-to-svex-assign-or-alias x instname range) (vl-portinfo-to-svex-assign-or-alias x instname-equiv range))) :rule-classes :congruence)
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-of-vl-maybe-range-fix-range (equal (vl-portinfo-to-svex-assign-or-alias x instname (vl-maybe-range-fix range)) (vl-portinfo-to-svex-assign-or-alias x instname range)))
Theorem:
(defthm vl-portinfo-to-svex-assign-or-alias-vl-maybe-range-equiv-congruence-on-range (implies (vl-maybe-range-equiv range range-equiv) (equal (vl-portinfo-to-svex-assign-or-alias x instname range) (vl-portinfo-to-svex-assign-or-alias x instname range-equiv))) :rule-classes :congruence)