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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(in-package "ACL2")
(set-inhibit-warnings "THEORY" "DISABLE" "NON-REC")
(include-book "rtl/rel4/lib/rtl" :dir :system)
(include-book "rtl/rel4/lib/rtlarr" :dir :system)
(include-book "rtl/rel4/lib/util" :dir :system)
(include-book "misc/symbol-btree" :dir :system)
(include-book "misc/rtl-untranslate" :dir :system)
(deftheory rtl-operators-after-macro-expansion
*rtl-operators-after-macro-expansion*)
(local
(in-theory
(set-difference-theories (current-theory :here)
(theory 'rtl-operators-after-macro-expansion))))
(defmacro ww (n) (list 'ww$ n '$path))
(defmacro sel (n) (list 'sel$ n '$path))
(defmacro in3 (n) (list 'in3$ n '$path))
(defmacro in2 (n) (list 'in2$ n '$path))
(defmacro in1 (n) (list 'in1$ n '$path))
(defmacro in0 (n) (list 'in0$ n '$path))
(ENCAPSULATE
(
(ww$ (n $path) t)
(sel$ (n $path) t)
(in3$ (n $path) t)
(in2$ (n $path) t)
(in1$ (n $path) t)
(in0$ (n $path) t)
)
(local (defun ww$ (n $path)
(declare (ignore n $path))
0))
(local (defun sel$ (n $path)
(declare (ignore n $path))
0))
(local (defun in3$ (n $path)
(declare (ignore n $path))
0))
(local (defun in2$ (n $path)
(declare (ignore n $path))
0))
(local (defun in1$ (n $path)
(declare (ignore n $path))
0))
(local (defun in0$ (n $path)
(declare (ignore n $path))
0))
(defbvecp ww (n) 3)
(defbvecp sel (n) 2)
(defbvecp in3 (n) 1)
(defbvecp in2 (n) 1)
(defbvecp in1 (n) 1)
(defbvecp in0 (n) 1)
)
(add-macro-alias ww ww$)
(add-macro-alias sel sel$)
(add-macro-alias in3 in3$)
(add-macro-alias in2 in2$)
(add-macro-alias in1 in1$)
(add-macro-alias in0 in0$)
(deflabel start-of-loop-defs)
(set-ignore-ok t)
(set-irrelevant-formals-ok t)
(deflabel end-of-loop-defs)
(deflabel start-of-clock-defs)
(defun clk (n)
(declare (ignore n))
1)
(deflabel end-of-clock-defs)
(deftheory loop-defs
(set-difference-theories (current-theory 'end-of-loop-defs)
(current-theory 'start-of-loop-defs)))
(deftheory
clock-defs
(set-difference-theories
(union-theories (function-theory 'end-of-clock-defs)
(executable-counterpart-theory 'end-of-clock-defs))
(union-theories (function-theory 'start-of-clock-defs)
(executable-counterpart-theory 'start-of-clock-defs))))
(table rtl-tbl 'sigs-btree
(symbol-alist-to-btree
(dollar-alist '(ww sel in3 in2 in1 in0
out1 FOO$RAW::OUT1 out2 FOO$RAW::OUT2)
nil)))
|
