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))
|