• 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-reduction-or

Reduction logical OR of a 3vec.

Signature

(3vec-reduction-or x) → or-x

Arguments

x — Guard (4vec-p x).

Returns

or-x — Type (4vec-p or-x).

See 4vec-reduction-or for some additional discussion. We assume that there are no Z bits. In that case, following the boolean-convention, we return:

• False (all 0s) if all of the (infinite) bits are 0, i.e., if X is 0,
• True (all 1s) if there is any bit that is 1, or
• All Xes otherwise.

Definitions and Theorems

Function: 3vec-reduction-or

(defun 3vec-reduction-or (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '3vec-reduction-or))
    (declare (ignorable __function__))
    (if-2vec-p (x)
               (2vec (bool->vec (not (int= (2vec->val x) 0))))
               (b* (((4vec x)))
                 (4vec (bool->vec (not (int= x.upper 0)))
                       (bool->vec (not (int= x.lower 0))))))))

Theorem: 4vec-p-of-3vec-reduction-or

(defthm 4vec-p-of-3vec-reduction-or
  (b* ((or-x (3vec-reduction-or x)))
    (4vec-p or-x))
  :rule-classes :rewrite)

Theorem: 3vec-p-of-3vec-reduction-or

(defthm 3vec-p-of-3vec-reduction-or
  (b* ((?or-x (3vec-reduction-or x)))
    (implies (3vec-p x) (3vec-p or-x))))

Theorem: 3vec-reduction-or-recursive

(defthm 3vec-reduction-or-recursive
 (implies
  (3vec-p! x)
  (equal
   (3vec-reduction-or x)
   (b* (((4vec x)))
    (if (and (or (zip x.upper) (eql x.upper -1))
             (or (zip x.lower) (eql x.lower -1)))
        (3vec-fix x)
     (4v->4vec-bit
        (acl2::4v-or
             (4vec-idx->4v 0 x)
             (4vec-idx->4v
                  0
                  (3vec-reduction-or (4vec (logcdr x.upper)
                                           (logcdr x.lower))))))))))
 :rule-classes
 ((:definition :install-body nil
               :clique (3vec-reduction-or)
               :controller-alist ((3vec-reduction-or t)))))

Theorem: 3vec-reduction-or-of-4vec-fix-x

(defthm 3vec-reduction-or-of-4vec-fix-x
  (equal (3vec-reduction-or (4vec-fix x))
         (3vec-reduction-or x)))

Theorem: 3vec-reduction-or-4vec-equiv-congruence-on-x

(defthm 3vec-reduction-or-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (3vec-reduction-or x)
                  (3vec-reduction-or x-equiv)))
  :rule-classes :congruence)