Check case statements for compatible sizes, and issue warnings if we find any incompatible sizes.
(vl-casestmt-size-warnings test cases ctx) → warnings
Regarding the sizing of case expressions, the Verilog-2005 standard (9.5) says:
Care is needed in specifying the expressions in the case statement. The bit length of all the expressions shall be equal so that exact bitwise matching can be performed. The length of all the case item expressions, as well as the case expression in the parentheses, shall be made equal to the length of the longest case expression and case item expression. If any of these expressions is unsigned, then all of them shall be treated as unsigned. If all of these expressions are signed.
This is just a wrapper for vl-casestmt-size-warnings-aux, which does most of the real work. We have this wrapper mainly to avoid giving multiple warnings if there is some problem with sizing the test expression. (This would typically cause one warning per match expression if we just called the aux function without checking for it.)
BOZO we should eventually properly incorporate this into our expression-sizing code.
Function:
(defun vl-casestmt-size-warnings (test cases ctx) (declare (xargs :guard (and (vl-expr-p test) (vl-caselist-p cases) (vl-modelement-p ctx)))) (let ((__function__ 'vl-casestmt-size-warnings)) (declare (ignorable __function__)) (b* ((test (vl-expr-fix test)) (ctx (vl-modelement-fix ctx)) ((unless (and (posp (vl-expr->finalwidth test)) (vl-expr->finaltype test))) (list (make-vl-warning :type :vl-case-stmt-size :msg "In ~a0: case statement is testing expression whose ~ size/type was not successfully determined: ~a1." :args (list ctx test) :fn __function__)))) (vl-casestmt-size-warnings-aux test cases ctx))))
Theorem:
(defthm vl-warninglist-p-of-vl-casestmt-size-warnings (b* ((warnings (vl-casestmt-size-warnings test cases ctx))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-casestmt-size-warnings (b* ((warnings (vl-casestmt-size-warnings test cases ctx))) (true-listp warnings)) :rule-classes :type-prescription)
Theorem:
(defthm widths-after-vl-casestmt-size-warnings (implies (not (vl-casestmt-size-warnings test cases ctx)) (and (posp (vl-expr->finalwidth test)) (vl-expr->finaltype test) (vl-casestmt-sizes-agreep test cases))))
Theorem:
(defthm vl-casestmt-size-warnings-of-vl-expr-fix-test (equal (vl-casestmt-size-warnings (vl-expr-fix test) cases ctx) (vl-casestmt-size-warnings test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-size-warnings test cases ctx) (vl-casestmt-size-warnings test-equiv cases ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-size-warnings-of-vl-caselist-fix-cases (equal (vl-casestmt-size-warnings test (vl-caselist-fix cases) ctx) (vl-casestmt-size-warnings test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casestmt-size-warnings test cases ctx) (vl-casestmt-size-warnings test cases-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-size-warnings-of-vl-modelement-fix-ctx (equal (vl-casestmt-size-warnings test cases (vl-modelement-fix ctx)) (vl-casestmt-size-warnings test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casestmt-size-warnings test cases ctx) (vl-casestmt-size-warnings test cases ctx-equiv))) :rule-classes :congruence)