• 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
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
          • 4vec-operations
          • 3vec-operations
          • *svex-op-table*
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Functions

*svex-op-table*

Raw table about the known svex functions.

Definition: *svex-op-table*

(defconst *svex-op-table*
 '((id 4vec-fix (x) "identity function")
   (bitsel 4vec-bit-extract (index x)
           "bit select")
   (unfloat 3vec-fix (x)
            "change Z bits to Xes")
   (bitnot 4vec-bitnot (x)
           "bitwise negation")
   (bitand 4vec-bitand (x y) "bitwise AND")
   (bitor 4vec-bitor (x y) "bitwise OR")
   (bitxor 4vec-bitxor (x y) "bitwise XOR")
   (res 4vec-res (x y)
        "resolve (short together)")
   (resand 4vec-resand (x y)
           "resolve wired AND")
   (resor 4vec-resor (x y)
          "resolve wired OR")
   (override 4vec-override (x y)
             "resolve different strengths")
   (onp 4vec-onset (x)
        "identity, except Z becomes 0")
   (offp 4vec-offset (x)
         "negation, except Z becomes 0")
   (uand 4vec-reduction-and (x)
         "unary (reduction) AND")
   (uor 4vec-reduction-or (x)
        "unary (reduction) OR")
   (uxor 4vec-parity (x)
         "reduction XOR, i.e. parity")
   (zerox 4vec-zero-ext (width x)
          "zero extend")
   (signx 4vec-sign-ext (width x)
          "sign extend")
   (concat 4vec-concat (width x y)
           "concatenate at a given bit width")
   (blkrev 4vec-rev-blocks (width bsz x)
           "reverse order of blocks")
   (rsh 4vec-rsh (shift x) "right shift")
   (lsh 4vec-lsh (shift x) "left shift")
   (+ 4vec-plus (x y) "addition")
   (b- 4vec-minus (x y) "subtraction")
   (u- 4vec-uminus (x) "unary minus")
   (* 4vec-times (x y) "multiplication")
   (/ 4vec-quotient (x y) "division")
   (% 4vec-remainder (x y) "modulus")
   (xdet 4vec-xdet (x)
         "identity on binary vectors, else X")
   (countones 4vec-countones (x)
              "count of 1-bits")
   (onehot 4vec-onehot (x) "one-hot check")
   (onehot0 4vec-onehot0 (x)
            "one-hot check (0-hot allowed)")
   (< 4vec-< (x y) "less than")
   (== 4vec-== (x y) "equality")
   (=== 4vec-=== (x y)
        "case equality (scary verilog semantics)")
   (===* 4vec-===* (x y)
         "modified case equality (x-monotonic if y is constant)")
   (==? 4vec-wildeq (x y)
        "wildcard equality (scary verilog semantics)")
   (safer-==? 4vec-wildeq-safe (x y)
              "wildcard equality (X-monotonic version)")
   (==?? 4vec-symwildeq (x y)
         "wildcard equality for casez")
   (clog2 4vec-clog2 (x) "ceiling of log2")
   (pow 4vec-pow (x y) "exponentiation")
   (? 4vec-? (test then else)
      "if-then-else")
   (?* 4vec-?* (test then else)
       "if-then-else (for statements)")
   (bit? 4vec-bit? (test then else)
         "bitwise if-then-else")
   (bit?!
      4vec-bit?! (test then else)
      "bitwise if-then-else, only chooses then[i] when test[i]===1")
   (?!
    4vec-?! (test then else)
    "procedural if-then-else, only chooses then when test has a definite 1 bit")
   (partsel 4vec-part-select (lsb width in)
            "part select")
   (partinst 4vec-part-install (lsb width in val)
             "part install")))