		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-expandsizes

Vl-constint-atom-expandsizes

Propagate the final width and type of an expression into a constant integer atom.

Signature
(vl-constint-atom-expandsizes x finalwidth finaltype ctx warnings) → (mv successp warnings new-x)
Arguments: x — Guard (vl-expr-p x).; finalwidth — Guard (natp finalwidth).; finaltype — Guard (vl-exprtype-p finaltype).; ctx — Guard (vl-context-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; new-x — Type (vl-expr-p 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, x-prime will have a new vl-constint-p for its guts, where the origwidth and origtype have been modified to match the final width and type of the atom. We have no choice but to do this in the case of a true sign extension, because the new value might not fit into the original width. So for consistency we do it in all cases. BOZO having :finalwidth and :finaltype fields for atoms seems somewhat redundant if we are changing the width and type of the guts. We could consider forcing these fields to either be nil or to agree with the constint's width/type (and similarly for weirdints). Otherwise we can make this part of well-typed expressions, but I'm partial to the former.

Compatibility Warnings

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 bar is zero. On a 32-bit system, the 2^31 represents a negative number, so when we sign-extend it to 48 bits we get FFFF_8000_0000. The final value of foo is thus FFFF_8000_0000. But on a 64-bit system, the 2^31 represents a positive number and we would instead end up sign-extending bar to 64 bits. The 64-bit addition produces 0000_0000_8000_0000 which is then truncated to 48 bits. The final value of foo is thus 0000_8000_0000, which does not match the 32-bit implementation.

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 0000_8000_0000 regardless of whether we are on a 32-bit, 64-bit, or other-bit implementation.

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 FFFF_FFFF_FFFF. On the 64-bit implementation, the addition produces is done in 64 bits and produces 1_0000_0000_0004, which is then shifted to obtain 8000_0000_0002. On a 32-bit implementation, the addition is only done in 48 bits and the carry is lost, so the sum is 4 and the final result is 2.

Definitions and Theorems

Function: vl-constint-atom-expandsizes

(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: booleanp-of-vl-constint-atom-expandsizes.successp

(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: vl-warninglist-p-of-vl-constint-atom-expandsizes.warnings

(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: vl-expr-p-of-vl-constint-atom-expandsizes.new-x

(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: warning-irrelevance-of-vl-constint-atom-expandsizes

(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: no-change-loserp-of-vl-constint-atom-expandsizes

(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: vl-expr-welltyped-p-of-vl-constint-atom-expandsizes

(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: vl-expr->finalwidth-of-vl-constint-atom-expandsizes

(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: vl-expr->finaltype-of-vl-constint-atom-expandsizes

(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: vl-constint-atom-expandsizes-of-vl-expr-fix-x

(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: vl-constint-atom-expandsizes-vl-expr-equiv-congruence-on-x

(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: vl-constint-atom-expandsizes-of-nfix-finalwidth

(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: vl-constint-atom-expandsizes-nat-equiv-congruence-on-finalwidth

(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: vl-constint-atom-expandsizes-of-vl-exprtype-fix-finaltype

(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: vl-constint-atom-expandsizes-vl-exprtype-equiv-congruence-on-finaltype

(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: vl-constint-atom-expandsizes-of-vl-context-fix-ctx

(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: vl-constint-atom-expandsizes-vl-context-equiv-congruence-on-ctx

(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: vl-constint-atom-expandsizes-of-vl-warninglist-fix-warnings

(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: vl-constint-atom-expandsizes-vl-warninglist-equiv-congruence-on-warnings

(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)