		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-binaryop-precedence

Signature
(vl-binaryop-precedence x) → precedence
Arguments: x — Guard (vl-binaryop-p x).
Returns: precedence — Type (posp precedence).

Definitions and Theorems

Function: vl-binaryop-precedence

(defun vl-binaryop-precedence (x)
  (declare (xargs :guard (vl-binaryop-p x)))
  (let ((__function__ 'vl-binaryop-precedence))
    (declare (ignorable __function__))
    (case (vl-binaryop-fix x)
          (:vl-binary-power 140)
          (:vl-binary-times 130)
          (:vl-binary-div 130)
          (:vl-binary-rem 130)
          (:vl-binary-plus 120)
          (:vl-binary-minus 120)
          (:vl-binary-shr 110)
          (:vl-binary-shl 110)
          (:vl-binary-ashr 110)
          (:vl-binary-ashl 110)
          (:vl-binary-lt 100)
          (:vl-binary-lte 100)
          (:vl-binary-gt 100)
          (:vl-binary-gte 100)
          (:vl-inside 100)
          (:vl-binary-eq 90)
          (:vl-binary-neq 90)
          (:vl-binary-ceq 90)
          (:vl-binary-cne 90)
          (:vl-binary-wildeq 90)
          (:vl-binary-wildneq 90)
          (:vl-binary-bitand 80)
          (:vl-binary-xor 70)
          (:vl-binary-xnor 70)
          (:vl-binary-bitor 60)
          (:vl-binary-logand 50)
          (:vl-binary-logor 40)
          (:vl-implies 20)
          (:vl-equiv 20)
          (:vl-binary-assign 10)
          (:vl-binary-plusassign 10)
          (:vl-binary-minusassign 10)
          (:vl-binary-timesassign 10)
          (:vl-binary-divassign 10)
          (:vl-binary-remassign 10)
          (:vl-binary-andassign 10)
          (:vl-binary-orassign 10)
          (:vl-binary-xorassign 10)
          (:vl-binary-shlassign 10)
          (:vl-binary-shrassign 10)
          (:vl-binary-ashlassign 10)
          (:vl-binary-ashrassign 10)
          (otherwise (impossible)))))

Theorem: posp-of-vl-binaryop-precedence

(defthm posp-of-vl-binaryop-precedence
  (b* ((precedence (vl-binaryop-precedence x)))
    (posp precedence))
  :rule-classes :type-prescription)

Theorem: vl-binaryop-precedence-of-vl-binaryop-fix-x

(defthm vl-binaryop-precedence-of-vl-binaryop-fix-x
  (equal (vl-binaryop-precedence (vl-binaryop-fix x))
         (vl-binaryop-precedence x)))

Theorem: vl-binaryop-precedence-vl-binaryop-equiv-congruence-on-x

(defthm vl-binaryop-precedence-vl-binaryop-equiv-congruence-on-x
  (implies (vl-binaryop-equiv x x-equiv)
           (equal (vl-binaryop-precedence x)
                  (vl-binaryop-precedence x-equiv)))
  :rule-classes :congruence)