Special warnings about shifting by signed amounts.
(vl-warn-about-signed-shifts rhs ctx warnings) → new-warnings
See expression-sizing-minutia; we warn about shifts by a signed value since Verilog-XL doesn't handle them correctly.
Function:
(defun vl-warn-about-signed-shifts (rhs ctx warnings) (declare (xargs :guard (and (vl-expr-p rhs) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (vl-expr->finaltype rhs))) (let ((__function__ 'vl-warn-about-signed-shifts)) (declare (ignorable __function__)) (b* ((rhs (vl-expr-fix rhs)) (ctx (vl-context-fix ctx)) (want-to-warn-p (b* (((unless (eq (vl-expr->finaltype rhs) :vl-signed)) nil) ((unless (vl-fast-atom-p rhs)) t) (guts (vl-atom->guts rhs)) ((unless (vl-constint-p guts)) t) (val (vl-constint->value guts)) (width (vl-constint->origwidth guts))) (logbitp (- width 1) val))) ((unless want-to-warn-p) (ok))) (warn :type :vl-warn-signed-shift :msg "~a0: found a shift-expression with a signed shift amount, ~ ~a1. This is dangerous because whereas NCVerilog properly ~ follows the Verilog-2005 standard (5.1.12) and treats the ~ right-hand side as unsigned, Verilog-XL incorrectly treats ~ negative right-shifts as left-shifts. We follow the ~ Verilog-2005 standard and mimick NCVerilog, but to ensure ~ compatibility, you should probably rewrite this expression to ~ ensure that the right-hand side is unsigned. For example, ~ you might wrap the right-hand side in a concatnation, e.g., ~ \"a >> {b}\" instead of \"a >> b\"." :args (list ctx rhs)))))
Theorem:
(defthm vl-warninglist-p-of-vl-warn-about-signed-shifts (b* ((new-warnings (vl-warn-about-signed-shifts rhs ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-warn-about-signed-shifts-of-vl-expr-fix-rhs (equal (vl-warn-about-signed-shifts (vl-expr-fix rhs) ctx warnings) (vl-warn-about-signed-shifts rhs ctx warnings)))
Theorem:
(defthm vl-warn-about-signed-shifts-vl-expr-equiv-congruence-on-rhs (implies (vl-expr-equiv rhs rhs-equiv) (equal (vl-warn-about-signed-shifts rhs ctx warnings) (vl-warn-about-signed-shifts rhs-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-signed-shifts-of-vl-context-fix-ctx (equal (vl-warn-about-signed-shifts rhs (vl-context-fix ctx) warnings) (vl-warn-about-signed-shifts rhs ctx warnings)))
Theorem:
(defthm vl-warn-about-signed-shifts-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-warn-about-signed-shifts rhs ctx warnings) (vl-warn-about-signed-shifts rhs ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-signed-shifts-of-vl-warninglist-fix-warnings (equal (vl-warn-about-signed-shifts rhs ctx (vl-warninglist-fix warnings)) (vl-warn-about-signed-shifts rhs ctx warnings)))
Theorem:
(defthm vl-warn-about-signed-shifts-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-warn-about-signed-shifts rhs ctx warnings) (vl-warn-about-signed-shifts rhs ctx warnings-equiv))) :rule-classes :congruence)