Main function for computing self-determined expression sizes.
(vl-binaryop-selfsize x left-size right-size ss scopes) → (mv warnings size)
We attempt to determine the size of the binary operator expression.
We assume that each argument has already had its self-size computed
successfully and that the results of these computations are given as the
This function basically implements Verilog-2005 Table 5-22, or SystemVerilog-2012 Table 11-21.
Function:
(defun vl-binaryop-selfsize (x left-size right-size ss scopes) (declare (xargs :guard (and (vl-expr-p x) (maybe-natp left-size) (maybe-natp right-size) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-expr-case x :vl-binary))) (let ((__function__ 'vl-binaryop-selfsize)) (declare (ignorable __function__)) (b* (((vl-binary x) (vl-expr-fix x)) (warnings nil) (left-size (maybe-natp-fix left-size)) (right-size (maybe-natp-fix right-size))) (case x.op ((: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* (((unless (and left-size right-size)) (mv (ok) 1)) (type (and (/= left-size right-size) (vl-tweak-fussy-warning-type :vl-fussy-size-warning-1 x.left x.right left-size right-size x.op ss scopes))) (warnings (if (not type) (ok) (warn :type type :msg "arguments to a ~s0 comparison operator have ~ different \"self-sizes\". The smaller argument ~ will be implicitly widened to match the larger ~ argument. Arguments:~% ~ - lhs (width ~x1): ~a3~% ~ - rhs (width ~x2): ~a4~%" :args (list (vl-binaryop-string (vl-binary->original-operator x)) left-size right-size x.left x.right))))) (mv (ok) 1))) ((:vl-binary-power :vl-binary-shl :vl-binary-shr :vl-binary-ashl :vl-binary-ashr) (mv (ok) left-size)) ((:vl-binary-plus :vl-binary-minus :vl-binary-times :vl-binary-div :vl-binary-rem) (mv (ok) (and left-size right-size (max left-size right-size)))) ((:vl-binary-bitand :vl-binary-bitor :vl-binary-xor :vl-binary-xnor) (b* (((unless (and left-size right-size)) (mv (ok) nil)) (max (max left-size right-size)) (type (and (/= left-size right-size) (vl-tweak-fussy-warning-type :vl-fussy-size-warning-2 x.left x.right left-size right-size x.op ss scopes))) (warnings (if (not type) (ok) (warn :type type :msg "arguments to a bitwise ~s0 operator have ~ different \"self-sizes\". The smaller argument ~ will be implicitly widened to match the larger ~ argument. Arguments:~% ~ - lhs (width ~x1): ~a3~% ~ - rhs (width ~x2): ~a4~%" :args (list (vl-binaryop-string (vl-binary->original-operator x)) left-size right-size x.left x.right x))))) (mv (ok) max))) ((: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) (mv (fatal :type :vl-programming-error :msg "vl-binaryop-selfsize should not encounter ~a0" :args (list x)) nil)) (otherwise (progn$ (impossible) (mv (ok) nil)))))))
Theorem:
(defthm vl-warninglist-p-of-vl-binaryop-selfsize.warnings (b* (((mv ?warnings ?size) (vl-binaryop-selfsize x left-size right-size ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm maybe-natp-of-vl-binaryop-selfsize.size (b* (((mv ?warnings ?size) (vl-binaryop-selfsize x left-size right-size ss scopes))) (maybe-natp size)) :rule-classes :type-prescription)
Theorem:
(defthm vl-binaryop-selfsize-of-vl-expr-fix-x (equal (vl-binaryop-selfsize (vl-expr-fix x) left-size right-size ss scopes) (vl-binaryop-selfsize x left-size right-size ss scopes)))
Theorem:
(defthm vl-binaryop-selfsize-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-binaryop-selfsize x left-size right-size ss scopes) (vl-binaryop-selfsize x-equiv left-size right-size ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-selfsize-of-maybe-natp-fix-left-size (equal (vl-binaryop-selfsize x (maybe-natp-fix left-size) right-size ss scopes) (vl-binaryop-selfsize x left-size right-size ss scopes)))
Theorem:
(defthm vl-binaryop-selfsize-maybe-nat-equiv-congruence-on-left-size (implies (acl2::maybe-nat-equiv left-size left-size-equiv) (equal (vl-binaryop-selfsize x left-size right-size ss scopes) (vl-binaryop-selfsize x left-size-equiv right-size ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-selfsize-of-maybe-natp-fix-right-size (equal (vl-binaryop-selfsize x left-size (maybe-natp-fix right-size) ss scopes) (vl-binaryop-selfsize x left-size right-size ss scopes)))
Theorem:
(defthm vl-binaryop-selfsize-maybe-nat-equiv-congruence-on-right-size (implies (acl2::maybe-nat-equiv right-size right-size-equiv) (equal (vl-binaryop-selfsize x left-size right-size ss scopes) (vl-binaryop-selfsize x left-size right-size-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-selfsize-of-vl-scopestack-fix-ss (equal (vl-binaryop-selfsize x left-size right-size (vl-scopestack-fix ss) scopes) (vl-binaryop-selfsize x left-size right-size ss scopes)))
Theorem:
(defthm vl-binaryop-selfsize-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-binaryop-selfsize x left-size right-size ss scopes) (vl-binaryop-selfsize x left-size right-size ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-selfsize-of-vl-elabscopes-fix-scopes (equal (vl-binaryop-selfsize x left-size right-size ss (vl-elabscopes-fix scopes)) (vl-binaryop-selfsize x left-size right-size ss scopes)))
Theorem:
(defthm vl-binaryop-selfsize-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-binaryop-selfsize x left-size right-size ss scopes) (vl-binaryop-selfsize x left-size right-size ss scopes-equiv))) :rule-classes :congruence)