Radix-8 Booth Encoding
Function:
(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:
(defun sum-eta (m y) (if (zp m) 0 (+ (* (expt 2 (* 3 (1- m))) (eta (1- m) y)) (sum-eta (1- m) y))))
Theorem:
(defthm sum-eta-lemma (implies (and (not (zp m)) (bvecp y (1- (* 3 m)))) (equal y (sum-eta m y))) :rule-classes nil)
Function:
(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:
(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:
(defun sum-xi (m) (if (zp m) 0 (+ (* (expt 2 (* 3 (1- m))) (xi (1- m))) (sum-xi (1- m)))))
Function:
(defun sum-pp8 (x m n) (if (zp m) 0 (+ (pp8 (1- m) x n) (sum-pp8 x (1- m) n))))
Theorem:
(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:
(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:
(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:
(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)