• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
          • Multiplication
          • FMA-Based Division
          • Addition
            • Bit Vector Addition
            • Leading One Prediction
            • Trailing One Prediction
          • SRT Division and Square Root
        • Register-Transfer Logic
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Addition

Leading One Prediction

Leading One Prediction

Definitions and Theorems

Function: u0

(defun u0 (x y n)
  (bits (logior x (lognot y)) (- n 2) 0))

Theorem: lza-thm-0-a

(defthm lza-thm-0-a
  (implies (and (natp n)
                (> n 1)
                (natp x)
                (natp y)
                (= (expo x) (1- n))
                (= (expo y) (- n 2)))
           (iff (equal (- x y) 1)
                (equal (u0 x y n) 0))))

Theorem: lza-thm-0-b

(defthm lza-thm-0-b
  (implies (and (natp n)
                (> n 1)
                (natp x)
                (natp y)
                (= (expo x) (1- n))
                (= (expo y) (- n 2))
                (not (= (u0 x y n) 0)))
           (and (<= (expo (u0 x y n)) (expo (- x y)))
                (<= (expo (- x y))
                    (1+ (expo (u0 x y n)))))))

Function: p0

(defun p0 (a b)
  (declare (xargs :guard (and (integerp a) (integerp b))))
  (logxor a b))

Function: g0

(defun g0 (a b)
  (declare (xargs :guard (and (integerp a) (integerp b))))
  (logand a b))

Function: k0

(defun k0 (a b n)
  (declare (xargs :guard (and (integerp a)
                              (integerp b)
                              (integerp n))))
  (logand (bits (lognot a) (1- n) 0)
          (bits (lognot b) (1- n) 0)))

Function: w0

(defun w0 (a b n)
  (declare (xargs :guard (and (integerp a)
                              (integerp b)
                              (integerp n))))
  (bits (lognot (logxor (p0 a b) (* 2 (k0 a b n))))
        (1- n)
        0))

Theorem: p0-rewrite

(defthm p0-rewrite
  (implies (and (integerp a)
                (integerp b)
                (integerp j))
           (equal (bitn (p0 a b) j)
                  (if (= (bitn a j) (bitn b j)) 0 1))))

Theorem: g0-rewrite

(defthm g0-rewrite
  (implies (and (integerp a)
                (integerp b)
                (integerp j))
           (equal (bitn (g0 a b) j)
                  (if (and (= (bitn a j) 1) (= (bitn b j) 1))
                      1
                    0))))

Theorem: k0-rewrite

(defthm k0-rewrite
  (implies (and (integerp a)
                (integerp b)
                (natp j)
                (natp n)
                (< j n))
           (equal (bitn (k0 a b n) j)
                  (if (and (= (bitn a j) 0) (= (bitn b j) 0))
                      1
                    0))))

Theorem: w0-rewrite

(defthm w0-rewrite
  (implies (and (integerp a)
                (integerp b)
                (not (zp n))
                (not (zp j))
                (< j n))
           (equal (bitn (w0 a b n) j)
                  (if (= (bitn (p0 a b) j)
                         (bitn (k0 a b n) (1- j)))
                      1
                    0))))

Theorem: lza-thm-1-case-1

(defthm lza-thm-1-case-1
  (implies (and (not (zp n))
                (bvecp a n)
                (bvecp b n)
                (= (+ a b) (expt 2 n)))
           (equal (w0 a b n) 1)))

Theorem: lza-thm-1-case-2

(defthm lza-thm-1-case-2
  (implies (and (not (zp n))
                (bvecp a n)
                (bvecp b n)
                (> (+ a b) (expt 2 n)))
           (and (>= (w0 a b n) 2)
                (or (= (expo (bits (+ a b) (1- n) 0))
                       (expo (w0 a b n)))
                    (= (expo (bits (+ a b) (1- n) 0))
                       (1- (expo (w0 a b n)))))
                (or (= (expo (bits (+ a b 1) (1- n) 0))
                       (expo (w0 a b n)))
                    (= (expo (bits (+ a b 1) (1- n) 0))
                       (1- (expo (w0 a b n)))))))
  :rule-classes nil)

Function: z1

(defun z1 (a b n)
  (declare (xargs :guard (and (integerp a)
                              (integerp b)
                              (integerp n))))
  (logior (logand (logxor (bits (p0 a b) n 1) (k0 a b n))
                  (logxor (p0 a b) (* 2 (k0 a b n))))
          (logand (logxor (bits (p0 a b) n 1) (g0 a b))
                  (logxor (p0 a b) (* 2 (g0 a b))))))

Function: w1

(defun w1 (a b n)
  (declare (xargs :guard (and (integerp a)
                              (integerp b)
                              (integerp n))))
  (bits (lognot (z1 a b n)) (- n 2) 0))

Theorem: w1-rewrite

(defthm w1-rewrite
  (implies (and (integerp a)
                (integerp b)
                (not (zp n))
                (not (zp j))
                (< j (1- n)))
           (equal (bitn (w1 a b n) j)
                  (if (and (or (= (bitn (p0 a b) (1+ j))
                                  (bitn (k0 a b n) j))
                               (= (bitn (p0 a b) j)
                                  (bitn (k0 a b n) (1- j))))
                           (or (= (bitn (p0 a b) (1+ j))
                                  (bitn (g0 a b) j))
                               (= (bitn (p0 a b) j)
                                  (bitn (g0 a b) (1- j)))))
                      1
                    0))))

Theorem: lza-thm-2-case-1

(defthm lza-thm-2-case-1
  (implies (and (not (zp n))
                (bvecp a n)
                (bvecp b n)
                (= (+ a b) (1- (expt 2 n)))
                (natp i))
           (equal (w1 a b n) 0)))

Theorem: lza-thm-2-case-2

(defthm lza-thm-2-case-2
  (implies (and (natp n)
                (> n 1)
                (bvecp a n)
                (bvecp b n)
                (or (= (+ a b) (expt 2 n))
                    (= (+ a b) (- (expt 2 n) 2))))
           (equal (w1 a b n) 1)))

Theorem: lza-thm-2-case-3

(defthm lza-thm-2-case-3
  (implies (and (not (zp n))
                (bvecp a n)
                (bvecp b n)
                (= (bitn (p0 a b) (1- n)) 1)
                (> (+ a b) (expt 2 n)))
           (and (>= (w1 a b n) 2)
                (or (= (expo (bits (+ a b) (1- n) 0))
                       (expo (w1 a b n)))
                    (= (expo (bits (+ a b) (1- n) 0))
                       (1- (expo (w1 a b n)))))
                (or (= (expo (bits (+ a b 1) (1- n) 0))
                       (expo (w1 a b n)))
                    (= (expo (bits (+ a b 1) (1- n) 0))
                       (1- (expo (w1 a b n)))))))
  :rule-classes nil)

Theorem: lza-thm-2-case-4

(defthm lza-thm-2-case-4
  (implies (and (not (zp n))
                (bvecp a n)
                (bvecp b n)
                (= (bitn (p0 a b) (1- n)) 1)
                (< (+ a b) (- (expt 2 n) 2)))
           (and (>= (w1 a b n) 2)
                (or (= (expo (bits (lognot (+ a b)) (1- n) 0))
                       (expo (w1 a b n)))
                    (= (expo (bits (lognot (+ a b)) (1- n) 0))
                       (1- (expo (w1 a b n)))))
                (or (= (expo (bits (lognot (+ a b 1)) (1- n) 0))
                       (expo (w1 a b n)))
                    (= (expo (bits (lognot (+ a b 1)) (1- n) 0))
                       (1- (expo (w1 a b n)))))))
  :rule-classes nil)

Function: zseg

(defun zseg (x k i)
  (if (zp k)
      (if (= (bitn x i) 0) 1 0)
    (if (and (= (zseg x (1- k) (1+ (* 2 i))) 1)
             (= (zseg x (1- k) (* 2 i)) 1))
        1
      0)))

Function: zcount

(defun zcount (x k i)
  (if (zp k)
      0
    (if (= (zseg x (1- k) (1+ (* 2 i))) 1)
        (logior (expt 2 (1- k))
                (zcount x (1- k) (* 2 i)))
      (zcount x (1- k) (1+ (* 2 i))))))

Function: clz

(defun clz (x n) (zcount x n 0))

Theorem: clz-thm

(defthm clz-thm
  (implies (and (natp n)
                (bvecp x (expt 2 n))
                (> x 0))
           (equal (clz x n)
                  (- (1- (expt 2 n)) (expo x)))))