• 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
            • 4vec-bit?
            • 4vec-part-install
            • 4vec-concat
            • 4vec-?
            • 4vec-rsh
            • 4vec-bit?!
            • 4vec-===*
            • 4vec-reduction-and
            • 4vec-bit-extract
            • 4vec-rev-blocks
            • 4vec-lsh
            • 4vec-resor
            • 4vec-resand
            • 4vec-parity
            • 4vec-plus
            • 4vec-<
            • 4vec-minus
            • 4vec-res
            • 4vec-override
            • 4vec-bit-index
            • 4vec-?!
            • 4vec-zero-ext
            • 4vec-part-select
            • 4vec-===
            • 4vec-remainder
            • 4vec-reduction-or
            • 4vec-idx->4v
            • 4vec-==
            • 4vec-sign-ext
            • 4vec-quotient
            • 4vec-?*
            • 4vec-bitxor
            • 4vec-wildeq
            • 4vec-times
            • 4vec-bitmux
            • 4vec-symwildeq
            • 4vec-bitand
            • 4vec-wildeq-safe
            • 4vec-bitor
            • 4vec-shift-core
            • 4vec-pow
            • 4vec-onset
            • 4vec-offset
            • 4vec-xdet
            • 4vec-uminus
            • 4vec-clog2
            • 4vec-bitnot
            • 4vec-onehot
            • 4vec-countones
            • 4veclist-p-to-stringp
            • 4vec-p-to-stringp
            • 4vec-onehot0
            • 4vec-1mask
            • 4vec-p-to-stringp-aux
            • 4v->4vec-bit
            • 4v-to-characterp
            • Bool->vec
            • Unsigned-4vec-p
          • 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

• 4vec-operations

4vec-bit?!

Bitwise multiple if-then-elses of 4vecs; doesn't unfloat then/else values; uses else branch bits for any test bits not equal to 1 (non-monotonic semantics in this respect).

Signature

(4vec-bit?! tests thens elses) → choices

Arguments

tests — Guard (4vec-p tests).

thens — Guard (4vec-p thens).

elses — Guard (4vec-p elses).

Returns

choices — Type (4vec-p choices).

We carry out an independent if-then-else for each bit of tests, thens, and elses, producing a new vector with all of the answers. This result is computed bit by bit, with result[i] being set to:

• thens[i] if tests[i] is 1,
• elses[i] if tests[i] is not 1.

This is used for conditionally overriding signals, as in:

(bit?! override-test override-val regular-val)

This way, if the override-test is left out of the environment (therefore its value is X), the regular value will go through.

Definitions and Theorems

Function: 4vec-bit?!

(defun 4vec-bit?! (tests thens elses)
  (declare (xargs :guard (and (4vec-p tests)
                              (4vec-p thens)
                              (4vec-p elses))))
  (let ((__function__ '4vec-bit?!))
    (declare (ignorable __function__))
    (4vec-bitmux (4vec-1mask tests)
                 thens elses)))

Theorem: 4vec-p-of-4vec-bit?!

(defthm 4vec-p-of-4vec-bit?!
  (b* ((choices (4vec-bit?! tests thens elses)))
    (4vec-p choices))
  :rule-classes :rewrite)

Theorem: 4vec-bit?!-of-4vec-fix-tests

(defthm 4vec-bit?!-of-4vec-fix-tests
  (equal (4vec-bit?! (4vec-fix tests)
                     thens elses)
         (4vec-bit?! tests thens elses)))

Theorem: 4vec-bit?!-4vec-equiv-congruence-on-tests

(defthm 4vec-bit?!-4vec-equiv-congruence-on-tests
  (implies (4vec-equiv tests tests-equiv)
           (equal (4vec-bit?! tests thens elses)
                  (4vec-bit?! tests-equiv thens elses)))
  :rule-classes :congruence)

Theorem: 4vec-bit?!-of-4vec-fix-thens

(defthm 4vec-bit?!-of-4vec-fix-thens
  (equal (4vec-bit?! tests (4vec-fix thens)
                     elses)
         (4vec-bit?! tests thens elses)))

Theorem: 4vec-bit?!-4vec-equiv-congruence-on-thens

(defthm 4vec-bit?!-4vec-equiv-congruence-on-thens
  (implies (4vec-equiv thens thens-equiv)
           (equal (4vec-bit?! tests thens elses)
                  (4vec-bit?! tests thens-equiv elses)))
  :rule-classes :congruence)

Theorem: 4vec-bit?!-of-4vec-fix-elses

(defthm 4vec-bit?!-of-4vec-fix-elses
  (equal (4vec-bit?! tests thens (4vec-fix elses))
         (4vec-bit?! tests thens elses)))

Theorem: 4vec-bit?!-4vec-equiv-congruence-on-elses

(defthm 4vec-bit?!-4vec-equiv-congruence-on-elses
  (implies (4vec-equiv elses elses-equiv)
           (equal (4vec-bit?! tests thens elses)
                  (4vec-bit?! tests thens elses-equiv)))
  :rule-classes :congruence)