Radix-4 Booth Encoding
Function:
(defun theta (i y) (+ (bitn y (1- (* 2 i))) (bitn y (* 2 i)) (* -2 (bitn y (1+ (* 2 i))))))
Theorem:
(defthm theta-bounds (and (<= -2 (theta i y)) (<= (theta i y) 2)) :rule-classes :linear)
Function:
(defun sum-theta (m y) (if (zp m) 0 (+ (* (expt 2 (* 2 (1- m))) (theta (1- m) y)) (sum-theta (1- m) y))))
Theorem:
(defthm sum-theta-lemma-signed (implies (and (posp m) (bvecp y (* 2 m))) (equal (sum-theta m y) (si y (* 2 m)))))
Function:
(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:
(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:
(defun tau (zeta sign) (if (equal zeta 0) 0 (if (< 0 zeta) sign (lognot1 sign))))
Function:
(defun neg (x) (if (< x 0) 1 0))
Function:
(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:
(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:
(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:
(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:
(defthm sum-theta-lemma (implies (and (not (zp m)) (bvecp y (1- (* 2 m)))) (equal y (sum-theta m y))) :rule-classes nil)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defun nbit (i y) (bitn y (1+ (* 2 i))))
Theorem:
(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:
(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:
(defthm bvecp-bmux4p (implies (and (not (zp n)) (bvecp x (1- n))) (bvecp (bmux4p i x y n) n)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)))))))