Compute the port pattern for a module.
(vl-portlist-msb-bit-pattern x walist) → (mv successp warnings pattern)
We don't take a warnings accumulator because we memoize this function.
Function:
(defun vl-portlist-msb-bit-pattern (x walist) (declare (xargs :guard (and (vl-portlist-p x) (vl-wirealist-p walist)))) (let ((__function__ 'vl-portlist-msb-bit-pattern)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t nil nil)) ((mv successp1 warnings1 wires1) (vl-port-msb-bits (car x) walist)) ((mv successp2 warnings2 wires2) (vl-portlist-msb-bit-pattern (cdr x) walist))) (mv (and successp1 successp2) (append-without-guard warnings1 warnings2) (cons wires1 wires2)))))
Theorem:
(defthm booleanp-of-vl-portlist-msb-bit-pattern.successp (b* (((mv ?successp ?warnings ?pattern) (vl-portlist-msb-bit-pattern x walist))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-portlist-msb-bit-pattern.warnings (b* (((mv ?successp ?warnings ?pattern) (vl-portlist-msb-bit-pattern x walist))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelistlist-p-of-vl-portlist-msb-bit-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-portlist-msb-bit-pattern x walist))) (vl-emodwirelistlist-p pattern)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-portlist-msb-bit-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-portlist-msb-bit-pattern x walist))) (true-listp pattern)) :rule-classes :type-prescription)
Theorem:
(defthm true-list-listp-of-vl-portlist-msb-bit-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-portlist-msb-bit-pattern x walist))) (true-list-listp pattern)) :rule-classes :rewrite)