(vl-signedness-ambiguity-warning x signedness caveat-flag) → new-warnings
Function:
(defun vl-signedness-ambiguity-warning (x signedness caveat-flag) (declare (xargs :guard (and (vl-expr-p x) (vl-arithclass-p signedness)))) (let ((__function__ 'vl-signedness-ambiguity-warning)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (signedness (vl-arithclass-fix signedness)) (warnings nil)) (if (and signedness caveat-flag) (warn :type :vl-signedness-ambiguity :msg "Signedness of ~a0 is potentially ambiguous. NCVerilog ~ regards packed arrays of signed usertypes as unsigned, ~ and index expressions that result in signed usertypes as ~ signed, whereas VCS regards packed arrays of signed ~ usertypes as signed, and index expressions that result in ~ signed usertypes as unsigned. We think the SystemVerilog ~ spec agrees with NCVerilog's interpretation, so we have ~ labeled this expression as ~s1." :args (list x (cond ((vl-arithclass-equiv signedness :vl-signed-int-class) "signed") ((vl-arithclass-equiv signedness :vl-unsigned-int-class) "unsigned") (t (symbol-name signedness))))) (ok)))))
Theorem:
(defthm vl-warninglist-p-of-vl-signedness-ambiguity-warning (b* ((new-warnings (vl-signedness-ambiguity-warning x signedness caveat-flag))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-signedness-ambiguity-warning-of-vl-expr-fix-x (equal (vl-signedness-ambiguity-warning (vl-expr-fix x) signedness caveat-flag) (vl-signedness-ambiguity-warning x signedness caveat-flag)))
Theorem:
(defthm vl-signedness-ambiguity-warning-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-signedness-ambiguity-warning x signedness caveat-flag) (vl-signedness-ambiguity-warning x-equiv signedness caveat-flag))) :rule-classes :congruence)
Theorem:
(defthm vl-signedness-ambiguity-warning-of-vl-arithclass-fix-signedness (equal (vl-signedness-ambiguity-warning x (vl-arithclass-fix signedness) caveat-flag) (vl-signedness-ambiguity-warning x signedness caveat-flag)))
Theorem:
(defthm vl-signedness-ambiguity-warning-vl-arithclass-equiv-congruence-on-signedness (implies (vl-arithclass-equiv signedness signedness-equiv) (equal (vl-signedness-ambiguity-warning x signedness caveat-flag) (vl-signedness-ambiguity-warning x signedness-equiv caveat-flag))) :rule-classes :congruence)