Statically Encoded Multiplier Arrays
Function:
(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:
(defun phi (i y) (if (= (bits (mu i y) 1 0) 3) -1 (bits (mu i y) 1 0)))
Theorem:
(defthm phi-bnd (member (phi i y) '(-1 0 1 2)))
Function:
(defun sum-odd-powers-of-2 (m) (if (zp m) 0 (+ (expt 2 (1- (* 2 m))) (sum-odd-powers-of-2 (1- m)))))
Theorem:
(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:
(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:
(defun sum-phi (m y) (if (zp m) 0 (+ (* (expt 2 (* 2 (1- m))) (phi (1- m) y)) (sum-phi (1- m) y))))
Theorem:
(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:
(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:
(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:
(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)