Construct the expression to replace
(vl-wildeq-replacement-expr lhs care-mask zapped atts) → new-x
LHS could be anything, but since X is well-typed we know that its width is positive and that its signedness agrees with the signedness of RHS. Moreover we constructed the care-mask and zap-expr in such a way that they also agree on this width and signedness. Hence, everything lines up perfectly and we're ready to go.
In the ==? case, we want to make sure that LHS agrees with RHS on all of the care bits, i.e., that
(LHS & CARE-MASK) == (RHS & CARE-MASK)
It is perhaps nicer to write
(LHS & CARE-MASK) == ZAPPED
Except that, per oprewrite, we would rather write this as:
& ( (LHS & CARE-MASK) ~^ ZAPPED )
Function:
(defun vl-wildeq-replacement-expr (lhs care-mask zapped atts) (declare (xargs :guard (and (vl-expr-p lhs) (vl-expr-p care-mask) (vl-expr-p zapped) (vl-atts-p atts)))) (declare (xargs :guard (and (vl-expr-welltyped-p lhs) (vl-expr-welltyped-p care-mask) (vl-expr-welltyped-p zapped) (posp (vl-expr->finalwidth lhs)) (equal (vl-expr->finalwidth care-mask) (vl-expr->finalwidth lhs)) (equal (vl-expr->finalwidth zapped) (vl-expr->finalwidth lhs)) (vl-expr->finaltype lhs) (equal (vl-expr->finaltype care-mask) (vl-expr->finaltype lhs)) (equal (vl-expr->finaltype zapped) (vl-expr->finaltype lhs))))) (let ((__function__ 'vl-wildeq-replacement-expr)) (declare (ignorable __function__)) (b* ((width (vl-expr->finalwidth lhs)) (type (vl-expr->finaltype lhs)) (masked-lhs (make-vl-nonatom :op :vl-binary-bitand :args (list lhs care-mask) :finalwidth width :finaltype type)) (inner-iff (make-vl-nonatom :op :vl-binary-xnor :args (list masked-lhs zapped) :finalwidth width :finaltype type))) (make-vl-nonatom :op :vl-unary-bitand :args (list inner-iff) :finalwidth 1 :finaltype :vl-unsigned :atts atts))))
Theorem:
(defthm vl-expr-p-of-vl-wildeq-replacement-expr (b* ((new-x (vl-wildeq-replacement-expr lhs care-mask zapped atts))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-wildeq-replacement-expr (implies (and (force (vl-expr-p lhs)) (force (vl-expr-p care-mask)) (force (vl-expr-p zapped)) (force (vl-atts-p atts)) (force (vl-expr-welltyped-p lhs)) (force (vl-expr-welltyped-p care-mask)) (force (vl-expr-welltyped-p zapped)) (force (posp (vl-expr->finalwidth$inline lhs))) (force (equal (vl-expr->finalwidth$inline care-mask) (vl-expr->finalwidth$inline lhs))) (force (equal (vl-expr->finalwidth$inline zapped) (vl-expr->finalwidth$inline lhs))) (force (vl-expr->finaltype$inline lhs)) (force (equal (vl-expr->finaltype$inline care-mask) (vl-expr->finaltype$inline lhs))) (force (equal (vl-expr->finaltype$inline zapped) (vl-expr->finaltype$inline lhs)))) (b* ((new-x (vl-wildeq-replacement-expr lhs care-mask zapped atts))) (vl-expr-welltyped-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-wildeq-replacement-expr-basics (b* ((new-x (vl-wildeq-replacement-expr lhs care-mask zapped atts))) (and (equal (vl-expr->finalwidth new-x) 1) (equal (vl-expr->finaltype new-x) :vl-unsigned))) :rule-classes :rewrite)
Theorem:
(defthm vl-wildeq-replacement-expr-of-vl-expr-fix-lhs (equal (vl-wildeq-replacement-expr (vl-expr-fix lhs) care-mask zapped atts) (vl-wildeq-replacement-expr lhs care-mask zapped atts)))
Theorem:
(defthm vl-wildeq-replacement-expr-vl-expr-equiv-congruence-on-lhs (implies (vl-expr-equiv lhs lhs-equiv) (equal (vl-wildeq-replacement-expr lhs care-mask zapped atts) (vl-wildeq-replacement-expr lhs-equiv care-mask zapped atts))) :rule-classes :congruence)
Theorem:
(defthm vl-wildeq-replacement-expr-of-vl-expr-fix-care-mask (equal (vl-wildeq-replacement-expr lhs (vl-expr-fix care-mask) zapped atts) (vl-wildeq-replacement-expr lhs care-mask zapped atts)))
Theorem:
(defthm vl-wildeq-replacement-expr-vl-expr-equiv-congruence-on-care-mask (implies (vl-expr-equiv care-mask care-mask-equiv) (equal (vl-wildeq-replacement-expr lhs care-mask zapped atts) (vl-wildeq-replacement-expr lhs care-mask-equiv zapped atts))) :rule-classes :congruence)
Theorem:
(defthm vl-wildeq-replacement-expr-of-vl-expr-fix-zapped (equal (vl-wildeq-replacement-expr lhs care-mask (vl-expr-fix zapped) atts) (vl-wildeq-replacement-expr lhs care-mask zapped atts)))
Theorem:
(defthm vl-wildeq-replacement-expr-vl-expr-equiv-congruence-on-zapped (implies (vl-expr-equiv zapped zapped-equiv) (equal (vl-wildeq-replacement-expr lhs care-mask zapped atts) (vl-wildeq-replacement-expr lhs care-mask zapped-equiv atts))) :rule-classes :congruence)
Theorem:
(defthm vl-wildeq-replacement-expr-of-vl-atts-fix-atts (equal (vl-wildeq-replacement-expr lhs care-mask zapped (vl-atts-fix atts)) (vl-wildeq-replacement-expr lhs care-mask zapped atts)))
Theorem:
(defthm vl-wildeq-replacement-expr-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-wildeq-replacement-expr lhs care-mask zapped atts) (vl-wildeq-replacement-expr lhs care-mask zapped atts-equiv))) :rule-classes :congruence)