← 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-designwires.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-designwires.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 "../parsetree")
33
 
(local (include-book "../util/arithmetic"))
34
 
 
35
 
(defxdoc designwires
36
 
  :parents (transforms)
37
 
  :short "Introduce @('VL_DESIGN_WIRE') annotations that say which wires/regs
38
 
were in the original Verilog modules."
39
 
 
40
 
  :long "<p>This transform lets you distinguish between:</p>
41
 
 
42
 
<ul>
43
 
<li>wires that are really present and visible in the design, and</li>
44
 
<li>wires that VL added in transforms like @(see split) and @(see occform).</li>
45
 
</ul>
46
 
 
47
 
<p>This transform should typically be run very early.  It just annotates every
48
 
net and reg declaration with a @('VL_DESIGN_WIRE') <see topic='@(url
49
 
vl-atts-p)'>attribute</see>.</p>
50
 
 
51
 
<p>When temporary wires are added to the module by subsequent VL transforms,
52
 
they will not have this attribute.  Hence, you can check for this attribute to
53
 
tell whether a wire was in the original design.</p>")
54
 
 
55
 
(local (xdoc::set-default-parents designwires))
56
 
 
57
 
(define vl-netdecl-designwires ((x vl-netdecl-p))
58
 
  :returns (new-x vl-netdecl-p :hyp :fguard)
59
 
  :short "Add a @('VL_DESIGN_WIRE') attribute to a @(see vl-netdecl-p)."
60
 
  (b* (((vl-netdecl x) x)
61
 
       ((when (assoc-equal "VL_DESIGN_WIRE" x.atts))
62
 
        ;; For idempotency, don't add it again.
63
 
        x)
64
 
       (atts (acons "VL_DESIGN_WIRE" nil x.atts)))
65
 
    (change-vl-netdecl x :atts atts)))
66
 
 
67
 
(defprojection vl-netdecllist-designwires (x)
68
 
  (vl-netdecl-designwires x)
69
 
  :guard (vl-netdecllist-p x)
70
 
  :result-type vl-netdecllist-p
71
 
  :nil-preservingp nil)
72
 
 
73
 
(define vl-vardecl-designwires ((x vl-vardecl-p))
74
 
  :returns (new-x vl-vardecl-p :hyp :fguard)
75
 
  :short "Add a @('VL_DESIGN_WIRE') attribute to a @(see vl-vardecl-p)."
76
 
  (b* (((vl-vardecl x) x)
77
 
       ((when (assoc-equal "VL_DESIGN_WIRE" x.atts))
78
 
        ;; For idempotency, don't add it again.
79
 
        x)
80
 
       (atts (acons "VL_DESIGN_WIRE" nil x.atts)))
81
 
    (change-vl-vardecl x :atts atts)))
82
 
 
83
 
(defprojection vl-vardecllist-designwires (x)
84
 
  (vl-vardecl-designwires x)
85
 
  :guard (vl-vardecllist-p x)
86
 
  :result-type vl-vardecllist-p
87
 
  :nil-preservingp nil)
88
 
 
89
 
(define vl-module-designwires ((x vl-module-p))
90
 
  :returns (new-x vl-module-p :hyp :fguard)
91
 
  :short "Add a @('VL_DESIGN_WIRE') attribute to every net and reg declaration
92
 
in a module."
93
 
  (b* (((vl-module x) x)
94
 
       ((when (vl-module->hands-offp x))
95
 
        x))
96
 
    (change-vl-module x
97
 
                      :netdecls (vl-netdecllist-designwires x.netdecls)
98
 
                      :vardecls (vl-vardecllist-designwires x.vardecls))))
99
 
 
100
 
(defprojection vl-modulelist-designwires (x)
101
 
  (vl-module-designwires x)
102
 
  :guard (vl-modulelist-p x)
103
 
  :result-type vl-modulelist-p
104
 
  :nil-preservingp nil)
105
 
 
106
 
(define vl-design-designwires ((x vl-design-p))
107
 
  :returns (new-x vl-design-p)
108
 
  (b* ((x (vl-design-fix x))
109
 
       ((vl-design x) x))
110
 
    (change-vl-design x :mods (vl-modulelist-designwires x.mods))))