• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
            • Sv::vl-expr.lisp
              • Vl-scopecontext-to-addr
              • Vl-binaryop-to-svex
              • Vl-expr-to-svex-maybe-typed
              • Vl-datatype-syscall-to-svex
              • Vl-operandinfo-to-svex-preproc
              • Vl-structmemberlist->types
              • Vl-seltrace-to-svex-select
              • Vl-portdecllist->types
              • Vl-operandinfo-to-svex-select
              • Vl-plusminus-partselect->svex
              • Vl-arrayrange->rel-lsb-and-width
              • Vl-unaryop-to-svex
              • Vl-funcall-args-to-ordered
              • Vl-expr-to-svex-lhs
              • Vl-operandinfo-to-svex
              • Vl-array-assignpat-keyval-resolve
              • Vl-err->vfatal
              • Vl-datatypelist-usertype-resolve
              • Vl-upscope-to-svex-upscope
              • Vl-err->fatal
              • Vl-streaming-concat-trunc/extend
              • Vl-operandinfo-base-svar
              • Vl-index-shift-amount
              • Vttree->constraints
              • Vl-slicesize-resolve
              • Vl-function-map-find-matching-aux
              • Vl-funname-lookup
              • Vl-datatype-size-warn
              • Svex-repeat-aux
              • Vl-$test$plusargs-to-svex
              • Svex-extend
              • Vl-structmemberlist-shift-bits
              • Vl-datatype-slot-width/range
              • Vl-datatype-index-shift-amount
              • Vl-datatype-field-shift-amount
              • 4vec-extend
              • Vl-function-pair-inputs-with-actuals
              • Vl-expr-to-svex-untyped
              • Vl-function-map-check-matching
              • Vl-datatype-syscall-remove-dims
              • Svex-concat-list-aux
              • Vttree-add-constraints
              • Vttree-add-warnings
              • Vl-check-struct-assignpat-keys
              • Vl-check-array-assignpat-keys
              • Sv::constraintlist-subst-memo
              • Vl-svex-keyval-index-lookup
              • Vl-function-map-find-matching
              • Vl-convert-dollarsign-to-expr
              • Vttree->constraints-acc
              • Vl-seltrace-type
              • Vl-seltrace-to-path
              • Vl-keyval-member-lookup
              • Svex-repeat
              • Vttree->warnings-acc
              • Vl-trunc/extend-type-err
              • Constraintlist-add-ctx
              • Vl-hidtrace-add-to-path
              • Svex-multiconcat
              • Vttree-join
              • Vl-value-to-string-aux
              • Vl-seltrace-add-to-path
              • Vl-value-to-4vec
              • Vl-expr-to-svex-selfdet
              • Vl-svex-keyval-default-lookup
              • Vl-$test$plusargs-p
              • Vl-value-to-svex
              • Vl-value-in-range
              • Vl-keyval-default-lookup
              • Sv::svexlist-args-extract-constants
              • Vl-string->bits
              • Vl-size-to-unsigned-logic
              • Vl-hidtrace-to-path
              • Svex-concat-list
              • Vttree->warnings
              • Vl-seltrace-unres-count
              • Vl-datatype-index-is-bitselect
              • Vl-bitlist->4vec
              • Vl-svex-keyvallist-vars
              • Vl-hidstep->svex-index
              • Vl-selstep->svex-name
              • Vl-datatypelist-resolved-p
              • Vl-datatype-$unpacked_dimensions
              • Vl-datatype-$dimensions
              • Vl-bitlist->offset
              • Vl-bitlist->onset
              • Vl-streamexprlist-has-with
              • Vl-hidstep-resolved-p
              • Vl-expr-needs-type-context
              • Vl-streamexprlist->exprs
              • Vl-integer-to-string
              • Vl-hidtrace-resolved-p
              • Vl-selstep-resolved-p
              • Vl-select-resolved-p
              • Vl-svex-keyvallist
              • Vl-datatypelist
              • Svex-x
            • Vttree
          • Vl-design->svex-modalist
          • Vl-svstmt
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sv::vl-expr.lisp

Vl-binaryop-to-svex

Signature

(vl-binaryop-to-svex op left right 
                     left-size right-size size signedness) 
 
  → 
(mv err svex)

Arguments

op — Guard (vl-binaryop-p op).

left — Guard (sv::svex-p left).

right — Guard (sv::svex-p right).

left-size — Guard (natp left-size).

right-size — Guard (natp right-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-binaryop-to-svex

(defun vl-binaryop-to-svex (op left right
                               left-size right-size size signedness)
 (declare (xargs :guard (and (vl-binaryop-p op)
                             (sv::svex-p left)
                             (sv::svex-p right)
                             (natp left-size)
                             (natp right-size)
                             (natp size)
                             (vl-exprsign-p signedness))))
 (declare (ignorable right-size))
 (let ((__function__ 'vl-binaryop-to-svex))
  (declare (ignorable __function__))
  (b*
   ((op (vl-binaryop-fix op))
    (body
     (case
      op
      (:vl-binary-plus (sv::svcall + left right))
      (:vl-binary-minus (sv::svcall sv::b- left right))
      (:vl-binary-times (sv::svcall * left right))
      (:vl-binary-div (sv::svcall / left right))
      (:vl-binary-rem (sv::svcall sv::% left right))
      (:vl-binary-eq (sv::svcall sv::== left right))
      (:vl-binary-neq (sv::svcall sv::bitnot
                                  (sv::svcall sv::== left right)))
      (:vl-binary-ceq (sv::svcall sv::=== left right))
      (:vl-binary-cne (sv::svcall sv::bitnot
                                  (sv::svcall sv::=== left right)))
      (:vl-binary-wildeq (sv::svcall sv::==? left right))
      (:vl-binary-wildneq
           (sv::svcall sv::bitnot
                       (sv::svcall sv::==? left right)))
      (:vl-binary-logand
           (sv::svcall sv::bitand (sv::svcall sv::uor left)
                       (sv::svcall sv::uor right)))
      (:vl-binary-logor
           (sv::svcall sv::bitor (sv::svcall sv::uor left)
                       (sv::svcall sv::uor right)))
      (:vl-binary-lt (sv::svcall < left right))
      (:vl-binary-lte
           (sv::svcall sv::bitnot (sv::svcall < right left)))
      (:vl-binary-gt (sv::svcall < right left))
      (:vl-binary-gte
           (sv::svcall sv::bitnot (sv::svcall < left right)))
      (:vl-binary-bitand (sv::svcall sv::bitand left right))
      (:vl-binary-bitor (sv::svcall sv::bitor left right))
      (:vl-binary-xor (sv::svcall sv::bitxor left right))
      (:vl-binary-xnor
           (sv::svcall sv::bitnot
                       (sv::svcall sv::bitxor left right)))
      (:vl-binary-power (sv::svcall sv::pow left right))
      (:vl-binary-shr (sv::svcall sv::rsh
                                  (sv::svex-zerox right-size right)
                                  (sv::svex-zerox left-size left)))
      (:vl-binary-shl (sv::svcall sv::lsh
                                  (sv::svex-zerox right-size right)
                                  left))
      (:vl-binary-ashr (sv::svcall sv::rsh
                                   (sv::svex-zerox right-size right)
                                   left))
      (:vl-binary-ashl (sv::svcall sv::lsh
                                   (sv::svex-zerox right-size right)
                                   left))
      (:vl-implies
       (sv::svcall sv::bitor
                   (sv::svcall sv::bitnot (sv::svcall sv::uor left))
                   (sv::svcall sv::uor right)))
      (:vl-equiv
        (sv::svcall sv::bitnot
                    (sv::svcall sv::bitxor (sv::svcall sv::uor left)
                                (sv::svcall sv::uor right))))
      (otherwise nil))))
   (mv (and (not body)
            (vmsg "Operator not implemented: ~s0"
                  (vl-binaryop-string op)))
       (if body (svex-extend signedness size body)
         (svex-x))))))

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

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

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

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

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

(defthm vars-of-vl-binaryop-to-svex
  (b* (((mv ?err ?svex)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))
    (implies (and (not (member v (sv::svex-vars left)))
                  (not (member v (sv::svex-vars right))))
             (not (member v (sv::svex-vars svex))))))

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

(defthm vl-binaryop-to-svex-of-vl-binaryop-fix-op
 (equal (vl-binaryop-to-svex (vl-binaryop-fix op)
                             left right
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

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

(defthm vl-binaryop-to-svex-vl-binaryop-equiv-congruence-on-op
 (implies
   (vl-binaryop-equiv op op-equiv)
   (equal
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op-equiv left right
                             left-size right-size size signedness)))
 :rule-classes :congruence)

Theorem: vl-binaryop-to-svex-of-svex-fix-left

(defthm vl-binaryop-to-svex-of-svex-fix-left
 (equal (vl-binaryop-to-svex op (sv::svex-fix left)
                             right
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

Theorem: vl-binaryop-to-svex-svex-equiv-congruence-on-left

(defthm vl-binaryop-to-svex-svex-equiv-congruence-on-left
 (implies
   (sv::svex-equiv left left-equiv)
   (equal
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op left-equiv right
                             left-size right-size size signedness)))
 :rule-classes :congruence)

Theorem: vl-binaryop-to-svex-of-svex-fix-right

(defthm vl-binaryop-to-svex-of-svex-fix-right
 (equal (vl-binaryop-to-svex op left (sv::svex-fix right)
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

Theorem: vl-binaryop-to-svex-svex-equiv-congruence-on-right

(defthm vl-binaryop-to-svex-svex-equiv-congruence-on-right
 (implies
   (sv::svex-equiv right right-equiv)
   (equal
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)
        (vl-binaryop-to-svex op left right-equiv
                             left-size right-size size signedness)))
 :rule-classes :congruence)

Theorem: vl-binaryop-to-svex-of-nfix-left-size

(defthm vl-binaryop-to-svex-of-nfix-left-size
 (equal (vl-binaryop-to-svex op left right (nfix left-size)
                             right-size size signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

Theorem: vl-binaryop-to-svex-nat-equiv-congruence-on-left-size

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

Theorem: vl-binaryop-to-svex-of-nfix-right-size

(defthm vl-binaryop-to-svex-of-nfix-right-size
 (equal (vl-binaryop-to-svex op
                             left right left-size (nfix right-size)
                             size signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

Theorem: vl-binaryop-to-svex-nat-equiv-congruence-on-right-size

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

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

(defthm vl-binaryop-to-svex-of-nfix-size
 (equal (vl-binaryop-to-svex op left
                             right left-size right-size (nfix size)
                             signedness)
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

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

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

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

(defthm vl-binaryop-to-svex-of-vl-exprsign-fix-signedness
 (equal (vl-binaryop-to-svex op left right left-size right-size
                             size (vl-exprsign-fix signedness))
        (vl-binaryop-to-svex op left right
                             left-size right-size size signedness)))

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

(defthm
     vl-binaryop-to-svex-vl-exprsign-equiv-congruence-on-signedness
 (implies
   (vl-exprsign-equiv signedness signedness-equiv)
   (equal (vl-binaryop-to-svex op left right
                               left-size right-size size signedness)
          (vl-binaryop-to-svex op left right left-size
                               right-size size signedness-equiv)))
 :rule-classes :congruence)