• 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
          • 4vmask
          • Why-infinite-width
          • Svex-vars
          • Evaluation
          • Values
            • 4vec
              • 4vec-operations
              • 4vec-p
              • S4vecs
                • S4vec-p
                • S4vec-part-install
                • S4vec-?!
                • S4vec-fix
                • S4vec-rev-blocks
                • Sparseint-rev-blocks
                • S4vec-part-select
                • S3vec-bit?
                • S4vec-concat
                • S4vec-bitmux
                • S4vec-bit?!
                • S3vec-?*
                • S3vec-?
                • Svex-s4apply
                • S4vec-bit?
                • S4vec-?*
                • S4vec-?
                • S4vec-===*
                • S4vec-pow
                • S4vec
                • S4vec-sign-ext
                • S4vec-override
                • S4vec-zero-ext
                • S4vec-wildeq-safe
                • S4vec-symwildeq
                • S4vec-shift-core
                • S4vec-remainder
                • S4vec-quotient
                • S4vec-bitxor
                • S3vec-bitxor
                • S4vec-resor
                • S4vec-resand
                • S4vec-bit-index
                • S4vec-bit-extract
                • S3vec-bitor
                • S3vec-bitand
                • S4vec->4vec
                • S4vec-wildeq
                • S4vec-times
                • S4vec-rsh
                • S4vec-plus
                • S4vec-minus
                • S4vec-bitand
                • S4vec-===
                • S4vec-<
                • S4vec-res
                • S4vec-lsh
                • S4vec-bitor
                • S4vec-==
                • S3vec-==
                • S4vec-equal
                • S3vec-reduction-or
                • S3vec-reduction-and
                • S4vec-sparseint-val
                • S4vec-parity
                • S4vec-countones
                • S2vec
                • S4vec-reduction-or
                • S4vec-reduction-and
                • S4vec-onehot0
                • S4vec-onehot
                • S4vec-offset
                • S3vec-bitnot
                • 4vec->s4vec
                • S4vec-xdet
                • S4vec-uminus
                • S4vec-onset
                • S4vec-clog2
                • S4vec-bitnot
                • S4vec-1mask
                • S3vec-fix
                • S4vec->upper
                • S4vec->lower
                • S4vec-index-p
                • S4veclist
                • S4vec-xfree-p
                • S4vec-2vec-p
                • S3vec-p
                • S2vec->val
                • S2vec-p
                • S4vec-correct-fn
                • S4vec-correct-formal-evals
              • 4vec-examples
              • Maybe-4vec
              • 4vec-equiv
              • Make-4vec
              • 4vec->upper
              • 4vec->lower
              • 4veclist
              • 4vec-fix
              • Make-honsed-4vec
              • 4vec-index-p
            • 4vec-<<=
            • 3vec
            • 2vec
            • 2vecx
            • 2vecnatx
            • 4vec-x
            • 4vec-1x
            • 4vec-1z
            • 4vec-z
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • 4vec

S4vecs

Representation of 4vecs using sparseint rather than bignum elements.

Subtopics

S4vec-p
S4vec-part-install
S4vec-?!
If-then-elses of s4vecs following the SystemVerilog semantics for procedural conditional branches, i.e. if the test has any bit that is exactly 1 (not 0, Z, or X), we choose the then branch, else the else branch. (Non-monotonic semantics).
S4vec-fix
S4vec-rev-blocks
Sparseint-rev-blocks
S4vec-part-select
S3vec-bit?
S4vec-concat
S4vec-bitmux
S4vec-bit?!
S3vec-?*
S3vec-?
Svex-s4apply
Apply an svex function to some s4vec arguments.
S4vec-bit?
S4vec-?*
S4vec-?
S4vec-===*
S4vec-pow
S4vec
S4vec-sign-ext
S4vec-override
S4vec-zero-ext
S4vec-wildeq-safe
S4vec-symwildeq
S4vec-shift-core
S4vec-remainder
S4vec-quotient
S4vec-bitxor
S3vec-bitxor
S4vec-resor
S4vec-resand
S4vec-bit-index
S4vec-bit-extract
S3vec-bitor
S3vec-bitand
S4vec->4vec
S4vec-wildeq
S4vec-times
S4vec-rsh
S4vec-plus
S4vec-minus
S4vec-bitand
S4vec-===
S4vec-<
S4vec-res
S4vec-lsh
S4vec-bitor
S4vec-==
S3vec-==
S4vec-equal
S3vec-reduction-or
S3vec-reduction-and
S4vec-sparseint-val
S4vec-parity
S4vec-countones
S2vec
S4vec-reduction-or
S4vec-reduction-and
S4vec-onehot0
S4vec-onehot
S4vec-offset
S3vec-bitnot
4vec->s4vec
S4vec-xdet
S4vec-uminus
S4vec-onset
S4vec-clog2
S4vec-bitnot
S4vec-1mask
S3vec-fix
S4vec->upper
S4vec->lower
S4vec-index-p
S4veclist
A list of s4vec-p objects.
S4vec-xfree-p
S4vec-2vec-p
S3vec-p
S2vec->val
S2vec-p
S4vec-correct-fn
S4vec-correct-formal-evals