• 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

Encoding Redundant Representations

Encoding Redundant Representations

Definitions and Theorems

Function: gamma

(defun gamma (i a b c)
  (if (zp i)
      (bitn c 0)
    (logior (bitn a (+ -1 (* 2 i)))
            (bitn b (+ -1 (* 2 i))))))

Function: delta

(defun delta (i a b c d)
  (if (zp i)
      (bitn d 0)
    (logand (logior (logand (bitn a (+ -2 (* 2 i)))
                            (bitn b (+ -2 (* 2 i))))
                    (logior (logand (bitn a (+ -2 (* 2 i)))
                                    (gamma (1- i) a b c))
                            (logand (bitn b (+ -2 (* 2 i)))
                                    (gamma (1- i) a b c))))
            (lognot (logxor (bitn a (1- (* 2 i)))
                            (bitn b (1- (* 2 i))))))))

Function: psi

(defun psi (i a b c d)
  (if (not (natp i))
      0
    (+ (bits a (1+ (* 2 i)) (* 2 i))
       (bits b (1+ (* 2 i)) (* 2 i))
       (gamma i a b c)
       (delta i a b c d)
       (* -4
          (+ (gamma (1+ i) a b c)
             (delta (1+ i) a b c d))))))

Theorem: psi-m-1

(defthm psi-m-1
  (implies (and (natp m)
                (>= m 1)
                (bvecp a (- (* 2 m) 2))
                (bvecp b (- (* 2 m) 2))
                (bvecp c 1)
                (bvecp d 1))
           (and (equal (gamma m a b c) 0)
                (equal (delta m a b c d) 0)
                (>= (psi (1- m) a b c d) 0)))
  :rule-classes nil)

Function: sum-psi

(defun sum-psi (m a b c d)
  (if (zp m)
      0
    (+ (* (expt 2 (* 2 (1- m)))
          (psi (1- m) a b c d))
       (sum-psi (1- m) a b c d))))

Theorem: sum-psi-lemma

(defthm sum-psi-lemma
  (implies (and (natp m)
                (<= 1 m)
                (bvecp a (- (* 2 m) 2))
                (bvecp b (- (* 2 m) 2))
                (bvecp c 1)
                (bvecp d 1))
           (equal (+ a b c d) (sum-psi m a b c d)))
  :rule-classes nil)

Theorem: psi-bnd

(defthm psi-bnd
  (and (integerp (psi i a b c d))
       (<= (psi i a b c d) 2)
       (>= (psi i a b c d) -2)))

Function: pp4-psi

(defun pp4-psi (i x a b c d n)
  (if (zerop i)
      (cat 1 1
           (bitn (lognot (neg (psi i a b c d))) 0)
           1 (bmux4 (psi i a b c d) x n)
           n)
    (cat 1 1
         (bitn (lognot (neg (psi i a b c d))) 0)
         1 (bmux4 (psi i a b c d) x n)
         n 0 1 (neg (psi (1- i) a b c d))
         1 0 (* 2 (1- i)))))

Function: sum-pp4-psi

(defun sum-pp4-psi (x a b c d m n)
  (if (zp m)
      0
    (+ (pp4-psi (1- m) x a b c d n)
       (sum-pp4-psi x a b c d (1- m) n))))

Theorem: redundant-booth

(defthm redundant-booth
  (implies (and (natp m)
                (<= 1 m)
                (not (zp n))
                (bvecp x (1- n))
                (bvecp a (- (* 2 m) 2))
                (bvecp b (- (* 2 m) 2))
                (bvecp c 1)
                (bvecp d 1)
                (= y (+ a b c d)))
           (= (+ (expt 2 n)
                 (sum-pp4-psi x a b c d m n))
              (+ (expt 2 (+ n (* 2 m))) (* x y))))
  :rule-classes nil)