Creates, e.g., the expression
This is mostly dealing with sizing. Recall from 5.5.1 that comparisons always produce unsigned results. Our guard is strong enough to ensure that we'll always have equal-width expressions and that we know their types. We haven't assumed anything about their types agreeing. To make sure that we produce well-typed expressions, we'll coerce anything signed into an unsigned equivalent, by just wrapping it in a one-bit concatenation.
Function:
(defun vl-casestmt-compare-expr1 (test expr) (declare (xargs :guard (and (vl-expr-p test) (vl-expr-p expr)))) (declare (xargs :guard (and (vl-expr->finaltype test) (vl-expr->finaltype expr) (posp (vl-expr->finalwidth test)) (equal (vl-expr->finalwidth test) (vl-expr->finalwidth expr))))) (let ((__function__ 'vl-casestmt-compare-expr1)) (declare (ignorable __function__)) (b* ((width (vl-expr->finalwidth test)) (test-fix (case (vl-expr->finaltype test) (:vl-unsigned test) (:vl-signed (make-vl-nonatom :op :vl-concat :args (list test) :finalwidth width :finaltype :vl-unsigned)) (otherwise (progn$ (impossible) test)))) (expr-fix (case (vl-expr->finaltype expr) (:vl-unsigned expr) (:vl-signed (make-vl-nonatom :op :vl-concat :args (list expr) :finalwidth width :finaltype :vl-unsigned)) (otherwise (progn$ (impossible) expr))))) (make-vl-nonatom :op :vl-binary-ceq :args (list test-fix expr-fix) :finaltype :vl-unsigned :finalwidth 1))))
Theorem:
(defthm vl-expr-p-of-vl-casestmt-compare-expr1 (b* ((compare-expr (vl-casestmt-compare-expr1 test expr))) (vl-expr-p compare-expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-casestmt-compare-expr1 (b* ((compare-expr (vl-casestmt-compare-expr1 test expr))) (equal (vl-expr->finalwidth compare-expr) 1)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finaltype-of-vl-casestmt-compare-expr1 (b* ((compare-expr (vl-casestmt-compare-expr1 test expr))) (equal (vl-expr->finaltype compare-expr) :vl-unsigned)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-casestmt-compare-expr1 (implies (and (force (posp (vl-expr->finalwidth test))) (force (vl-expr->finaltype test)) (force (vl-expr->finaltype expr)) (force (equal (vl-expr->finalwidth test) (vl-expr->finalwidth expr))) (force (vl-expr-welltyped-p test)) (force (vl-expr-welltyped-p expr))) (vl-expr-welltyped-p (vl-casestmt-compare-expr1 test expr))))
Theorem:
(defthm vl-casestmt-compare-expr1-of-vl-expr-fix-test (equal (vl-casestmt-compare-expr1 (vl-expr-fix test) expr) (vl-casestmt-compare-expr1 test expr)))
Theorem:
(defthm vl-casestmt-compare-expr1-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-compare-expr1 test expr) (vl-casestmt-compare-expr1 test-equiv expr))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-compare-expr1-of-vl-expr-fix-expr (equal (vl-casestmt-compare-expr1 test (vl-expr-fix expr)) (vl-casestmt-compare-expr1 test expr)))
Theorem:
(defthm vl-casestmt-compare-expr1-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-casestmt-compare-expr1 test expr) (vl-casestmt-compare-expr1 test expr-equiv))) :rule-classes :congruence)