Build the list of vl-emodwire-ps for a vl-plainarg-p, in LSB-first order.
(vl-plainarg-lsb-bits x walist warnings) → (mv successp warnings lsb-bits)
See vl-msb-expr-bitlist. This function just makes sure a
vl-plainarg-p isn't blank and then calls
Function:
(defun vl-plainarg-lsb-bits (x walist warnings) (declare (xargs :guard (and (vl-plainarg-p x) (vl-wirealist-p walist) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-plainarg-lsb-bits)) (declare (ignorable __function__)) (b* ((warnings (vl-warninglist-fix warnings)) (expr (vl-plainarg->expr x)) ((unless expr) (mv nil (fatal :type :vl-unsupported :msg "In vl-plainarg-lsb-bits, expected no blank ports.") nil)) ((mv successp warnings bits) (vl-msb-expr-bitlist expr walist warnings))) (mv successp warnings (reverse bits)))))
Theorem:
(defthm vl-warninglist-p-of-vl-plainarg-lsb-bits.warnings (b* (((mv ?successp ?warnings ?lsb-bits) (vl-plainarg-lsb-bits x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-plainarg-lsb-bits.lsb-bits (b* (((mv ?successp ?warnings ?lsb-bits) (vl-plainarg-lsb-bits x walist warnings))) (vl-emodwirelist-p lsb-bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-plainarg-lsb-bits.lsb-bits (b* (((mv ?successp ?warnings ?lsb-bits) (vl-plainarg-lsb-bits x walist warnings))) (true-listp lsb-bits)) :rule-classes :type-prescription)