File: fast-zero.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (107 lines) | stat: -rw-r--r-- 3,448 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
;; Copyright (C) 2017, Regents of the University of Texas
;; Written by Cuong Chau (derived from the FM9001 work of Brock and Hunt)
;; License: A 3-clause BSD license.  See the LICENSE file distributed with
;; ACL2.

;; The ACL2 source code for the FM9001 work is available at
;; https://github.com/acl2/acl2/tree/master/books/projects/fm9001.

;; Cuong Chau <ckcuong@cs.utexas.edu>
;; January 2019

;; A zero detector optimized for quick detection of the last 2 bits of the
;; input vector.  It should save a few nanoseconds in the FM9001.

;; LSI Logic timing analysis of the final design showed that this "fast"
;; zero-detector was about the same as simple, fully-balanced zero-detectors
;; defined in "t-or-nor.lisp".

(in-package "ADE")

(include-book "t-or-nor")

;; ======================================================================

(defun f$fast-zero (v)
  (f-nor3 (tr-or-nor (take (- (len v) 2) v)
                     nil
                     (make-tree (- (len v) 2)))
          (nth (- (len v) 2) v)
          (nth (1- (len v)) v)))

(defthm f$fast-zero-of-v-threefix-canceled
  (equal (f$fast-zero (v-threefix v))
         (f$fast-zero v)))

(defthm f$fast-zero=tr-or-nor
  (implies (>= (len v) 3)
           (equal (f$fast-zero v)
                  (tr-or-nor v t (cons (make-tree (- (len v) 2))
                                       (cons 0 0)))))
  :hints (("Goal" :in-theory (enable tr-or-nor f-nor3 f-nor
                                     car-nthcdr cdr-nthcdr))))

(defthm f$fast-zero=v-zp
  (implies (and (bvp v)
                (>= (len v) 3))
           (equal (f$fast-zero v)
                  (v-zp v)))
  :hints (("Goal" :in-theory (enable tree-size))))

(in-theory (disable f$fast-zero))

;; Hardware

(module-generator
 fast-zero* (n)
 (si 'fast-zero n)
 (sis 'a 0 n)
 '(z)
 nil
 (list
  (list 'front '(zfront) (si 't-or (tree-number (make-tree (1- (1- n)))))
        (take (- n 2) (sis 'a 0 n)))
  (list 'result '(z) 'b-nor3
        (list 'zfront (si 'a (- n 2)) (si 'a (1- n)))))
 (declare (xargs :guard (and (natp n) (<= 2 n)))))

(defund fast-zero$netlist (n)
  (declare (xargs :guard (and (natp n)
                              (<= 2 n))))
  (cons (fast-zero* n)
        (t-or-nor$netlist (make-tree (- n 2)) nil)))

(defund fast-zero& (netlist n)
  (declare (xargs :guard (and (alistp netlist)
                              (natp n)
                              (<= 2 n))))
  (b* ((subnetlist (delete-to-eq (si 'fast-zero n) netlist)))
    (and (equal (assoc (si 'fast-zero n) netlist)
                (fast-zero* n))
         (t-or-nor& subnetlist (make-tree (- n 2)) nil))))

(defthm check-fast-zero$netlist-5
  (fast-zero& (fast-zero$netlist 5) 5))

(defthm fast-zero$value
  (implies (and (fast-zero& netlist n)
                (equal (len v) n)
                (>= n 3))
           (equal (se (si 'fast-zero n) v st netlist)
                  (list (f$fast-zero v))))
  :hints (("Goal"
           :expand (:free (v n)
                          (se (si 'fast-zero n) v st netlist))
           :in-theory (e/d (de-rules
                            fast-zero&
                            fast-zero*$destructure
                            tr-or-nor
                            f-nor3
                            f-nor
                            car-nthcdr
                            cdr-nthcdr)
                           (de-module-disabled-rules)))))

(in-theory (disable f$fast-zero=tr-or-nor))