• 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
              • 3vec-bit?
              • 3vec-?*
              • 3vec-?
              • 3vec-reduction-or
              • 3vec-reduction-and
              • 3vec-==
              • 3vec-bitxor
              • 3vec-bitor
              • 3vec-bitand
              • 3vec-bitnot
            • *svex-op-table*
          • 4vmask
          • Why-infinite-width
          • Svex-vars
          • Evaluation
          • Values
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Functions

3vec-operations

Core operations on 3vecs.

You can mostly think of these as utility functions for defining 4vec-operations. Many operations on 4vecs treat X and Z input bits the same. In these cases, for instance in 4vec-bitand, we typically define the 4vec operation to simply:

  • ``unfloating'' its inputs using 3vec-fix, and then
  • invoke a simpler 3vec operation on the unfloated inputs.

Subtopics

3vec-bit?
Bitwise multiple if-then-elses of 4vecs, with a 3vec test vector; doesn't unfloat then/else values.
3vec-?*
Atomic if-then-else of 4vecs, with a 3vec test. Has the property that when branches are equal, the result is equal to the branch, regardless of the test.
3vec-?
Atomic if-then-else of 4vecs, with a 3vec test; doesn't unfloat then/else values.
3vec-reduction-or
Reduction logical OR of a 3vec.
3vec-reduction-and
Reduction logical AND of a 3vec.
3vec-==
Bitwise equality of 3vecs.
3vec-bitxor
Bitwise logical XOR of 3vecs.
3vec-bitor
Bitwise logical OR of 3vecs.
3vec-bitand
Bitwise logical AND of 3vecs.
3vec-bitnot
Bitwise logical NOT of a 3vec.