		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-selfsize

Vl-unaryop-selfsize

Main function for computing self-determined expression sizes.

Signature
(vl-unaryop-selfsize x arg-size) → (mv warnings size)
Arguments: x — Guard (vl-expr-p x).; arg-size — Guard (maybe-natp arg-size).
Returns: warnings — Type (vl-warninglist-p warnings).; size — Type (maybe-natp 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 arg-sizes.

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

Definitions and Theorems

Function: vl-unaryop-selfsize

(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: vl-warninglist-p-of-vl-unaryop-selfsize.warnings

(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: maybe-natp-of-vl-unaryop-selfsize.size

(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: vl-unaryop-selfsize-of-vl-expr-fix-x

(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: vl-unaryop-selfsize-vl-expr-equiv-congruence-on-x

(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: vl-unaryop-selfsize-of-maybe-natp-fix-arg-size

(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: vl-unaryop-selfsize-maybe-nat-equiv-congruence-on-arg-size

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