Main function for computing self-determined expression sizes.
(vl-unaryop-selfsize x arg-size) → (mv warnings size)
We attempt to determine the size of the unary 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-unaryop-selfsize (x arg-size) (declare (xargs :guard (and (vl-expr-p x) (maybe-natp arg-size)))) (declare (xargs :guard (vl-expr-case x :vl-unary))) (let ((__function__ 'vl-unaryop-selfsize)) (declare (ignorable __function__)) (b* (((vl-unary x) (vl-expr-fix x)) (arg-size (maybe-natp-fix arg-size)) (warnings nil)) (case x.op ((:vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor :vl-unary-lognot) (mv (ok) 1)) ((:vl-unary-plus :vl-unary-minus :vl-unary-bitnot) (mv (ok) arg-size)) ((:vl-unary-preinc :vl-unary-predec :vl-unary-postinc :vl-unary-postdec) (mv (fatal :type :vl-programming-error :msg "vl-op-selfsize should not encounter ~a0" :args (list x)) nil)) (otherwise (progn$ (impossible) (mv (ok) nil)))))))
Theorem:
(defthm vl-warninglist-p-of-vl-unaryop-selfsize.warnings (b* (((mv ?warnings ?size) (vl-unaryop-selfsize x arg-size))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm maybe-natp-of-vl-unaryop-selfsize.size (b* (((mv ?warnings ?size) (vl-unaryop-selfsize x arg-size))) (maybe-natp size)) :rule-classes :type-prescription)
Theorem:
(defthm vl-unaryop-selfsize-of-vl-expr-fix-x (equal (vl-unaryop-selfsize (vl-expr-fix x) arg-size) (vl-unaryop-selfsize x arg-size)))
Theorem:
(defthm vl-unaryop-selfsize-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-unaryop-selfsize x arg-size) (vl-unaryop-selfsize x-equiv arg-size))) :rule-classes :congruence)
Theorem:
(defthm vl-unaryop-selfsize-of-maybe-natp-fix-arg-size (equal (vl-unaryop-selfsize x (maybe-natp-fix arg-size)) (vl-unaryop-selfsize x arg-size)))
Theorem:
(defthm vl-unaryop-selfsize-maybe-nat-equiv-congruence-on-arg-size (implies (acl2::maybe-nat-equiv arg-size arg-size-equiv) (equal (vl-unaryop-selfsize x arg-size) (vl-unaryop-selfsize x arg-size-equiv))) :rule-classes :congruence)