← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/xf-portdecl-sign.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/transforms/xf-portdecl-sign.lisp
1
 
; VL Verilog Toolkit
2
 
; Copyright (C) 2008-2011 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 "../mlib/range-tools")
33
 
(local (include-book "../util/arithmetic"))
34
 
(local (include-book "../util/osets"))
35
 
(local (std::add-default-post-define-hook :fix))
36
 
 
37
 
(defxdoc portdecl-sign
38
 
  :parents (transforms)
39
 
  :short "Cross-propagate signedness between net/reg and port declarations."
40
 
 
41
 
  :long "<p>This transformation ensures that each port declaration and its
42
 
corresponding net declaration have the same signedness.</p>
43
 
 
44
 
<p>A Verilog module may include both a port declaration and a net/reg
45
 
declaration for the same wire.  For instance, the following is valid:</p>
46
 
 
47
 
@({
48
 
module mymod (a, b, c, ...) ;
49
 
  input [3:0] a;   // <-- port declaration
50
 
  wire [3:0] a;    // <-- net declaration
51
 
endmodule
52
 
})
53
 
 
54
 
<p>Indeed, if a port is not also given a net declaration, we infer one
55
 
in the @(see make-implicit-wires) transform.</p>
56
 
 
57
 
<p>According to the Verilog-2005 specification (page 175),</p>
58
 
 
59
 
<box>
60
 
<p>\"The signed attribute can be attached to either a port declaration or to
61
 
the corresponding net or reg declaration or to both.  If either the port or
62
 
the net/reg is declared as signed, then the other shall also be considered
63
 
signed.\"</p>
64
 
</box>
65
 
 
66
 
<p>Our @(see parser) does not do this cross-checking, so in this transformation
67
 
we cross-check the port declarations against the net/reg declarations and
68
 
propagate any signed attributes to ensure they are found in both
69
 
declarations.</p>")
70
 
 
71
 
(local (xdoc::set-default-parents portdecl-sign))
72
 
 
73
 
(define vl-signed-portdecls ((x vl-portdecllist-p))
74
 
  :returns (names string-listp)
75
 
  :short "Gather the names of any signed port declarations."
76
 
  (cond ((atom x)
77
 
         nil)
78
 
        ((vl-portdecl->signedp (car x))
79
 
         (cons (vl-portdecl->name (car x))
80
 
               (vl-signed-portdecls (cdr x))))
81
 
        (t
82
 
         (vl-signed-portdecls (cdr x)))))
83
 
 
84
 
(define vl-signed-netdecls ((x vl-netdecllist-p))
85
 
  :returns (names string-listp)
86
 
  :short "Gather the names of any signed net declarations."
87
 
  (cond ((atom x)
88
 
         nil)
89
 
        ((vl-netdecl->signedp (car x))
90
 
         (cons (vl-netdecl->name (car x))
91
 
               (vl-signed-netdecls (cdr x))))
92
 
        (t
93
 
         (vl-signed-netdecls (cdr x)))))
94
 
 
95
 
(define vl-signed-vardecls ((x vl-vardecllist-p))
96
 
  :returns (names string-listp)
97
 
  :short "Gather the names of any signed reg declarations."
98
 
  :long "<p>Note that we really only look at @('reg') declarations here.  While
99
 
things like @('integer') variables are signed, they can't be used as ports in
100
 
Verilog-2005.  (Is that still true in SystemVerilog?)</p>
101
 
 
102
 
<p>BOZO probably this isn't correct at all for SystemVerilog, but we're going
103
 
to have to really extend ports to deal with modports stuff anyway, so let's
104
 
just go with it for now.</p>"
105
 
  (cond ((atom x)
106
 
         nil)
107
 
        ((and (vl-simplereg-p (car x))
108
 
              (vl-simplereg->signedp (car x)))
109
 
         (cons (vl-vardecl->name (car x))
110
 
               (vl-signed-vardecls (cdr x))))
111
 
        (t
112
 
         (vl-signed-vardecls (cdr x)))))
113
 
 
114
 
(define vl-make-portdecls-signed
115
 
  ((names "names of portdecls to make signed" string-listp)
116
 
   (x     "original portdecls"                vl-portdecllist-p))
117
 
  :returns (new-x vl-portdecllist-p)
118
 
  :short "Change some port declarations to make them signed."
119
 
  (b* ((names   (string-list-fix names))
120
 
       ((when (atom x))
121
 
        nil)
122
 
       (x1     (vl-portdecl-fix (car x)))
123
 
       (new-x1 (if (member-equal (vl-portdecl->name x1) names)
124
 
                   (change-vl-portdecl x1 :signedp t)
125
 
                 x1)))
126
 
    (cons new-x1 (vl-make-portdecls-signed names (cdr x)))))
127
 
 
128
 
(define vl-make-netdecls-signed
129
 
  ((names "names of netdecls to make signed" string-listp)
130
 
   (x     "original netdecls"                vl-netdecllist-p))
131
 
  :returns (new-x vl-netdecllist-p)
132
 
  :short "Change some net declarations to make them signed."
133
 
  (b* ((names (string-list-fix names))
134
 
       ((when (atom x))
135
 
        nil)
136
 
       (x1     (vl-netdecl-fix (car x)))
137
 
       (new-x1 (if (member-equal (vl-netdecl->name x1) names)
138
 
                   (change-vl-netdecl x1 :signedp t)
139
 
                 x1)))
140
 
    (cons new-x1 (vl-make-netdecls-signed names (cdr x)))))
141
 
 
142
 
(define vl-make-vardecls-signed
143
 
  ((names "names of vardecls to make signed" string-listp)
144
 
   (x     "original vardecls"                vl-vardecllist-p))
145
 
  :returns (new-x vl-vardecllist-p)
146
 
  :short "Change some variable declarations to make them signed."
147
 
  :guard-hints(("Goal" :in-theory (enable vl-simplereg-p)))
148
 
  :measure (len x)
149
 
  (b* ((names (string-list-fix names))
150
 
       ((when (atom x))
151
 
        nil)
152
 
       (x1     (vl-vardecl-fix (car x)))
153
 
       ((unless (member-equal (vl-vardecl->name x1) names))
154
 
        (cons x1 (vl-make-vardecls-signed names (cdr x))))
155
 
       ((unless (vl-simplereg-p x1))
156
 
        (raise "Expected a simple register but found ~x0." x1))
157
 
       (new-x1 (change-vl-vardecl x1
158
 
                                  :vartype (change-vl-coretype (vl-vardecl->vartype x1)
159
 
                                                               :signedp t))))
160
 
    (cons new-x1 (vl-make-vardecls-signed names (cdr x)))))
161
 
 
162
 
(define vl-module-portdecl-sign ((x vl-module-p))
163
 
  :returns (new-x vl-module-p)
164
 
  :short "Cross-propagate @('signed') declarations between port declarations
165
 
and net/reg declarations in a module."
166
 
 
167
 
; I'm really happy with how simple and efficient this is. I particularly like
168
 
; how we aren't trying to match up particular ports with the corresponding
169
 
; net/reg declarations.
170
 
 
171
 
    (b* ((x (vl-module-fix x))
172
 
         ((vl-module x) x)
173
 
 
174
 
         ((when (vl-module->hands-offp x))
175
 
          x)
176
 
 
177
 
; We begin by just collecting all the ports, nets, and regs that are signed.
178
 
; At Centaur, signed stuff is almost never used, so in practice the following
179
 
; often just does a quick scan of the declarations and doesn't result in any
180
 
; consing at all.
181
 
 
182
 
         (signed-ports (mergesort (vl-signed-portdecls x.portdecls)))
183
 
         (signed-nets  (mergesort (vl-signed-netdecls x.netdecls)))
184
 
         (signed-vars  (mergesort (vl-signed-vardecls x.vardecls)))
185
 
 
186
 
; Optimization.  If nothing is signed, nothing needs to be done.
187
 
 
188
 
         ((unless (or signed-ports signed-nets signed-vars))
189
 
          x)
190
 
 
191
 
; Otherwise there are at least some signed wires, so we need to do the checks.
192
 
; Any ports whose corresponding reg/net is declared to be signed, but which is
193
 
; not itself signed, needs to be fixed.
194
 
 
195
 
         (ports-to-fix (union (difference signed-nets signed-ports)
196
 
                              (difference signed-vars signed-ports)))
197
 
 
198
 
; Any net or reg whose corresponding port is signed, but which is not itself
199
 
; signed, needs to be fixed.
200
 
 
201
 
         (nets-to-fix  (difference signed-ports signed-nets))
202
 
         (vars-to-fix  (difference signed-ports signed-vars))
203
 
 
204
 
; Optimization.  We may have found that nothing needs to be fixed because the
205
 
; signedness for all port and net/reg declarations already agrees.  In this
206
 
; case, we don't need to change the module at all, so we can stop now and do no
207
 
; more consing.
208
 
 
209
 
         ((unless (or ports-to-fix nets-to-fix vars-to-fix))
210
 
          x)
211
 
 
212
 
; Otherwise, we can't avoid the re-consing, so carry out the fixes and return
213
 
; the updated module.
214
 
 
215
 
         (new-portdecls (if ports-to-fix
216
 
                            (vl-make-portdecls-signed ports-to-fix x.portdecls)
217
 
                          x.portdecls))
218
 
         (new-netdecls (if nets-to-fix
219
 
                           (vl-make-netdecls-signed nets-to-fix x.netdecls)
220
 
                         x.netdecls))
221
 
         (new-vardecls (if vars-to-fix
222
 
                           (vl-make-vardecls-signed vars-to-fix x.vardecls)
223
 
                         x.vardecls)))
224
 
 
225
 
      (change-vl-module x
226
 
                        :portdecls new-portdecls
227
 
                        :netdecls  new-netdecls
228
 
                        :vardecls  new-vardecls))
229
 
 
230
 
    ///
231
 
    (defthm vl-module->name-of-vl-module-portdecl-sign
232
 
      (equal (vl-module->name (vl-module-portdecl-sign x))
233
 
             (vl-module->name x))))
234
 
 
235
 
(defprojection vl-modulelist-portdecl-sign ((x vl-modulelist-p))
236
 
  :returns (new-x vl-modulelist-p)
237
 
  (vl-module-portdecl-sign x))
238
 
 
239
 
(define vl-design-portdecl-sign
240
 
  :short "Top-level @(see portdecl-sign) transform."
241
 
  ((x vl-design-p))
242
 
  :returns (new-x vl-design-p)
243
 
  (b* (((vl-design x) x))
244
 
    (change-vl-design x :mods (vl-modulelist-portdecl-sign x.mods))))