• 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

Bit Vector Addition

Bit Vector Addition

Definitions and Theorems

Theorem: half-adder

(defthm half-adder
  (implies (and (bvecp u 1) (bvecp v 1))
           (equal (+ u v)
                  (cat (logand u v) 1 (logxor u v) 1)))
  :rule-classes nil)

Theorem: add-2

(defthm add-2
  (implies (and (integerp x) (integerp y))
           (equal (+ x y)
                  (+ (logxor x y) (* 2 (logand x y)))))
  :rule-classes nil)

Theorem: full-adder

(defthm full-adder
  (implies (and (bvecp u 1)
                (bvecp v 1)
                (bvecp w 1))
           (equal (+ u v w)
                  (cat (logior (logand u v)
                               (logior (logand u w) (logand v w)))
                       1 (logxor u (logxor v w))
                       1)))
  :rule-classes nil)

Theorem: add-3

(defthm add-3
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (= (+ x y z)
              (+ (logxor x (logxor y z))
                 (* 2
                    (logior (logand x y)
                            (logior (logand x z) (logand y z)))))))
  :rule-classes nil)

Theorem: plus-logior-logand

(defthm plus-logior-logand
  (implies (and (integerp x) (integerp y))
           (equal (+ x y)
                  (- (* 2 (logior x y)) (logxor x y)))))

Theorem: lutz-lemma

(defthm lutz-lemma
  (implies (and (integerp x) (integerp y) (natp n))
           (and (iff (= (bits (+ x y) (1- n) 0)
                        (1- (expt 2 n)))
                     (= (bits (logxor x y) (1- n) 0)
                        (1- (expt 2 n))))
                (iff (= (bits (+ x y) (1- n) 0)
                        (1- (expt 2 n)))
                     (= (+ (bits x (1- n) 0) (bits y (1- n) 0))
                        (1- (expt 2 n)))))))

Function: cbit

(defun cbit (x y cin k)
  (if (zp k)
      cin
    (logior (logand (bitn x (1- k)) (bitn y (1- k)))
            (logior (logand (bitn x (1- k))
                            (cbit x y cin (1- k)))
                    (logand (bitn y (1- k))
                            (cbit x y cin (1- k)))))))

Theorem: ripple-carry-lemma

(defthm ripple-carry-lemma
  (implies (and (integerp x)
                (integerp y)
                (bitp cin)
                (natp i))
           (equal (bitn (+ x y cin) i)
                  (logxor (logxor (bitn x i) (bitn y i))
                          (cbit x y cin i)))))

Function: gen

(defun gen (x y i j)
  (declare (xargs :guard (and (integerp x) (integerp y))))
  (if (and (natp i) (natp j) (>= i j))
      (if (= (bitn x i) (bitn y i))
          (bitn x i)
        (gen x y (1- i) j))
    0))

Function: prop

(defun prop (x y i j)
  (declare (xargs :guard (and (integerp x) (integerp y))))
  (if (and (natp i) (natp j) (>= i j))
      (if (= (bitn x i) (bitn y i))
          0
        (prop x y (1- i) j))
    1))

Theorem: bvecp-1-gen

(defthm bvecp-1-gen
  (bvecp (gen x y i j) 1)
  :rule-classes
  (:rewrite (:forward-chaining :trigger-terms ((gen x y i j)))))

Theorem: bvecp-1-prop

(defthm bvecp-1-prop
  (bvecp (prop x y i j) 1)
  :rule-classes
  (:rewrite (:forward-chaining :trigger-terms ((prop x y i j)))))

Theorem: gen-i-i

(defthm gen-i-i
  (implies (and (integerp x) (integerp y) (natp i))
           (equal (gen x y i i)
                  (logand (bitn x i) (bitn y i)))))

Theorem: prop-i-i

(defthm prop-i-i
  (implies (and (integerp x) (integerp y) (natp i))
           (equal (prop x y i i)
                  (logxor (bitn x i) (bitn y i)))))

Theorem: gen-val

(defthm gen-val
  (implies (natp j)
           (equal (gen x y i j)
                  (if (>= (+ (bits x i j) (bits y i j))
                          (expt 2 (1+ (- i j))))
                      1
                    0))))

Theorem: bits-sum

(defthm bits-sum
  (implies (and (integerp x) (integerp y))
           (equal (bits (+ x y) i j)
                  (bits (+ (bits x i j)
                           (bits y i j)
                           (gen x y (1- j) 0))
                        (- i j)
                        0)))
  :rule-classes nil)

Theorem: prop-val

(defthm prop-val
  (implies (and (integerp i) (natp j) (>= i j))
           (equal (prop x y i j)
                  (if (= (+ (bits x i j) (bits y i j))
                         (1- (expt 2 (1+ (- i j)))))
                      1
                    0))))

Function: gp

(defun gp (x y i j)
  (cons (gen x y i j) (prop x y i j)))

Function: gp0

(defun gp0 (x y i) (gp x y i i))

Function: fco

(defun fco (gp1 gp2)
  (cons (logior (car gp1)
                (logand (cdr gp1) (car gp2)))
        (logand (cdr gp1) (cdr gp2))))

Theorem: fco-assoc

(defthm fco-assoc
  (implies (and (bitp g1)
                (bitp p1)
                (bitp g2)
                (bitp p2)
                (bitp g3)
                (bitp p3))
           (equal (fco (fco (cons g1 p1) (cons g2 p2))
                       (cons g3 p3))
                  (fco (cons g1 p1)
                       (fco (cons g2 p2) (cons g3 p3))))))

Theorem: gp-decomp

(defthm gp-decomp
  (implies (and (integerp x)
                (integerp y)
                (natp j)
                (natp i)
                (natp k)
                (<= j k)
                (< k i))
           (equal (fco (gp x y i (1+ k)) (gp x y k j))
                  (gp x y i j))))

Theorem: cbit-rewrite

(defthm cbit-rewrite
  (implies (and (integerp x)
                (integerp y)
                (bitp cin)
                (natp i))
           (equal (cbit x y cin (1+ i))
                  (logior (gen x y i 0)
                          (logand (prop x y i 0) cin)))))

Function: rc

(defun rc (x y i)
  (if (zp i)
      (gp0 x y 0)
    (fco (gp0 x y i) (rc x y (1- i)))))

Theorem: rc-correct

(defthm rc-correct
  (implies (and (integerp x) (integerp y) (natp i))
           (equal (rc x y i) (gp x y i 0))))

Function: lf

(defun lf (x y i d)
  (if (zp d)
      (gp0 x y i)
    (if (< (mod i (expt 2 d)) (expt 2 (1- d)))
        (lf x y i (1- d))
      (fco (lf x y i (1- d))
           (lf x
               y (+ (chop i (- d)) (expt 2 (1- d)) -1)
               (1- d))))))

Theorem: lf-correct-gen

(defthm lf-correct-gen
  (implies (and (integerp x)
                (integerp y)
                (natp i)
                (natp d))
           (equal (lf x y i d)
                  (gp x y i (chop i (- d))))))

Theorem: lf-correct

(defthm lf-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (bvecp i n))
           (equal (lf x y i n) (gp x y i 0))))

Function: ks

(defun ks (x y i d)
  (if (zp d)
      (gp0 x y i)
    (if (< i (expt 2 (1- d)))
        (ks x y i (1- d))
      (fco (ks x y i (1- d))
           (ks x y (- i (expt 2 (1- d)))
               (1- d))))))

Theorem: ks-correct-gen

(defthm ks-correct-gen
  (implies (and (integerp x)
                (integerp y)
                (natp i)
                (natp d))
           (equal (ks x y i d)
                  (gp x y i (max 0 (1+ (- i (expt 2 d))))))))

Theorem: ks-correct

(defthm ks-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (bvecp i n))
           (equal (ks x y i n) (gp x y i 0))))

Function: pi2

(defun pi2 (k)
  (if (zp k)
      0
    (if (integerp (/ k 2))
        (1+ (pi2 (/ k 2)))
      0)))

Theorem: pi2-upper

(defthm pi2-upper
  (implies (not (zp k))
           (<= (expt 2 (pi2 k)) k)))

Theorem: pi2-lemma

(defthm pi2-lemma
  (implies (and (not (zp k)) (integerp p))
           (iff (integerp (/ k (expt 2 p)))
                (<= p (pi2 k)))))

Function: bk0

(defun bk0 (x y i d)
  (if (zp d)
      (gp0 x y i)
    (if (< (pi2 (1+ i)) d)
        (bk0 x y i (1- d))
      (fco (bk0 x y i (1- d))
           (bk0 x y (- i (expt 2 (1- d)))
                (1- d))))))

Function: bk

(defun bk (x y i n)
  (let ((p (pi2 (1+ i))))
    (if (or (zp n)
            (not (bvecp i n))
            (= i (1- (expt 2 p))))
        (bk0 x y i n)
      (fco (bk0 x y i n)
           (bk x y (- i (expt 2 p)) n)))))

Theorem: bk0-correct-gen

(defthm bk0-correct-gen
  (implies (and (integerp x)
                (integerp y)
                (natp i)
                (natp d))
           (equal (bk0 x y i d)
                  (gp x y i
                      (1+ (- i (expt 2 (min (pi2 (1+ i)) d))))))))

Theorem: bk0-correct

(defthm bk0-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (bvecp i n))
           (equal (bk0 x y i n)
                  (gp x
                      y i (1+ (- i (expt 2 (pi2 (1+ i)))))))))

Theorem: bk-correct

(defthm bk-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (bvecp i n))
           (equal (bk x y i n) (gp x y i 0))))

Function: hc0

(defun hc0 (x y i k d)
  (let ((p (pi2 (1+ i))))
    (if (or (zp d) (< p k))
        (bk0 x y i k)
      (if (< i (expt 2 (+ k d -1)))
          (hc0 x y i k (1- d))
        (fco (hc0 x y i k (1- d))
             (hc0 x y (- i (expt 2 (+ k d -1)))
                  k (1- d)))))))

Function: hc

(defun hc (x y i k n)
  (let ((p (pi2 (1+ i))))
    (if (or (zp n)
            (not (bvecp i n))
            (>= (pi2 (1+ i)) k)
            (= i (1- (expt 2 p))))
        (hc0 x y i k (- n k))
      (fco (hc0 x y i k (- n k))
           (hc x y (- i (expt 2 p)) k n)))))

Theorem: hc0-correct-gen

(defthm hc0-correct-gen
  (implies (and (integerp x)
                (integerp y)
                (natp i)
                (natp k)
                (natp d)
                (>= (pi2 (1+ i)) k))
           (let ((m (max 0 (- (1+ i) (expt 2 (+ k d))))))
             (equal (hc0 x y i k d) (gp x y i m)))))

Theorem: hc0-correct

(defthm hc0-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (natp k)
                (<= k n)
                (bvecp i n)
                (integerp (/ (1+ i) (expt 2 k))))
           (equal (hc0 x y i k (- n k))
                  (gp x y i 0))))

Theorem: hc-correct

(defthm hc-correct
  (implies (and (integerp x)
                (integerp y)
                (natp n)
                (natp k)
                (<= k n)
                (bvecp i n))
           (equal (hc x y i k n) (gp x y i 0))))