← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/lib1/mult.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/lib1/mult.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
(include-book "add")
 
6
 
 
7
(local (include-book "../support/top"))
 
8
 
 
9
(set-inhibit-warnings "theory")
 
10
(local (in-theory nil))
 
11
 
 
12
;;;**********************************************************************
 
13
;;;                     Radix-4 Booth Encoding
 
14
;;;**********************************************************************
 
15
 
 
16
(defun theta (i y)
 
17
  (+ (bitn y (1- (* 2 i))) 
 
18
     (bitn y (* 2 i))
 
19
     (* -2 (bit y (1+ (* 2 i))))))
 
20
 
 
21
(defun sum-theta (m y)
 
22
   (if (zp m)
 
23
       0
 
24
     (+ (* (expt 2 (* 2 (1- m))) (theta (1- m) y))
 
25
        (sum-theta (1- m) y))))
 
26
 
 
27
 
 
28
(defthm sum-theta-lemma
 
29
    (implies (and (not (zp m))
 
30
                  (bvecp y (1- (* 2 m))))
 
31
             (equal y (sum-theta m y)))
 
32
  :rule-classes ())
 
33
 
 
34
 
 
35
(defun bmux4 (zeta x n)
 
36
  (case zeta
 
37
    (1  x)
 
38
    (-1 (lnot x n))
 
39
    (2  (* 2 x))
 
40
    (-2 (lnot (* 2 x) n))
 
41
    (0  0)))
 
42
 
 
43
(defun neg (x) (if (< x 0) 1 0))
 
44
 
 
45
(encapsulate ((zeta (i) t))
 
46
 (local (defun zeta (i) (declare (ignore i)) 0))
 
47
 (defthm zeta-bnd 
 
48
     (and (integerp (zeta i))
 
49
          (<= (zeta i) 2)
 
50
          (>= (zeta i) -2))))
 
51
 
 
52
 
 
53
(defun pp4 (i x n)
 
54
  (if (zerop i)
 
55
      (cat 1 1
 
56
           (lnot (neg (zeta i)) 1) 1
 
57
           (bmux4 (zeta i) x n) n)
 
58
    (cat 1 1
 
59
         (lnot (neg (zeta i)) 1) 1
 
60
         (bmux4 (zeta i) x n) n
 
61
         0 1
 
62
         (neg (zeta (1- i))) 1
 
63
         0 (* 2 (1- i)))))
 
64
 
 
65
(defun sum-zeta (m)
 
66
  (if (zp m)
 
67
      0
 
68
    (+ (* (expt 2 (* 2 (1- m))) (zeta (1- m)))
 
69
       (sum-zeta (1- m)))))   
 
70
 
 
71
(defun sum-pp4 (x m n)
 
72
  (if (zp m)
 
73
      0
 
74
    (+ (pp4 (1- m) x n)
 
75
       (sum-pp4 x (1- m) n))))
 
76
 
 
77
 
 
78
(defthm booth4-thm
 
79
    (implies (and (not (zp n))
 
80
                  (not (zp m))
 
81
                  (bvecp x (1- n)))
 
82
             (= (+ (expt 2 n)
 
83
                   (sum-pp4 x m n))
 
84
                (+ (expt 2 (+ n (* 2 m)))
 
85
                   (* x (sum-zeta m))
 
86
                   (- (* (expt 2 (* 2 (1- m))) (neg (zeta (1- m))))))))
 
87
  :rule-classes ())
 
88
 
 
89
(defun pp4-theta (i x y n)
 
90
   (if (zerop i)
 
91
       (cat 1 1
 
92
            (lnot (neg (theta i y)) 1) 1
 
93
            (bmux4 (theta i y) x n) n)
 
94
     (cat 1 1
 
95
          (lnot (neg (theta i y)) 1) 1
 
96
          (bmux4 (theta i y) x n) n
 
97
          0 1
 
98
          (neg (theta (1- i) y)) 1
 
99
          0 (* 2 (1- i)))))
 
100
 
 
101
(defun sum-pp4-theta (x y m n)
 
102
  (if (zp m)
 
103
      0
 
104
    (+ (pp4-theta (1- m) x y n)
 
105
       (sum-pp4-theta x y (1- m) n))))
 
106
 
 
107
 
 
108
(defthm booth4-corollary
 
109
    (implies (and (not (zp n))
 
110
                  (not (zp m))
 
111
                  (bvecp x (1- n))
 
112
                  (bvecp y (1- (* 2 m))))
 
113
             (= (+ (expt 2 n)
 
114
                   (sum-pp4-theta x y m n))
 
115
                (+ (expt 2 (+ n (* 2 m)))
 
116
                   (* x y))))
 
117
  :rule-classes ())
 
118
 
 
119
;;;**********************************************************************
 
120
;;;                Statically Encoded Multiplier Arrays
 
121
;;;**********************************************************************
 
122
 
 
123
 
 
124
(mutual-recursion
 
125
 
 
126
 (defun mu (i y) (+ (bits y (1+ (* 2 i)) (* 2 i)) (chi i y)))
 
127
 
 
128
 (defun chi (i y)
 
129
   (if (zp i)
 
130
       0
 
131
     (if (>= (mu (1- i) y) 3)
 
132
         1
 
133
       0))))
 
134
 
 
135
 
 
136
(defun phi (i y)
 
137
  (if (= (bits (mu i y) 1 0) 3)
 
138
      -1
 
139
    (bits (mu i y) 1 0)))
 
140
 
 
141
(defthm phi-bnd
 
142
    (member (phi i y) '(-1 0 1 2)))
 
143
 
 
144
(defun sum-odd-powers-of-2 (m)
 
145
  (if (zp m)
 
146
      0
 
147
    (+ (expt 2 (1- (* 2 m)))
 
148
       (sum-odd-powers-of-2 (1- m)))))
 
149
 
 
150
 
 
151
(defthm chi-m
 
152
    (implies (and (natp m)
 
153
                  (natp y)
 
154
                  (<= y (sum-odd-powers-of-2 m)))
 
155
             (equal (chi m y) 0))
 
156
  :rule-classes())
 
157
 
 
158
 
 
159
(defthm phi-m-1
 
160
    (implies (and (natp m)
 
161
                  (natp y)
 
162
                  (<= y (sum-odd-powers-of-2 m)))
 
163
             (>= (phi (1- m) y) 0))
 
164
  :rule-classes())
 
165
 
 
166
(defun sum-phi (m y)
 
167
   (if (zp m)
 
168
       0
 
169
     (+ (* (expt 2 (* 2 (1- m))) (phi (1- m) y))
 
170
        (sum-phi (1- m) y))))
 
171
 
 
172
 
 
173
(defthm sum-phi-lemma
 
174
    (implies (and (natp m)
 
175
                  (natp y)
 
176
                  (<= y (sum-odd-powers-of-2 m)))
 
177
             (equal y (sum-phi m y)))
 
178
  :rule-classes ())
 
179
 
 
180
(defun pp4-phi (i x y n)
 
181
   (if (zerop i)
 
182
       (cat 1 1
 
183
            (lnot (neg (phi i y)) 1) 1
 
184
            (bmux4 (phi i y) x n) n)
 
185
     (cat 1 1
 
186
          (lnot (neg (phi i y)) 1) 1
 
187
          (bmux4 (phi i y) x n) n
 
188
          0 1
 
189
          (neg (phi (1- i) y)) 1
 
190
          0 (* 2 (1- i)))))
 
191
 
 
192
(defun sum-pp4-phi (x y m n)
 
193
  (if (zp m)
 
194
      0
 
195
    (+ (pp4-phi (1- m) x y n)
 
196
       (sum-pp4-phi x y (1- m) n))))
 
197
 
 
198
 
 
199
(defthm static-booth
 
200
    (implies (and (not (zp n))
 
201
                  (not (zp m))
 
202
                  (bvecp x (1- n))
 
203
                  (<= y (sum-odd-powers-of-2 m)))
 
204
             (= (+ (expt 2 n)
 
205
                   (sum-pp4-phi x y m n))
 
206
                (+ (expt 2 (+ n (* 2 m)))
 
207
                   (* x y))))
 
208
  :rule-classes ())
 
209
 
 
210
;;;**********************************************************************
 
211
;;;                Encoding Redundant Representations
 
212
;;;**********************************************************************
 
213
 
 
214
 
 
215
(defun gamma (i a b c)
 
216
  (if (zp i)
 
217
      c
 
218
    (lior (bitn a (1- (* 2 i)))
 
219
          (bitn b (1- (* 2 i)))
 
220
          1)))
 
221
 
 
222
 
 
223
(defun delta (i a b c d)
 
224
  (if (zp i)
 
225
      d
 
226
    (land (lior (land (bitn a (- (* 2 i) 2)) (bitn b (- (* 2 i) 2)) 1)
 
227
                (lior (land (bitn a (- (* 2 i) 2)) (gamma (1- i) a b c) 1)
 
228
                      (land (bitn b (- (* 2 i) 2)) (gamma (1- i) a b c) 1)))
 
229
          (lnot (lxor (bitn a (1- (* 2 i))) (bitn b (1- (* 2 i))) 1) 1)
 
230
          1)))
 
231
 
 
232
 
 
233
(defun psi (i a b c d)
 
234
  (+ (bits a (1+ (* 2 i)) (* 2 i))
 
235
     (bits b (1+ (* 2 i)) (* 2 i))
 
236
     (gamma i a b c)
 
237
     (delta i a b c d)
 
238
     (* -4 (+ (gamma (1+ i) a b c)
 
239
              (delta (1+ i) a b c d)))))
 
240
 
 
241
(defthm psi-m-1
 
242
    (implies (and (natp m)
 
243
                  (bvecp a (- (* 2 m) 3))
 
244
                  (bvecp b (- (* 2 m) 3))
 
245
                  (bvecp c 1)
 
246
                  (bvecp d 1))
 
247
             (and (equal (gamma m a b c) 0)
 
248
                  (equal (delta m a b c d) 0)
 
249
                  (>= (psi (1- m) a b c d) 0)))
 
250
  :rule-classes ())
 
251
 
 
252
(defun sum-psi (m a b c d)
 
253
   (if (zp m)
 
254
       0
 
255
     (+ (* (expt 2 (* 2 (1- m))) (psi (1- m) a b c d))
 
256
        (sum-psi (1- m) a b c d))))
 
257
 
 
258
 
 
259
(defthm sum-psi-lemma
 
260
    (implies (and (natp m)
 
261
                  (bvecp a (- (* 2 m) 3))
 
262
                  (bvecp b (- (* 2 m) 3))
 
263
                  (bvecp c 1)
 
264
                  (bvecp d 1))
 
265
             (equal (+ a b c d) (sum-psi m a b c d)))
 
266
  :rule-classes ())
 
267
 
 
268
 
 
269
(defthm psi-bnd
 
270
    (implies (and (natp m)
 
271
                  (bvecp a (- (* 2 m) 3))
 
272
                  (bvecp b (- (* 2 m) 3))
 
273
                  (bvecp c 1)
 
274
                  (bvecp d 1)
 
275
                  (natp i)
 
276
                  (< i m))
 
277
             (and (integerp (psi i a b c d))
 
278
                  (<= (psi i a b c d) 2)
 
279
                  (>= (psi i a b c d) -2)))
 
280
  :rule-classes ())
 
281
 
 
282
(defun pp4-psi (i x a b c d n)
 
283
   (if (zerop i)
 
284
       (cat 1 1
 
285
            (lnot (neg (psi i a b c d)) 1) 1
 
286
            (bmux4 (psi i a b c d) x n) n)
 
287
     (cat 1 1
 
288
          (lnot (neg (psi i a b c d)) 1) 1
 
289
          (bmux4 (psi i a b c d) x n) n
 
290
          0 1
 
291
          (neg (psi (1- i) a b c d)) 1
 
292
          0 (* 2 (1- i)))))
 
293
 
 
294
(defun sum-pp4-psi (x a b c d m n)
 
295
  (if (zp m)
 
296
      0
 
297
    (+ (pp4-psi (1- m) x a b c d n)
 
298
       (sum-pp4-psi x a b c d (1- m) n))))
 
299
 
 
300
 
 
301
(defthm redundant-booth
 
302
    (implies (and (natp m)
 
303
                  (bvecp a (- (* 2 m) 3))
 
304
                  (bvecp b (- (* 2 m) 3))
 
305
                  (bvecp c 1)
 
306
                  (bvecp d 1)
 
307
                  (= y (+ a b c d)))
 
308
             (= (+ (expt 2 n)
 
309
                   (sum-pp4-psi x a b c d m n))
 
310
                (+ (expt 2 (+ n (* 2 m)))
 
311
                   (* x y))))
 
312
  :rule-classes ())
 
313
 
 
314
;;;**********************************************************************
 
315
;;;                     Radix-8 Booth Encoding
 
316
;;;**********************************************************************
 
317
 
 
318
 
 
319
(defun eta (i y)
 
320
  (+ (bitn y (1- (* 3 i))) 
 
321
     (bitn y (* 3 i))
 
322
     (* 2 (bitn y (1+ (* 3 i))))
 
323
     (* -4 (bit y (+ 2 (* 3 i))))))
 
324
 
 
325
(defun sum-eta (m y)
 
326
   (if (zp m)
 
327
       0
 
328
     (+ (* (expt 2 (* 3 (1- m))) (eta (1- m) y))
 
329
        (sum-eta (1- m) y))))
 
330
 
 
331
 
 
332
(defthm sum-eta-lemma
 
333
    (implies (and (not (zp m))
 
334
                  (bvecp y (1- (* 2 m))))
 
335
             (equal y (sum-eta m y)))
 
336
  :rule-classes ())
 
337
 
 
338
 
 
339
(defun bmux8 (zeta x n)
 
340
  (case zeta
 
341
    (1  x)
 
342
    (-1 (lnot x n))
 
343
    (2  (* 2 x))
 
344
    (-2 (lnot (* 2 x) n))
 
345
    (3  (* 3 x))
 
346
    (-3 (lnot (* 3 x) n))
 
347
    (4  (* 4 x))
 
348
    (-4 (lnot (* 4 x) n))
 
349
    (0  0)))
 
350
 
 
351
(encapsulate ((xi (i) t))
 
352
 (local (defun xi (i) (declare (ignore i)) 0))
 
353
 (defthm xi-bnd 
 
354
     (and (integerp (xi i))
 
355
          (<= (xi i) 4)
 
356
          (>= (xi i) -4))))
 
357
 
 
358
 
 
359
(defun pp8 (i x n)
 
360
  (if (zerop i)
 
361
      (cat 3 2
 
362
           (lnot (neg (xi i)) 1) 1
 
363
           (bmux8 (xi i) x n) n)
 
364
    (cat 3 2
 
365
         (lnot (neg (xi i)) 1) 1
 
366
         (bmux4 (xi i) x n) n
 
367
         0 2
 
368
         (neg (xi (1- i))) 1
 
369
         0 (* 3 (1- i)))))
 
370
 
 
371
(defun sum-xi (m)
 
372
  (if (zp m)
 
373
      0
 
374
    (+ (* (expt 2 (* 3 (1- m))) (xi (1- m)))
 
375
       (sum-xi (1- m)))))   
 
376
 
 
377
(defun sum-pp8 (x m n)
 
378
  (if (zp m)
 
379
      0
 
380
    (+ (pp8 (1- m) x n)
 
381
       (sum-pp8 x (1- m) n))))
 
382
 
 
383
 
 
384
(defthm booth8-thm
 
385
    (implies (and (not (zp n))
 
386
                  (not (zp m))
 
387
                  (bvecp x (- n 2)))
 
388
             (= (+ (expt 2 n)
 
389
                   (sum-pp8 x m n))
 
390
                (+ (expt 2 (+ n (* 3 m)))
 
391
                   (* x (sum-xi m))
 
392
                   (- (* (expt 2 (* 3 (1- m))) (neg (xi (1- m))))))))
 
393
  :rule-classes ())
 
394
 
 
395
(defun pp8-eta (i x y n)
 
396
  (if (zerop i)
 
397
      (cat 3 2
 
398
           (lnot (neg (eta i y)) 1) 1
 
399
           (bmux8 (eta i y) x n) n)
 
400
    (cat 3 2
 
401
         (lnot (neg (eta i y)) 1) 1
 
402
         (bmux8 (eta i y) x n) n
 
403
         0 2
 
404
         (neg (eta (1- i) y)) 1
 
405
         0 (* 3 (1- i)))))
 
406
 
 
407
(defun sum-pp8-eta (x y m n)
 
408
  (if (zp m)
 
409
      0
 
410
    (+ (pp8-eta (1- m) x y n)
 
411
       (sum-pp8-eta x y (1- m) n))))
 
412
 
 
413
 
 
414
(defthm booth8-corollary
 
415
    (implies (and (not (zp n))
 
416
                  (not (zp m))
 
417
                  (bvecp x (- n 2))
 
418
                  (bvecp y (1- (* 3 m))))
 
419
             (= (+ (expt 2 n)
 
420
                   (sum-pp8-eta x y m n))
 
421
                (+ (expt 2 (+ n (* 3 m)))
 
422
                   (* x y))))
 
423
  :rule-classes ())
 
424