Propagate the final width and type of an expression into a constant integer atom.
(vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) → (mv successp warnings new-x)
Warning: this function should typically only be called by the expression-sizing transform.
We expect that the finalwidth is at least as large as the constant's original width, and that if the constant was originally unsigned then the finaltype should also be unsigned. If these conditions are not met, expansion fails with fatal warnings.
The new atom we build,
In certain cases we issue non-fatal "compatibility warnings" to say that an expression might have different values on different Verilog implementations. It is scary to expand originally-unsized numbers (most frequently plain decimal numbers) past 32-bits because this could perhaps result in implementation-dependent behavior. For instance, consider:
wire signed [47:0] foo, bar; assign bar = ...; assign foo = bar + 'h 8000_0000 ; // bar + 2^31
Suppose
So, when can these kinds of problems arise?
If bar was unsigned, then I think there is no problem because we will need
to zero-extend the 2^31 to 48 bits, which yields
I once imagined that the sign-bit of the constant had to be 1 to cause problems, but it is still possible to demonstrate a compatibility problem with a zero sign bit. On the other hand, because examples I can think of seem to rely upon shift operations and hence be relatively unlikely, I mark these as minor warnings. Here is an example of such a problem:
wire signed [47:0] foo, bar; assign bar = ...; assign foo = (bar + 5) >> 1;
Suppose bar is
Function:
(defun vl-constint-atom-expandsizes (x finalwidth finaltype ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (natp finalwidth) (vl-exprtype-p finaltype) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (vl-atom-p x) (vl-fast-constint-p (vl-atom->guts x))))) (let ((__function__ 'vl-constint-atom-expandsizes)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (ctx (vl-context-fix ctx)) (finalwidth (lnfix finalwidth)) (finaltype (vl-exprtype-fix finaltype)) (guts (vl-atom->guts x)) ((vl-constint guts) guts) ((when (> guts.origwidth finalwidth)) (mv nil (fatal :type :vl-programming-error :msg "~a0: origwidth > finalwidth when expanding ~a1. ~ This indicates a serious bug in our sizing code." :args (list ctx x)) x)) ((unless (or (eq guts.origtype finaltype) (and (eq guts.origtype :vl-signed) (eq finaltype :vl-unsigned)))) (mv nil (fatal :type :vl-programming-error :msg "~a0: origtype is ~s1 but finaltype is ~s2 when ~ expanding ~a3. This indicates a serious bug in ~ our typing code." :args (list ctx guts.origtype finaltype x)) x)) ((when (= guts.origwidth finalwidth)) (b* ((new-guts (if (eq guts.origtype finaltype) guts (change-vl-constint guts :origwidth finalwidth :origtype finaltype))) (new-x (change-vl-atom x :guts new-guts :finalwidth finalwidth :finaltype finaltype))) (mv t (ok) new-x))) ((when (eq finaltype :vl-unsigned)) (b* ((new-guts (change-vl-constint guts :origwidth finalwidth :origtype finaltype)) (new-x (change-vl-atom x :guts new-guts :finalwidth finalwidth :finaltype finaltype))) (mv t (ok) new-x))) (new-value (vl-sign-extend-constint guts.value guts.origwidth finalwidth)) (new-guts (change-vl-constint guts :value new-value :origwidth finalwidth)) (new-x (change-vl-atom x :guts new-guts :finalwidth finalwidth :finaltype finaltype)) ((unless guts.wasunsized) (mv t (ok) new-x)) (minorp (= new-value guts.value)) (warnings (warn :type (if minorp :vl-warn-integer-size-minor :vl-warn-integer-size) :msg (if minorp "~a0: the unsized integer ~a1 occurs in a context ~ that is larger than 32-bits. In rare cases ~ (particularly involving right-shifts), the ~ resulting expression may produce different results ~ on Verilog implementations with different integer ~ sizes; consider adding an explicit size to this ~ number." "~a0: the unsized integer ~a1 occurs in a signed ~ context that is larger than 32-bits; it is likely ~ that this could cause the expression results to ~ differ between Verilog implementations that have ~ different integer sizes. Adding an explicit size to ~ this number is recommended.") :args (list ctx x)))) (mv t warnings new-x))))
Theorem:
(defthm booleanp-of-vl-constint-atom-expandsizes.successp (b* (((mv ?successp ?warnings ?new-x) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-constint-atom-expandsizes.warnings (b* (((mv ?successp ?warnings ?new-x) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-constint-atom-expandsizes.new-x (b* (((mv ?successp ?warnings ?new-x) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm warning-irrelevance-of-vl-constint-atom-expandsizes (let ((ret1 (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)) (ret2 (vl-constint-atom-expandsizes x finalwidth finaltype nil nil))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (and (equal (mv-nth 0 ret1) (mv-nth 0 ret2)) (equal (mv-nth 2 ret1) (mv-nth 2 ret2))))))
Theorem:
(defthm no-change-loserp-of-vl-constint-atom-expandsizes (let ((ret (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (implies (not (mv-nth 0 ret)) (equal (mv-nth 2 ret) (vl-expr-fix x)))))
Theorem:
(defthm vl-expr-welltyped-p-of-vl-constint-atom-expandsizes (let ((ret (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (implies (and (mv-nth 0 ret) (force (vl-atom-p x)) (force (vl-constint-p (vl-atom->guts x)))) (vl-expr-welltyped-p (mv-nth 2 ret)))))
Theorem:
(defthm vl-expr->finalwidth-of-vl-constint-atom-expandsizes (let ((ret (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (implies (and (mv-nth 0 ret) (force (vl-atom-p x)) (force (vl-constint-p (vl-atom->guts x)))) (equal (vl-expr->finalwidth (mv-nth 2 ret)) (nfix finalwidth)))))
Theorem:
(defthm vl-expr->finaltype-of-vl-constint-atom-expandsizes (let ((ret (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings))) (implies (and (mv-nth 0 ret) (force (vl-atom-p x)) (force (vl-constint-p (vl-atom->guts x)))) (equal (vl-expr->finaltype (mv-nth 2 ret)) (vl-exprtype-fix finaltype)))))
Theorem:
(defthm vl-constint-atom-expandsizes-of-vl-expr-fix-x (equal (vl-constint-atom-expandsizes (vl-expr-fix x) finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)))
Theorem:
(defthm vl-constint-atom-expandsizes-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x-equiv finalwidth finaltype ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-constint-atom-expandsizes-of-nfix-finalwidth (equal (vl-constint-atom-expandsizes x (nfix finalwidth) finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)))
Theorem:
(defthm vl-constint-atom-expandsizes-nat-equiv-congruence-on-finalwidth (implies (acl2::nat-equiv finalwidth finalwidth-equiv) (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth-equiv finaltype ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-constint-atom-expandsizes-of-vl-exprtype-fix-finaltype (equal (vl-constint-atom-expandsizes x finalwidth (vl-exprtype-fix finaltype) ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)))
Theorem:
(defthm vl-constint-atom-expandsizes-vl-exprtype-equiv-congruence-on-finaltype (implies (vl-exprtype-equiv finaltype finaltype-equiv) (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-constint-atom-expandsizes-of-vl-context-fix-ctx (equal (vl-constint-atom-expandsizes x finalwidth finaltype (vl-context-fix ctx) warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)))
Theorem:
(defthm vl-constint-atom-expandsizes-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-constint-atom-expandsizes-of-vl-warninglist-fix-warnings (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx (vl-warninglist-fix warnings)) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings)))
Theorem:
(defthm vl-constint-atom-expandsizes-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) (vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings-equiv))) :rule-classes :congruence)