• 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 3vec-operations

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.

Signature

(3vec-?* test then else) → choice

Arguments

test — Guard (4vec-p test).

then — Guard (4vec-p then).

else — Guard (4vec-p else).

Returns

choice — Type (4vec-p choice).

The difference between this and 3vec-? is that when the test is X and the branches are both Z, here we return Z whereas 3vec-? returns X.

Definitions and Theorems

Function: 3vec-?*

(defun 3vec-?* (test then else)
  (declare (xargs :guard (and (4vec-p test)
                              (4vec-p then)
                              (4vec-p else))))
  (let ((__function__ '3vec-?*))
    (declare (ignorable __function__))
    (b* (((4vec test))
         ((when (eql test.upper 0))
          (4vec-fix else))
         ((when (not (eql test.lower 0)))
          (4vec-fix then))
         ((4vec then))
         ((4vec else)))
      (4vec (logior then.upper else.upper
                    (logxor then.lower else.lower))
            (logand (logeqv then.upper else.upper)
                    then.lower else.lower)))))

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

(defthm 4vec-p-of-3vec-?*
  (b* ((choice (3vec-?* test then else)))
    (4vec-p choice))
  :rule-classes :rewrite)

Theorem: 3vec-?*-of-4vec-fix-test

(defthm 3vec-?*-of-4vec-fix-test
  (equal (3vec-?* (4vec-fix test) then else)
         (3vec-?* test then else)))

Theorem: 3vec-?*-4vec-equiv-congruence-on-test

(defthm 3vec-?*-4vec-equiv-congruence-on-test
  (implies (4vec-equiv test test-equiv)
           (equal (3vec-?* test then else)
                  (3vec-?* test-equiv then else)))
  :rule-classes :congruence)

Theorem: 3vec-?*-of-4vec-fix-then

(defthm 3vec-?*-of-4vec-fix-then
  (equal (3vec-?* test (4vec-fix then) else)
         (3vec-?* test then else)))

Theorem: 3vec-?*-4vec-equiv-congruence-on-then

(defthm 3vec-?*-4vec-equiv-congruence-on-then
  (implies (4vec-equiv then then-equiv)
           (equal (3vec-?* test then else)
                  (3vec-?* test then-equiv else)))
  :rule-classes :congruence)

Theorem: 3vec-?*-of-4vec-fix-else

(defthm 3vec-?*-of-4vec-fix-else
  (equal (3vec-?* test then (4vec-fix else))
         (3vec-?* test then else)))

Theorem: 3vec-?*-4vec-equiv-congruence-on-else

(defthm 3vec-?*-4vec-equiv-congruence-on-else
  (implies (4vec-equiv else else-equiv)
           (equal (3vec-?* test then else)
                  (3vec-?* test then else-equiv)))
  :rule-classes :congruence)