• 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
            • 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-8 Booth Encoding

Radix-8 Booth Encoding

Definitions and Theorems

Function: eta

(defun eta (i y)
  (+ (bitn y (1- (* 3 i)))
     (bitn y (* 3 i))
     (* 2 (bitn y (1+ (* 3 i))))
     (* -4 (bitn y (+ 2 (* 3 i))))))

Function: sum-eta

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

Theorem: sum-eta-lemma

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

Function: bmux8

(defun bmux8 (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))
    (3 (* 3 x))
    (-3 (bits (lognot (* 3 x)) (1- n) 0))
    (4 (* 4 x))
    (-4 (bits (lognot (* 4 x)) (1- n) 0))
    (0 0)))

Function: pp8

(defun pp8 (i x n)
  (if (zerop i)
      (cat 3 2 (bitn (lognot (neg (xi i))) 0)
           1 (bmux8 (xi i) x n)
           n)
    (cat 3 2 (bitn (lognot (neg (xi i))) 0)
         1 (bmux8 (xi i) x n)
         n 0 2 (neg (xi (1- i)))
         1 0 (* 3 (1- i)))))

Function: sum-xi

(defun sum-xi (m)
  (if (zp m)
      0
    (+ (* (expt 2 (* 3 (1- m))) (xi (1- m)))
       (sum-xi (1- m)))))

Function: sum-pp8

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

Theorem: booth8-thm

(defthm booth8-thm
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (- n 2)))
           (= (+ (expt 2 n) (sum-pp8 x m n))
              (+ (expt 2 (+ n (* 3 m)))
                 (* x (sum-xi m))
                 (- (* (expt 2 (* 3 (1- m)))
                       (neg (xi (1- m))))))))
  :rule-classes nil)

Function: pp8-eta

(defun pp8-eta (i x y n)
  (if (zerop i)
      (cat 3 2 (bitn (lognot (neg (eta i y))) 0)
           1 (bmux8 (eta i y) x n)
           n)
    (cat 3 2 (bitn (lognot (neg (eta i y))) 0)
         1 (bmux8 (eta i y) x n)
         n 0 2 (neg (eta (1- i) y))
         1 0 (* 3 (1- i)))))

Function: sum-pp8-eta

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

Theorem: booth8-corollary

(defthm booth8-corollary
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (- n 2))
                (bvecp y (1- (* 3 m))))
           (= (+ (expt 2 n) (sum-pp8-eta x y m n))
              (+ (expt 2 (+ n (* 3 m))) (* x y))))
  :rule-classes nil)