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

Reduction logical AND of a 3vec.

Signature

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

Arguments

x — Guard (4vec-p x).

Returns

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

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

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

Definitions and Theorems

Function: 3vec-reduction-and

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

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

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

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

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

Theorem: 3vec-reduction-and-recursive

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

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

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

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

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