← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/vl/mlib/hierarchy-basic.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/vl/mlib/hierarchy-basic.lisp
 
1
; VL Verilog Toolkit
 
2
; Copyright (C) 2008-2014 Centaur Technology
 
3
;
 
4
; Contact:
 
5
;   Centaur Technology Formal Verification Group
 
6
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
 
7
;   http://www.centtech.com/
 
8
;
 
9
; License: (An MIT/X11-style license)
 
10
;
 
11
;   Permission is hereby granted, free of charge, to any person obtaining a
 
12
;   copy of this software and associated documentation files (the "Software"),
 
13
;   to deal in the Software without restriction, including without limitation
 
14
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
15
;   and/or sell copies of the Software, and to permit persons to whom the
 
16
;   Software is furnished to do so, subject to the following conditions:
 
17
;
 
18
;   The above copyright notice and this permission notice shall be included in
 
19
;   all copies or substantial portions of the Software.
 
20
;
 
21
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
22
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
23
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
24
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
25
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
26
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
27
;   DEALINGS IN THE SOFTWARE.
 
28
;
 
29
; Original author: Jared Davis <jared@centtech.com>
 
30
 
 
31
(in-package "VL")
 
32
(include-book "blocks")
 
33
(include-book "find")
 
34
(local (include-book "../util/arithmetic"))
 
35
(local (std::add-default-post-define-hook :fix))
 
36
 
 
37
 
 
38
(def-genblob-transform vl-genblob->flatten-modinsts ((acc vl-modinstlist-p))
 
39
  :no-new-x t
 
40
  :returns ((acc vl-modinstlist-p))
 
41
  :apply-to-generates vl-generates->flatten-modinsts
 
42
  :prepwork ((local (in-theory (disable ;; vl-genelement-p-by-tag-when-vl-scopeitem-p
 
43
                                        vl-modinstlist-p-when-not-consp
 
44
                                        (tau-system)
 
45
                                        append
 
46
                                        vl-modinstlist-p-when-subsetp-equal))))
 
47
  (vl-generates->flatten-modinsts (vl-genblob->generates x)
 
48
                                  (append-without-guard
 
49
                                   (vl-genblob->modinsts x)
 
50
                                   (vl-modinstlist-fix acc))))
 
51
 
 
52
(define vl-module->flatten-modinsts ((x vl-module-p))
 
53
  :parents (vl-modulelist-everinstanced)
 
54
  :short "Gather modinsts from the module, including its generate blocks."
 
55
  :returns (modinsts vl-modinstlist-p)
 
56
  (b* ((genblob (vl-module->genblob x)))
 
57
    (vl-genblob->flatten-modinsts genblob nil)))
 
58
 
 
59
(defprojection vl-interfaceportlist->ifnames ((x vl-interfaceportlist-p))
 
60
  :returns (names string-listp)
 
61
  (vl-interfaceport->ifname x))
 
62
 
 
63
 
 
64
 
 
65
(define vl-modulelist-everinstanced-nrev ((x vl-modulelist-p)
 
66
                                          (nrev))
 
67
  :parents (vl-modulelist-everinstanced)
 
68
  (b* (((when (atom x))
 
69
        (nrev-fix nrev))
 
70
       (modinsts1 (vl-module->flatten-modinsts (car x)))
 
71
       (ifports1  (vl-module->ifports (car x)))
 
72
       (nrev      (vl-modinstlist->modnames-nrev modinsts1 nrev))
 
73
       (nrev      (vl-interfaceportlist->ifnames-nrev ifports1 nrev)))
 
74
    (vl-modulelist-everinstanced-nrev (cdr x) nrev)))
 
75
 
 
76
(define vl-modulelist-everinstanced ((x vl-modulelist-p))
 
77
  :parents (hierarchy)
 
78
  :short "Gather the names of every module and interface ever instanced in a
 
79
  module list or used in an interface port."
 
80
 
 
81
  :long "<p>The returned list typically will contain a lot of duplicates.  This
 
82
is fairly expensive, requiring a cons for every single module instance.  We
 
83
optimize it to avoid the construction of intermediate lists and to use @(see
 
84
nrev).</p>"
 
85
 
 
86
  :returns (names string-listp)
 
87
  :enabled t
 
88
  (mbe :logic
 
89
       (b* (((when (atom x))
 
90
             nil)
 
91
            (modinsts1 (vl-module->flatten-modinsts (car x)))
 
92
            (ifports1  (vl-module->ifports (car x))))
 
93
         (append (vl-modinstlist->modnames modinsts1)
 
94
                 (vl-interfaceportlist->ifnames ifports1)
 
95
                 (vl-modulelist-everinstanced (cdr x))))
 
96
       :exec
 
97
       (with-local-nrev (vl-modulelist-everinstanced-nrev x nrev)))
 
98
  :verify-guards nil
 
99
  ///
 
100
  (defthm vl-modulelist-everinstanced-nrev-removal
 
101
    (equal (vl-modulelist-everinstanced-nrev x nrev)
 
102
           (append nrev (vl-modulelist-everinstanced x)))
 
103
    :hints(("Goal" :in-theory (enable vl-modulelist-everinstanced-nrev))))
 
104
 
 
105
  (verify-guards vl-modulelist-everinstanced))
 
106
 
 
107
 
 
108
;; (define vl-modulelist-missing
 
109
;;   :parents (hierarchy missing)
 
110
;;   :short "@(call vl-modulelist-missing) gathers the names of any modules which
 
111
;; are instantiated in the module list @('x') but are not defined in
 
112
;; @('x'), and returns them as an ordered set."
 
113
 
 
114
;;   ((x vl-modulelist-p))
 
115
;;   :returns (names string-listp)
 
116
 
 
117
;;   (mbe :logic
 
118
;;        (let ((mentioned (mergesort (vl-modulelist-everinstanced x)))
 
119
;;              (defined   (mergesort (vl-modulelist->names x))))
 
120
;;          (difference mentioned defined))
 
121
;;        :exec
 
122
 
 
123
;; ; Some minor optimizations.
 
124
 
 
125
;; ; Historically, since we're sorting the instnames anyway, we don't need to pay
 
126
;; ; the price of reversing them and can just use the exec function directly.  Now
 
127
;; ; that we're using nrev I don't bother to do this.
 
128
 
 
129
;;        (let* ((mentioned (mergesort (vl-modulelist-everinstanced x)))
 
130
 
 
131
;; ; Also, since we often work with sets of modules, we can try to avoid
 
132
;; ; mergesorting the names when they are known to be a set.  At best, this
 
133
;; ; allows us to avoid sorting the module names, and hence saves a bunch of
 
134
;; ; consing.
 
135
;; ;
 
136
;; ; Of course, when this fails we incur the additional price of a setp check,
 
137
;; ; which in principle is as bad as O(n) comparisons.  On the other hand, setp
 
138
;; ; can fail early.  It seems likely that an unordered list will have elements
 
139
;; ; near its head that are out of order.  So, even when the setp check fails, it
 
140
;; ; may often be that it fails pretty quickly.
 
141
 
 
142
;;               (names     (vl-modulelist->names x))
 
143
;;               (defined   (redundant-mergesort names)))
 
144
;;          (difference mentioned defined)))
 
145
;;   ///
 
146
;;   (defthm true-listp-of-vl-modulelist-missing
 
147
;;     (true-listp (vl-modulelist-missing x))
 
148
;;     :rule-classes :type-prescription)
 
149
 
 
150
;;   (defthm setp-of-vl-modulelist-missing
 
151
;;     (setp (vl-modulelist-missing x))))
 
152
 
 
153
 
 
154
(define vl-modulelist-toplevel
 
155
  :parents (hierarchy)
 
156
  :short "@(call vl-modulelist-toplevel) gathers the names of any modules that
 
157
are defined in the module list @('x') but are never instantiated in @('x'), and
 
158
returns them as an ordered set."
 
159
 
 
160
  ((x vl-modulelist-p))
 
161
  :returns (names string-listp)
 
162
 
 
163
  (mbe :logic
 
164
       (let ((mentioned (mergesort (vl-modulelist-everinstanced x)))
 
165
             (defined   (mergesort (vl-modulelist->names x))))
 
166
         (difference defined mentioned))
 
167
       :exec
 
168
       ;; Optimizations as in vl-modulelist-missing
 
169
       (let* ((mentioned (mergesort (vl-modulelist-everinstanced x)))
 
170
              (names     (vl-modulelist->names x))
 
171
              (defined   (if (setp names) names (mergesort names))))
 
172
         (difference defined mentioned)))
 
173
  ///
 
174
  (defthm true-listp-of-vl-modulelist-toplevel
 
175
    (true-listp (vl-modulelist-toplevel x))
 
176
    :rule-classes :type-prescription)
 
177
 
 
178
  (defthm setp-of-vl-modulelist-toplevel
 
179
    (setp (vl-modulelist-toplevel x)))
 
180
 
 
181
  ;; (defthm vl-has-modules-of-vl-modulelist-toplevel
 
182
  ;;   (implies (vl-modulelist-complete-p mods mods)
 
183
  ;;            (subsetp-equal (vl-modulelist-toplevel mods)
 
184
  ;;                           (vl-modulelist->names mods)))
 
185
  ;;   :hints((set-reasoning)))
 
186
  )
 
187
 
 
188
 
 
189
 
 
190
;; (define vl-modulelist-highlevel
 
191
;;   :parents (hierarchy)
 
192
;;   :short "@(call vl-modulelist-highlevel) gathers the names of any \"high
 
193
;; level\" modules and return them as an ordered set."
 
194
 
 
195
;;   ((x vl-modulelist-p)
 
196
;;    (n natp "How many levels from the top to consider."))
 
197
 
 
198
;;   :returns (names string-listp)
 
199
 
 
200
;;   :long "<p>We say a module is <b>top level</b> (@(see vl-modulelist-toplevel))
 
201
;; when it is never instantiated by another module.  Similarly, we say that
 
202
;; modules are <b>high level</b> when they are \"near the top level\".</p>
 
203
 
 
204
;; <p>@(call vl-modulelist-highlevel) gathers the names of all modules which are
 
205
;; within @('n') levels of the top.  When @('n') is relatively small,
 
206
;; these modules are possibly the \"big units\" in the chip.</p>
 
207
 
 
208
;; <p>Historic note.  This function was once used in the \"unreasonable modules
 
209
;; report.\" It may not be in use any more.</p>"
 
210
 
 
211
;;   :verify-guards nil
 
212
;;   (b* (((when (zp n))
 
213
;;         nil)
 
214
;;        (top (vl-modulelist-toplevel x)))
 
215
;;     (union top
 
216
;;            (vl-modulelist-highlevel (vl-delete-modules top x)
 
217
;;                                     (- n 1))))
 
218
;;   ///
 
219
;;   (defthm true-listp-of-vl-modulelist-highlevel
 
220
;;     (true-listp (vl-modulelist-highlevel x n))
 
221
;;     :rule-classes :type-prescription
 
222
;;     :hints(("Goal" :in-theory (disable (force)))))
 
223
 
 
224
;;   (defthm setp-of-vl-modulelist-highlevel
 
225
;;     (setp (vl-modulelist-highlevel x n)))
 
226
 
 
227
;;   (verify-guards vl-modulelist-highlevel))