Compute the port pattern for a single port.
(vl-port-msb-bits x walist) → (mv successp warnings msb-bits)
Function:
(defun vl-port-msb-bits (x walist) (declare (xargs :guard (and (vl-port-p x) (vl-wirealist-p walist)))) (let ((__function__ 'vl-port-msb-bits)) (declare (ignorable __function__)) (b* ((warnings nil) (x (vl-port-fix x)) ((when (eq (tag x) :vl-interfaceport)) (mv nil (fatal :type :vl-bad-port :msg "~a0: interface ports are not supported." :args (list x)) nil)) (expr (vl-regularport->expr x)) ((unless expr) (mv nil (fatal :type :vl-bad-port :msg "~a0: expected no blank ports." :args (list x)) nil)) ((mv successp warnings msb-bits) (vl-msb-expr-bitlist expr walist warnings)) ((unless successp) (mv nil (fatal :type :vl-bad-port :msg "~a0: failed to generate wires for this port." :args (list x)) nil))) (mv t warnings msb-bits))))
Theorem:
(defthm booleanp-of-vl-port-msb-bits.successp (b* (((mv ?successp ?warnings ?msb-bits) (vl-port-msb-bits x walist))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-port-msb-bits.warnings (b* (((mv ?successp ?warnings ?msb-bits) (vl-port-msb-bits x walist))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-port-msb-bits.msb-bits (b* (((mv ?successp ?warnings ?msb-bits) (vl-port-msb-bits x walist))) (vl-emodwirelist-p msb-bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-port-msb-bits.msb-bits (b* (((mv ?successp ?warnings ?msb-bits) (vl-port-msb-bits x walist))) (true-listp msb-bits)) :rule-classes :type-prescription)