• 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

• 3vec-operations

3vec-bit?

Bitwise multiple if-then-elses of 4vecs, with a 3vec test vector; doesn't unfloat then/else values.

Signature

(3vec-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).

See 4vec-bit?. This is identical except that we assume tests has no Z bits.

Definitions and Theorems

Function: 3vec-bit?

(defun 3vec-bit? (tests thens elses)
 (declare (xargs :guard (and (4vec-p tests)
                             (4vec-p thens)
                             (4vec-p elses))))
 (let ((__function__ '3vec-bit?))
  (declare (ignorable __function__))
  (b* (((4vec tests))
       ((4vec thens))
       ((4vec elses))
       (test-x (logand tests.upper (lognot tests.lower))))
   (4vec (logior (logand (lognot tests.upper)
                         elses.upper)
                 (logand tests.lower thens.upper)
                 (logand test-x
                         (logior (logior thens.upper thens.lower)
                                 (logior elses.upper elses.lower))))
         (logior (logand (lognot tests.upper)
                         elses.lower)
                 (logand tests.lower thens.lower)
                 (logand test-x (logand thens.upper thens.lower)
                         (logand elses.upper elses.lower)))))))

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

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

Theorem: 3vec-?-in-terms-of-3vec-bit?

(defthm 3vec-?-in-terms-of-3vec-bit?
  (implies
       (3vec-p tests)
       (equal (3vec-bit? (4vec-sign-ext 1 (3vec-reduction-or tests))
                         thens elses)
              (3vec-? tests thens elses))))

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

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

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

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

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

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

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

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

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

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

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

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