• 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-?!

If-then-elses of 4vecs 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).

Signature

(4vec-?! test then else) → choices

Arguments

test — Guard (4vec-p test).

then — Guard (4vec-p then).

else — Guard (4vec-p else).

Returns

choices — Type (4vec-p choices).

Definitions and Theorems

Function: 4vec-?!

(defun 4vec-?! (test then else)
  (declare (xargs :guard (and (4vec-p test)
                              (4vec-p then)
                              (4vec-p else))))
  (let ((__function__ '4vec-?!))
    (declare (ignorable __function__))
    (b* (((4vec test))
         (pick-else (equal 0 (logand test.upper test.lower))))
      (if pick-else (4vec-fix else)
        (4vec-fix then)))))

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

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

Theorem: 4vec-?!-of-4vec-fix-test

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

Theorem: 4vec-?!-4vec-equiv-congruence-on-test

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

Theorem: 4vec-?!-of-4vec-fix-then

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

Theorem: 4vec-?!-4vec-equiv-congruence-on-then

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

Theorem: 4vec-?!-of-4vec-fix-else

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

Theorem: 4vec-?!-4vec-equiv-congruence-on-else

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