• 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

Statically Encoded Multiplier Arrays

Statically Encoded Multiplier Arrays

Definitions and Theorems

Function: m-mu-chi

(defun m-mu-chi (i mode)
  (cond ((equal mode 'mu)
         (if (zp i) 1 (cons (cons 1 i) 1)))
        ((equal mode 'chi)
         (if (zp i) 0 (cons (cons 1 i) 0)))))

Function: phi

(defun phi (i y)
  (if (= (bits (mu i y) 1 0) 3)
      -1
    (bits (mu i y) 1 0)))

Theorem: phi-bnd

(defthm phi-bnd
  (member (phi i y) '(-1 0 1 2)))

Function: sum-odd-powers-of-2

(defun sum-odd-powers-of-2 (m)
  (if (zp m)
      0
    (+ (expt 2 (1- (* 2 m)))
       (sum-odd-powers-of-2 (1- m)))))

Theorem: chi-m

(defthm chi-m
  (implies (and (natp m)
                (natp y)
                (<= y (sum-odd-powers-of-2 m)))
           (equal (chi m y) 0))
  :rule-classes nil)

Theorem: phi-m-1

(defthm phi-m-1
  (implies (and (natp m)
                (natp y)
                (<= y (sum-odd-powers-of-2 m)))
           (>= (phi (1- m) y) 0))
  :rule-classes nil)

Function: sum-phi

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

Theorem: sum-phi-lemma

(defthm sum-phi-lemma
  (implies (and (natp m)
                (natp y)
                (<= y (sum-odd-powers-of-2 m)))
           (equal y (sum-phi m y)))
  :rule-classes nil)

Function: pp4-phi

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

Function: sum-pp4-phi

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

Theorem: static-booth

(defthm static-booth
  (implies (and (not (zp n))
                (not (zp m))
                (bvecp x (1- n))
                (natp y)
                (<= y (sum-odd-powers-of-2 m)))
           (= (+ (expt 2 n) (sum-pp4-phi x y m n))
              (+ (expt 2 (+ n (* 2 m))) (* x y))))
  :rule-classes nil)