		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-selfsize

Vl-op-selfsize

Main function for computing self-determined expression sizes.

Signature
(vl-op-selfsize op args arg-sizes context ctx warnings) → (mv warnings size)
Arguments: op — Guard (vl-op-p op).; args — Guard (vl-exprlist-p args).; arg-sizes — Guard (nat-listp arg-sizes).; context — Guard (vl-expr-p context).; ctx — Guard (vl-context-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; size — Type (maybe-natp size).

Warning: this function should typically only be called by the expression-sizing transform.

We attempt to determine the size of the expression formed by applying some operator, op, to some arguments, args. We assume that each argument has already had its self-size computed successfully and that the results of these computations are given as the arg-sizes.

The context is irrelevant and is only used to form better error messages; it is supposed to be the (sub) expression we are trying to size. The ctx is similarly irrelevant, and gives the broader context for this expression.

This function basically implements Verilog-2005 Table 5-22, or SystemVerilog-2012 Table 11-21. See expression-sizing.

Definitions and Theorems

Function: vl-op-selfsize

(defun vl-op-selfsize (op args arg-sizes context ctx warnings)
 (declare (xargs :guard (and (vl-op-p op)
                             (vl-exprlist-p args)
                             (nat-listp arg-sizes)
                             (vl-expr-p context)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (declare
      (xargs :guard (and (not (vl-atom-p context))
                         (or (not (vl-op-arity op))
                             (equal (len args) (vl-op-arity op)))
                         (same-lengthp args arg-sizes))))
 (let ((__function__ 'vl-op-selfsize))
  (declare (ignorable __function__))
  (b* ((op (vl-op-fix op))
       (args (vl-exprlist-fix args))
       (context (vl-expr-fix context))
       (ctx (vl-context-fix ctx)))
   (case
    (vl-op-fix op)
    ((:vl-bitselect :vl-unary-bitand
                    :vl-unary-nand :vl-unary-bitor
                    :vl-unary-nor :vl-unary-xor
                    :vl-unary-xnor :vl-unary-lognot
                    :vl-binary-logand :vl-binary-logor
                    :vl-implies :vl-equiv)
     (mv (ok) 1))
    ((:vl-binary-eq :vl-binary-neq
                    :vl-binary-ceq :vl-binary-cne
                    :vl-binary-lt :vl-binary-lte
                    :vl-binary-gt :vl-binary-gte
                    :vl-binary-wildeq :vl-binary-wildneq)
     (b*
      ((type (and (/= (first arg-sizes)
                      (second arg-sizes))
                  (vl-tweak-fussy-warning-type
                       :vl-fussy-size-warning-1 (first args)
                       (second args)
                       (first arg-sizes)
                       (second arg-sizes)
                       op)))
       (warnings
        (if (not type)
            (ok)
         (warn
          :type type
          :msg
          "~a0: arguments to a ~s1 comparison operator have ~
                             different \"self-sizes\".  The smaller argument ~
                             will be implicitly widened to match the larger ~
                             argument. Arguments:~%     ~
                               - lhs (width ~x2): ~a4~%     ~
                               - rhs (width ~x3): ~a5~%"
          :args
          (list
           ctx
           (vl-fancy-op-str (vl-nonatom->original-operator context))
           (first arg-sizes)
           (second arg-sizes)
           (first args)
           (second args))))))
      (mv (ok) 1)))
    ((:vl-binary-power :vl-unary-plus
                       :vl-unary-minus :vl-unary-bitnot
                       :vl-binary-shl :vl-binary-shr
                       :vl-binary-ashl :vl-binary-ashr)
     (mv (ok) (lnfix (first arg-sizes))))
    ((:vl-binary-plus :vl-binary-minus :vl-binary-times
                      :vl-binary-div :vl-binary-rem)
     (mv (ok)
         (max (lnfix (first arg-sizes))
              (lnfix (second arg-sizes)))))
    ((:vl-binary-bitand :vl-binary-bitor
                        :vl-binary-xor :vl-binary-xnor)
     (b*
      ((max (max (lnfix (first arg-sizes))
                 (lnfix (second arg-sizes))))
       (type (and (/= (first arg-sizes)
                      (second arg-sizes))
                  (vl-tweak-fussy-warning-type
                       :vl-fussy-size-warning-2 (first args)
                       (second args)
                       (first arg-sizes)
                       (second arg-sizes)
                       op)))
       (warnings
        (if (not type)
            (ok)
         (warn
          :type type
          :msg
          "~a0: arguments to a bitwise ~s1 operator have ~
                             different \"self-sizes\".  The smaller argument ~
                             will be implicitly widened to match the larger ~
                             argument. Arguments:~%     ~
                               - lhs (width ~x2): ~a4~%     ~
                               - rhs (width ~x3): ~a5~%"
          :args
          (list
           ctx
           (vl-fancy-op-str (vl-nonatom->original-operator context))
           (first arg-sizes)
           (second arg-sizes)
           (first args)
           (second args)
           context)))))
      (mv (ok) max)))
    ((:vl-qmark)
     (b*
      ((max (max (lnfix (second arg-sizes))
                 (lnfix (third arg-sizes))))
       (type (and (/= (second arg-sizes)
                      (third arg-sizes))
                  (vl-tweak-fussy-warning-type
                       :vl-fussy-size-warning-3 (second args)
                       (third args)
                       (second arg-sizes)
                       (third arg-sizes)
                       op)))
       (warnings
        (if (not type)
            (ok)
         (warn
          :type type
          :msg
          "~a0: branches of a ?: operator have different ~
                             \"self-sizes\".  The smaller branch will be ~
                             implicitly widened to match the larger branch. ~
                             Arguments:~%     ~
                               - Condition:               ~a1~%     ~
                               - True Branch  (size ~x2): ~a4~%     ~
                               - False Branch (size ~x3): ~a5~%"
          :args (list ctx (first args)
                      (second arg-sizes)
                      (third arg-sizes)
                      (second args)
                      (third args))))))
      (mv (ok) max)))
    ((:vl-concat)
     (mv (ok) (sum-nats arg-sizes)))
    ((:vl-multiconcat)
     (b*
      ((multiplicity (first args))
       (concat-width (lnfix (second arg-sizes)))
       ((unless (vl-expr-resolved-p multiplicity))
        (mv
         (fatal
          :type :vl-unresolved-multiplicity
          :msg
          "~a0: cannot size ~a1 because its multiplicity ~
                                has not been resolved."
          :args (list ctx context))
         nil))
       (size (* (vl-resolved->val multiplicity)
                concat-width)))
      (mv (ok) size)))
    ((:vl-partselect-colon)
     (b*
      ((left (second args))
       (right (third args))
       ((unless (and (vl-expr-resolved-p left)
                     (vl-expr-resolved-p right)))
        (mv
         (fatal
          :type :vl-unresolved-select
          :msg
          "~a0: cannot size ~a1 since it does not have ~
                                resolved indices."
          :args (list ctx context))
         nil))
       (left-val (vl-resolved->val left))
       (right-val (vl-resolved->val right))
       (size (+ 1 (abs (- left-val right-val)))))
      (mv (ok) size)))
    ((:vl-partselect-pluscolon :vl-partselect-minuscolon)
     (b*
      ((width-expr (second args))
       ((unless (and (vl-expr-resolved-p width-expr)
                     (> (vl-resolved->val width-expr) 0)))
        (mv
         (fatal
          :type :vl-unresolved-select
          :msg
          "~a0: cannot size ~a1 since its width expression ~
                                is not a resolved, positive constant."
          :args (list ctx context))
         nil))
       (size (vl-resolved->val width-expr)))
      (mv (ok) size)))
    ((:vl-mintypmax) (mv (ok) nil))
    ((:vl-stream-left :vl-stream-right
                      :vl-stream-left-sized :vl-stream-right-sized)
     (mv
      (warn
       :type :vl-untested-sizing-assumptions
       :msg
       "~a0: sizing of streaming concatenations is ~
                         experimental and may not be correct."
       :args (list ctx))
      (if (member op
                  '(:vl-stream-left-sized :vl-stream-right-sized))
          (sum-nats (mbe :logic (cdr arg-sizes)
                         :exec (and (consp arg-sizes)
                                    (cdr arg-sizes))))
        (sum-nats arg-sizes))))
    ((:vl-hid-dot :vl-index :vl-scope
                  :vl-syscall :vl-funcall
                  :vl-with-index :vl-with-colon
                  :vl-with-pluscolon :vl-with-minuscolon
                  :vl-tagged :vl-binary-cast
                  :vl-select-colon :vl-select-pluscolon
                  :vl-select-minuscolon :vl-pattern-multi
                  :vl-pattern-type :vl-pattern-positional
                  :vl-pattern-keyvalue :vl-keyvalue
                  :vl-unary-preinc :vl-unary-predec
                  :vl-unary-postinc :vl-unary-postdec
                  :vl-binary-assign :vl-binary-plusassign
                  :vl-binary-minusassign :vl-binary-timesassign
                  :vl-binary-divassign :vl-binary-remassign
                  :vl-binary-andassign :vl-binary-orassign
                  :vl-binary-xorassign :vl-binary-shlassign
                  :vl-binary-shrassign :vl-binary-ashlassign
                  :vl-binary-ashrassign :vl-inside
                  :vl-valuerange :vl-valuerangelist)
     (mv (fatal :type :vl-programming-error
                :msg "~a0: vl-op-selfsize should not encounter ~a1"
                :args (list ctx context))
         nil))
    (otherwise (progn$ (impossible) (mv (ok) nil)))))))

Theorem: vl-warninglist-p-of-vl-op-selfsize.warnings

(defthm vl-warninglist-p-of-vl-op-selfsize.warnings
  (b* (((mv ?warnings ?size)
        (vl-op-selfsize op
                        args arg-sizes context ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-vl-op-selfsize.size

(defthm maybe-natp-of-vl-op-selfsize.size
  (b* (((mv ?warnings ?size)
        (vl-op-selfsize op
                        args arg-sizes context ctx warnings)))
    (maybe-natp size))
  :rule-classes :type-prescription)

Theorem: warning-irrelevance-of-vl-op-selfsize

(defthm warning-irrelevance-of-vl-op-selfsize
  (let
     ((ret1 (vl-op-selfsize op args arg-sizes context ctx warnings))
      (ret2 (vl-op-selfsize op args arg-sizes context nil nil)))
    (implies (syntaxp (not (and (equal ctx ''nil)
                                (equal warnings ''nil))))
             (equal (mv-nth 1 ret1)
                    (mv-nth 1 ret2)))))

Theorem: vl-op-selfsize-of-vl-op-fix-op

(defthm vl-op-selfsize-of-vl-op-fix-op
  (equal (vl-op-selfsize (vl-op-fix op)
                         args arg-sizes context ctx warnings)
         (vl-op-selfsize op
                         args arg-sizes context ctx warnings)))

Theorem: vl-op-selfsize-vl-op-equiv-congruence-on-op

(defthm vl-op-selfsize-vl-op-equiv-congruence-on-op
 (implies
      (vl-op-equiv op op-equiv)
      (equal (vl-op-selfsize op args arg-sizes context ctx warnings)
             (vl-op-selfsize op-equiv
                             args arg-sizes context ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-op-selfsize-of-vl-exprlist-fix-args

(defthm vl-op-selfsize-of-vl-exprlist-fix-args
  (equal (vl-op-selfsize op (vl-exprlist-fix args)
                         arg-sizes context ctx warnings)
         (vl-op-selfsize op
                         args arg-sizes context ctx warnings)))

Theorem: vl-op-selfsize-vl-exprlist-equiv-congruence-on-args

(defthm vl-op-selfsize-vl-exprlist-equiv-congruence-on-args
 (implies
      (vl-exprlist-equiv args args-equiv)
      (equal (vl-op-selfsize op args arg-sizes context ctx warnings)
             (vl-op-selfsize op args-equiv
                             arg-sizes context ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-op-selfsize-of-vl-expr-fix-context

(defthm vl-op-selfsize-of-vl-expr-fix-context
  (equal (vl-op-selfsize op args arg-sizes (vl-expr-fix context)
                         ctx warnings)
         (vl-op-selfsize op
                         args arg-sizes context ctx warnings)))

Theorem: vl-op-selfsize-vl-expr-equiv-congruence-on-context

(defthm vl-op-selfsize-vl-expr-equiv-congruence-on-context
 (implies
      (vl-expr-equiv context context-equiv)
      (equal (vl-op-selfsize op args arg-sizes context ctx warnings)
             (vl-op-selfsize op args
                             arg-sizes context-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-op-selfsize-of-vl-context-fix-ctx

(defthm vl-op-selfsize-of-vl-context-fix-ctx
  (equal (vl-op-selfsize op args
                         arg-sizes context (vl-context-fix ctx)
                         warnings)
         (vl-op-selfsize op
                         args arg-sizes context ctx warnings)))

Theorem: vl-op-selfsize-vl-context-equiv-congruence-on-ctx

(defthm vl-op-selfsize-vl-context-equiv-congruence-on-ctx
 (implies
      (vl-context-equiv ctx ctx-equiv)
      (equal (vl-op-selfsize op args arg-sizes context ctx warnings)
             (vl-op-selfsize op args
                             arg-sizes context ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-op-selfsize-of-vl-warninglist-fix-warnings

(defthm vl-op-selfsize-of-vl-warninglist-fix-warnings
  (equal (vl-op-selfsize op args arg-sizes context
                         ctx (vl-warninglist-fix warnings))
         (vl-op-selfsize op
                         args arg-sizes context ctx warnings)))

Theorem: vl-op-selfsize-vl-warninglist-equiv-congruence-on-warnings

(defthm vl-op-selfsize-vl-warninglist-equiv-congruence-on-warnings
 (implies
      (vl-warninglist-equiv warnings warnings-equiv)
      (equal (vl-op-selfsize op args arg-sizes context ctx warnings)
             (vl-op-selfsize op args
                             arg-sizes context ctx warnings-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-tweak-fussy-warning-type: Heuristically categorize fussy warnings according to severity.