Compute the care mask and zapped right-hand side for an
Function:
(defun vl-wildeq-decompose-rhs (rhs) (declare (xargs :guard (vl-expr-p rhs))) (declare (xargs :guard (vl-expr-welltyped-p rhs))) (let ((__function__ 'vl-wildeq-decompose-rhs)) (declare (ignorable __function__)) (b* (((mv okp msb-bits) (vl-intliteral-msb-bits rhs)) ((unless okp) (mv nil nil nil)) (finalwidth (vl-expr->finalwidth rhs)) (finaltype (vl-expr->finaltype rhs)) ((unless (posp finalwidth)) (mv nil nil nil)) ((unless finaltype) (mv nil nil nil)) (cm-value (vl-msb-bits-to-zx-care-mask msb-bits 0)) (cm-guts (make-vl-constint :value cm-value :origwidth finalwidth :origtype finaltype)) (cm-expr (make-vl-atom :guts cm-guts :finalwidth finalwidth :finaltype finaltype)) (zap-bits (vl-msb-bits-zap-dontcares-zx msb-bits)) (zap-expr (vl-msb-bits-to-intliteral zap-bits finaltype))) (mv t cm-expr zap-expr))))
Theorem:
(defthm booleanp-of-vl-wildeq-decompose-rhs.okp (b* (((mv ?okp ?care-mask ?zapped) (vl-wildeq-decompose-rhs rhs))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-wildeq-decompose-rhs.care-mask (b* (((mv ?okp ?care-mask ?zapped) (vl-wildeq-decompose-rhs rhs))) (equal (vl-expr-p care-mask) (if okp t nil))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-wildeq-decompose-rhs.zapped (b* (((mv ?okp ?care-mask ?zapped) (vl-wildeq-decompose-rhs rhs))) (equal (vl-expr-p zapped) (if okp t nil))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-wildeq-decompose-rhs.care-mask (implies (vl-expr-welltyped-p rhs) (b* (((mv ?okp ?care-mask ?zapped) (vl-wildeq-decompose-rhs rhs))) (implies okp (and (vl-expr-welltyped-p care-mask) (equal (vl-expr->finalwidth care-mask) (vl-expr->finalwidth rhs)) (equal (vl-expr->finaltype care-mask) (vl-expr->finaltype rhs)))))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-wildeq-decompose-rhs.zapped (implies (vl-expr-welltyped-p rhs) (b* (((mv ?okp ?care-mask ?zapped) (vl-wildeq-decompose-rhs rhs))) (implies okp (and (vl-expr-welltyped-p zapped) (equal (vl-expr->finalwidth zapped) (vl-expr->finalwidth rhs)) (equal (vl-expr->finaltype zapped) (vl-expr->finaltype rhs)))))) :rule-classes :rewrite)
Theorem:
(defthm vl-wildeq-decompose-rhs-of-vl-expr-fix-rhs (equal (vl-wildeq-decompose-rhs (vl-expr-fix rhs)) (vl-wildeq-decompose-rhs rhs)))
Theorem:
(defthm vl-wildeq-decompose-rhs-vl-expr-equiv-congruence-on-rhs (implies (vl-expr-equiv rhs rhs-equiv) (equal (vl-wildeq-decompose-rhs rhs) (vl-wildeq-decompose-rhs rhs-equiv))) :rule-classes :congruence)