		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-unaryop-to-svex

Signature
(vl-unaryop-to-svex op arg arg-size size signedness) → (mv err svex)
Arguments: op — Guard (vl-unaryop-p op).; arg — Guard (sv::svex-p arg).; arg-size — Guard (natp arg-size).; size — Guard (natp size).; signedness — Guard (vl-exprsign-p signedness).
Returns: err — Type (iff (vl-msg-p err) err).; svex — Type (sv::svex-p svex).

Definitions and Theorems

Function: vl-unaryop-to-svex

(defun vl-unaryop-to-svex (op arg arg-size size signedness)
 (declare (xargs :guard (and (vl-unaryop-p op)
                             (sv::svex-p arg)
                             (natp arg-size)
                             (natp size)
                             (vl-exprsign-p signedness))))
 (let ((__function__ 'vl-unaryop-to-svex))
  (declare (ignorable __function__))
  (b*
   ((op (vl-unaryop-fix op))
    (body
     (case
      op
      (:vl-unary-plus (sv::svcall sv::xdet arg))
      (:vl-unary-minus (sv::svcall sv::u- arg))
      (:vl-unary-bitnot (sv::svcall sv::bitnot arg))
      (:vl-unary-lognot
           (sv::svcall sv::bitnot (sv::svcall sv::uor arg)))
      (:vl-unary-bitand
           (sv::svcall sv::uand (sv::svex-signx arg-size arg)))
      (:vl-unary-nand
           (sv::svcall sv::bitnot
                       (sv::svcall sv::uand
                                   (sv::svex-signx arg-size arg))))
      (:vl-unary-bitor (sv::svcall sv::uor arg))
      (:vl-unary-nor
           (sv::svcall sv::bitnot (sv::svcall sv::uor arg)))
      (:vl-unary-xor
           (sv::svcall sv::uxor (sv::svex-zerox arg-size arg)))
      (:vl-unary-xnor
         (sv::svcall sv::bitnot
                     (sv::svcall sv::uxor
                                 (sv::svex-zerox arg-size arg)))))))
   (mv (and (not body)
            (vmsg "Operator not implemented: ~s0"
                  (vl-unaryop-string op)))
       (if body (svex-extend signedness size body)
         (svex-x))))))

Theorem: return-type-of-vl-unaryop-to-svex.err

(defthm return-type-of-vl-unaryop-to-svex.err
  (b* (((mv ?err ?svex)
        (vl-unaryop-to-svex op arg arg-size size signedness)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: svex-p-of-vl-unaryop-to-svex.svex

(defthm svex-p-of-vl-unaryop-to-svex.svex
  (b* (((mv ?err ?svex)
        (vl-unaryop-to-svex op arg arg-size size signedness)))
    (sv::svex-p svex))
  :rule-classes :rewrite)

Theorem: vars-of-vl-unaryop-to-svex

(defthm vars-of-vl-unaryop-to-svex
  (b* (((mv ?err ?svex)
        (vl-unaryop-to-svex op arg arg-size size signedness)))
    (implies (not (member v (sv::svex-vars arg)))
             (not (member v (sv::svex-vars svex))))))

Theorem: vl-unaryop-to-svex-of-vl-unaryop-fix-op

(defthm vl-unaryop-to-svex-of-vl-unaryop-fix-op
  (equal (vl-unaryop-to-svex (vl-unaryop-fix op)
                             arg arg-size size signedness)
         (vl-unaryop-to-svex op arg arg-size size signedness)))

Theorem: vl-unaryop-to-svex-vl-unaryop-equiv-congruence-on-op

(defthm vl-unaryop-to-svex-vl-unaryop-equiv-congruence-on-op
 (implies
   (vl-unaryop-equiv op op-equiv)
   (equal
        (vl-unaryop-to-svex op arg arg-size size signedness)
        (vl-unaryop-to-svex op-equiv arg arg-size size signedness)))
 :rule-classes :congruence)

Theorem: vl-unaryop-to-svex-of-svex-fix-arg

(defthm vl-unaryop-to-svex-of-svex-fix-arg
  (equal (vl-unaryop-to-svex op (sv::svex-fix arg)
                             arg-size size signedness)
         (vl-unaryop-to-svex op arg arg-size size signedness)))

Theorem: vl-unaryop-to-svex-svex-equiv-congruence-on-arg

(defthm vl-unaryop-to-svex-svex-equiv-congruence-on-arg
 (implies
   (sv::svex-equiv arg arg-equiv)
   (equal
        (vl-unaryop-to-svex op arg arg-size size signedness)
        (vl-unaryop-to-svex op arg-equiv arg-size size signedness)))
 :rule-classes :congruence)

Theorem: vl-unaryop-to-svex-of-nfix-arg-size

(defthm vl-unaryop-to-svex-of-nfix-arg-size
  (equal (vl-unaryop-to-svex op arg (nfix arg-size)
                             size signedness)
         (vl-unaryop-to-svex op arg arg-size size signedness)))

Theorem: vl-unaryop-to-svex-nat-equiv-congruence-on-arg-size

(defthm vl-unaryop-to-svex-nat-equiv-congruence-on-arg-size
 (implies
   (acl2::nat-equiv arg-size arg-size-equiv)
   (equal
        (vl-unaryop-to-svex op arg arg-size size signedness)
        (vl-unaryop-to-svex op arg arg-size-equiv size signedness)))
 :rule-classes :congruence)

Theorem: vl-unaryop-to-svex-of-nfix-size

(defthm vl-unaryop-to-svex-of-nfix-size
  (equal (vl-unaryop-to-svex op arg arg-size (nfix size)
                             signedness)
         (vl-unaryop-to-svex op arg arg-size size signedness)))

Theorem: vl-unaryop-to-svex-nat-equiv-congruence-on-size

(defthm vl-unaryop-to-svex-nat-equiv-congruence-on-size
 (implies
   (acl2::nat-equiv size size-equiv)
   (equal
        (vl-unaryop-to-svex op arg arg-size size signedness)
        (vl-unaryop-to-svex op arg arg-size size-equiv signedness)))
 :rule-classes :congruence)

Theorem: vl-unaryop-to-svex-of-vl-exprsign-fix-signedness

(defthm vl-unaryop-to-svex-of-vl-exprsign-fix-signedness
  (equal (vl-unaryop-to-svex op arg arg-size
                             size (vl-exprsign-fix signedness))
         (vl-unaryop-to-svex op arg arg-size size signedness)))

Theorem: vl-unaryop-to-svex-vl-exprsign-equiv-congruence-on-signedness

(defthm
      vl-unaryop-to-svex-vl-exprsign-equiv-congruence-on-signedness
 (implies
   (vl-exprsign-equiv signedness signedness-equiv)
   (equal
        (vl-unaryop-to-svex op arg arg-size size signedness)
        (vl-unaryop-to-svex op arg arg-size size signedness-equiv)))
 :rule-classes :congruence)