Main function for computing self-determined expression sizes.
(vl-op-selfsize op args arg-sizes context ctx warnings) → (mv warnings 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,
The
This function basically implements Verilog-2005 Table 5-22, or SystemVerilog-2012 Table 11-21. See expression-sizing.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)