• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
            • Radix-4 Booth Encoding
            • Encoding Redundant Representations
            • Radix-8 Booth Encoding
            • Statically Encoded Multiplier Arrays
          • FMA-Based Division
          • Addition
          • SRT Division and Square Root
        • Register-Transfer Logic
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Multiplication

Radix-4 Booth Encoding

Radix-4 Booth Encoding

Definitions and Theorems

Function: theta

(defun theta (i y)
  (+ (bitn y (1- (* 2 i)))
     (bitn y (* 2 i))
     (* -2 (bitn y (1+ (* 2 i))))))

Theorem: theta-bounds

(defthm theta-bounds
  (and (<= -2 (theta i y))
       (<= (theta i y) 2))
  :rule-classes :linear)

Function: sum-theta

(defun sum-theta (m y)
  (if (zp m)
      0
    (+ (* (expt 2 (* 2 (1- m)))
          (theta (1- m) y))
       (sum-theta (1- m) y))))

Theorem: sum-theta-lemma-signed

(defthm sum-theta-lemma-signed
  (implies (and (posp m) (bvecp y (* 2 m)))
           (equal (sum-theta m y) (si y (* 2 m)))))

Function: bmux4signed

(defun bmux4signed (zeta x n)
  (case zeta
    (1 x)
    (-1 (bits (lognot x) (1- n) 0))
    (2 (bits (* 2 x) (1- n) 0))
    (-2 (bits (lognot (* 2 x)) (1- n) 0))
    (0 0)))

Theorem: bvecp-bmux4signed

(defthm bvecp-bmux4signed
  (implies (and (integerp zeta)
                (<= -2 zeta)
                (<= zeta 2)
                (integerp n)
                (bvecp x n))
           (bvecp (bmux4signed zeta x n) n))
  :rule-classes
  ((:rewrite :corollary (implies (and (integerp zeta)
                                      (<= -2 zeta)
                                      (<= zeta 2)
                                      (bvecp x n)
                                      (integerp n))
                                 (bvecp (bmux4signed zeta x n) n)))
   (:type-prescription
        :corollary (implies (and (integerp zeta)
                                 (<= -2 zeta)
                                 (<= zeta 2)
                                 (bvecp x n)
                                 (integerp n))
                            (natp (bmux4signed zeta x n))))
   (:linear :corollary (implies (and (integerp zeta)
                                     (<= -2 zeta)
                                     (<= zeta 2)
                                     (bvecp x n)
                                     (integerp n))
                                (< (bmux4signed zeta x n)
                                   (expt 2 n))))))

Function: tau

(defun tau (zeta sign)
  (if (equal zeta 0)
      0
    (if (< 0 zeta) sign (lognot1 sign))))

Function: neg

(defun neg (x) (if (< x 0) 1 0))

Function: pp4signed-theta

(defun pp4signed-theta (i x y n)
  (if (zerop i)
      (cat 1 1
           (lognot1 (tau (theta i y) (bitn x (1- n))))
           1 (bmux4signed (theta i y) x n)
           n)
    (cat 1 1
         (lognot1 (tau (theta i y) (bitn x (1- n))))
         1 (bmux4signed (theta i y) x n)
         n 0 1 (neg (theta (1- i) y))
         1 0 (* 2 (1- i)))))

Function: sum-pp4signed-theta

(defun sum-pp4signed-theta (x y m n)
  (if (zp m)
      0
    (+ (pp4signed-theta (1- m) x y n)
       (sum-pp4signed-theta x y (1- m) n))))

Theorem: booth4signed-corollary

(defthm booth4signed-corollary
  (implies (and (posp m)
                (posp n)
                (bvecp x n)
                (bvecp y (* 2 m)))
           (equal (sum-pp4signed-theta x y m n)
                  (+ (- (expt 2 n))
                     (- (* (expt 2 (* 2 (1- m)))
                           (neg (theta (1- m) y))))
                     (expt 2 (+ n (* 2 m)))
                     (* (si x n) (si y (* 2 m)))))))

Theorem: booth4signed-corollary-alt

(defthm booth4signed-corollary-alt
  (implies (and (posp m)
                (posp n)
                (bvecp x n)
                (bvecp y (* 2 m)))
           (equal (+ (expt 2 n)
                     (* (expt 2 (* 2 (1- m)))
                        (neg (theta (1- m) y)))
                     (sum-pp4signed-theta x y m n))
                  (+ (expt 2 (+ n (* 2 m)))
                     (* (si x n) (si y (* 2 m)))))))

Theorem: sum-theta-lemma

(defthm sum-theta-lemma
  (implies (and (not (zp m))
                (bvecp y (1- (* 2 m))))
           (equal y (sum-theta m y)))
  :rule-classes nil)

Function: bmux4

(defun bmux4 (zeta x n)
  (case zeta
    (1 x)
    (-1 (bits (lognot x) (1- n) 0))
    (2 (* 2 x))
    (-2 (bits (lognot (* 2 x)) (1- n) 0))
    (0 0)))

Function: pp4-theta

(defun pp4-theta (i x y n)
  (if (zerop i)
      (cat 1 1 (bitn (lognot (neg (theta i y))) 0)
           1 (bmux4 (theta i y) x n)
           n)
    (cat 1 1 (bitn (lognot (neg (theta i y))) 0)
         1 (bmux4 (theta i y) x n)
         n 0 1 (neg (theta (1- i) y))
         1 0 (* 2 (1- i)))))

Function: sum-pp4-theta

(defun sum-pp4-theta (x y m n)
  (if (zp m)
      0
    (+ (pp4-theta (1- m) x y n)
       (sum-pp4-theta x y (1- m) n))))

Theorem: booth4-corollary-1

(defthm booth4-corollary-1
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m))))
           (= (+ (expt 2 n) (sum-pp4-theta x y m n))
              (+ (expt 2 (+ n (* 2 m))) (* x y))))
  :rule-classes nil)

Function: pp4p-theta

(defun pp4p-theta (i x y n)
  (if (zerop i)
      (cat (bitn (lognot (neg (theta i y))) 0)
           1 (neg (theta i y))
           1 (neg (theta i y))
           1 (bmux4 (theta i y) x n)
           n)
    (cat 1 1 (bitn (lognot (neg (theta i y))) 0)
         1 (bmux4 (theta i y) x n)
         n 0 1 (neg (theta (1- i) y))
         1 0 (* 2 (1- i)))))

Function: sum-pp4p-theta

(defun sum-pp4p-theta (x y m n)
  (if (zp m)
      0
    (+ (pp4p-theta (1- m) x y n)
       (sum-pp4p-theta x y (1- m) n))))

Theorem: booth4-corollary-2

(defthm booth4-corollary-2
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m))))
           (= (bits (sum-pp4p-theta x y m n)
                    (1- (+ n (* 2 m)))
                    0)
              (* x y)))
  :rule-classes nil)

Function: mag

(defun mag (i y)
  (if (member (bits y (1+ (* 2 i)) (1- (* 2 i)))
              '(3 4))
      2
    (if (member (bits y (* 2 i) (1- (* 2 i)))
                '(1 2))
        1
      0)))

Function: nbit

(defun nbit (i y) (bitn y (1+ (* 2 i))))

Theorem: theta-rewrite

(defthm theta-rewrite
  (implies (and (natp y) (natp i))
           (equal (theta i y)
                  (if (= (nbit i y) 1)
                      (- (mag i y))
                    (mag i y)))))

Function: bmux4p

(defun bmux4p (i x y n)
  (if (= (nbit i y) 1)
      (bits (lognot (* (mag i y) x)) (1- n) 0)
    (* (mag i y) x)))

Theorem: bvecp-bmux4p

(defthm bvecp-bmux4p
  (implies (and (not (zp n)) (bvecp x (1- n)))
           (bvecp (bmux4p i x y n) n)))

Theorem: bmux4p-rewrite

(defthm bmux4p-rewrite
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m)))
                (natp i)
                (< i m))
           (equal (bmux4p i x y n)
                  (+ (* (theta i y) x)
                     (* (1- (expt 2 n)) (nbit i y))))))

Function: pp4p

(defun pp4p (i x y n)
  (if (zerop i)
      (cat (if (= (nbit 0 y) 0) 1 0)
           1 (nbit 0 y)
           1 (nbit 0 y)
           1 (bmux4p 0 x y n)
           n)
    (cat 1 1 (lognot (nbit i y))
         1 (bmux4p i x y n)
         n 0 1 (nbit (1- i) y)
         1 0 (* 2 (1- i)))))

Theorem: pp4p0-rewrite

(defthm pp4p0-rewrite
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m))))
           (equal (pp4p 0 x y n)
                  (+ (expt 2 (+ n 2))
                     (* (theta 0 y) x)
                     (- (nbit 0 y))))))

Theorem: pp4p-rewrite

(defthm pp4p-rewrite
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m)))
                (not (zp i))
                (< i m))
           (equal (pp4p i x y n)
                  (+ (expt 2 (+ n (* 2 i) 1))
                     (expt 2 (+ n (* 2 i)))
                     (* (expt 2 (* 2 i)) (theta i y) x)
                     (* (expt 2 (* 2 (1- i)))
                        (nbit (1- i) y))
                     (- (* (expt 2 (* 2 i)) (nbit i y)))))))

Function: sum-pp4p

(defun sum-pp4p (x y m n)
  (if (zp m)
      0
    (+ (pp4p (1- m) x y n)
       (sum-pp4p x y (1- m) n))))

Theorem: booth4-corollary-3

(defthm booth4-corollary-3
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (bvecp y (1- (* 2 m))))
           (equal (sum-pp4p x y m n)
                  (+ (* x y) (expt 2 (+ n (* 2 m)))))))