OpenCores
URL https://opencores.org/ocsvn/wb2axip/wb2axip/trunk

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [bench/] [formal/] [Makefile] - Blame information for rev 16

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 10 dgisselq
################################################################################
2
##
3
## Filename:    Makefile
4
##
5
## Project:     Pipelined Wishbone to AXI converter
6
##
7
## Purpose:     To direct the formal verification of the bus bridge
8
##              sources.
9
##
10
## Targets:     The default target, all, tests all of the components defined
11
##              within this module.
12
##
13
## Creator:     Dan Gisselquist, Ph.D.
14
##              Gisselquist Technology, LLC
15
##
16
################################################################################
17
##
18 16 dgisselq
## Copyright (C) 2017-2018, Gisselquist Technology, LLC
19 10 dgisselq
##
20 16 dgisselq
## This file is part of the pipelined Wishbone to AXI converter project, a
21
## project that contains multiple bus bridging designs and formal bus property
22
## sets.
23 10 dgisselq
##
24 16 dgisselq
## The bus bridge designs and property sets are free RTL designs: you can
25
## redistribute them and/or modify any of them under the terms of the GNU
26
## Lesser General Public License as published by the Free Software Foundation,
27
## either version 3 of the License, or (at your option) any later version.
28 10 dgisselq
##
29 16 dgisselq
## The bus bridge designs and property sets are distributed in the hope that
30
## they will be useful, but WITHOUT ANY WARRANTY; without even the implied
31
## warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
32
## GNU Lesser General Public License for more details.
33
##
34
## You should have received a copy of the GNU Lesser General Public License
35
## along with these designs.  (It's in the $(ROOT)/doc directory.  Run make
36
## with no target there if the PDF file isn't present.)  If not, see
37 10 dgisselq
##  for a copy.
38
##
39 16 dgisselq
## License:     LGPL, v3, as defined and found on www.gnu.org,
40
##              http://www.gnu.org/licenses/lgpl.html
41 10 dgisselq
##
42
################################################################################
43
##
44
##
45 16 dgisselq
TESTS := wbarbiter wbm2axilite axilrd2wbsp axilwr2wbsp demoaxi axlite2wbsp wbxbar # wbm2axisp axim2wbsp
46 10 dgisselq
.PHONY: $(TESTS)
47
all: $(TESTS)
48
RTL := ../../rtl
49
SMTBMC  := yosys-smtbmc
50
# SOLVER  := -s z3
51
SOLVER  := -s yices
52
# SOLVER  := -s boolector
53
BMCARGS := --presat $(SOLVER)
54
# BMCARGS := $(SOLVER)
55
INDARGS := $(SOLVER) -i
56
 
57 16 dgisselq
DEMOAXI    := demoaxi
58
WBARB      := wbarbiter
59
WB2AXI     := wbm2axisp
60
AXI2WB     := axim2wbsp
61
WB2LITE    := wbm2axilite
62
RDLITE     := axilrd2wbsp
63
WRLITE     := axilwr2wbsp
64
AXLITE     := axlite2wbsp
65
XILINXDEMO := xlnxdemo
66
WBXBAR     := wbxbar
67
WBXBAR4x8  := wbxbar4x8
68
WBXBAR1x8  := wbxbar1x8
69
WBXBAR4x1  := wbxbar4x1
70
WB         := fwb_master.v fwb_slave.v
71 10 dgisselq
 
72 16 dgisselq
.PHONY: $(WBARB) $(WB2AXI) $(RDLITE) $(WRLITE) $(AXLITE) $(WB2LITE) $(DEMOAXI)
73 10 dgisselq
 
74 16 dgisselq
$(WBARB): $(WBARB)_prf/PASS $(WBARB)_cvr/PASS
75
$(WBARB)_prf/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
76
        sby -f $(WBARB).sby
77
$(WBARB)_cvr/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
78
        sby -f $(WBARB).sby
79 10 dgisselq
 
80 16 dgisselq
.PHONY: $(WB2AXI)
81
$(WB2AXI): $(WB2AXI)/PASS
82
$(WB2AXI)/PASS: $(RTL)/$(WB2AXI).v $(WB2AXI).sby $(WB)
83
        sby -f $(WB2AXI).sby
84 10 dgisselq
 
85 16 dgisselq
$(RDLITE): $(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS
86
$(RDLITE)_prf/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
87
        sby -f $(RDLITE).sby prf
88
$(RDLITE)_cvr/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
89
        sby -f $(RDLITE).sby cvr
90 10 dgisselq
 
91 16 dgisselq
$(WRLITE): $(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
92
$(WRLITE)_prf/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
93
        sby -f $(WRLITE).sby prf
94
$(WRLITE)_cvr/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
95
        sby -f $(WRLITE).sby cvr
96 10 dgisselq
 
97 16 dgisselq
$(AXLITE): $(AXLITE)_prf/PASS $(AXLITE)_cvr/PASS
98
AXLITE_DEPS := $(RTL)/$(RDLITE).v $(RTL)/$(WRLITE).v \
99
        $(RTL)/$(WBARB).v fwb_master.v faxil_slave.v                    \
100
        $(AXLITE).sby $(RTL)/$(AXLITE).v                                \
101
        $(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS                           \
102
        $(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
103 10 dgisselq
 
104 16 dgisselq
$(AXLITE)_prf/PASS: $(AXLITE_DEPS)
105
        sby -f $(AXLITE).sby prf
106
 
107
$(AXLITE)_cvr/PASS: $(AXLITE_DEPS)
108
        sby -f $(AXLITE).sby cvr
109
 
110
.PHONY: $(WB2LITE)
111
$(WB2LITE): $(WB2LITE)_cvr/PASS $(WB2LITE)_prf/PASS
112
$(WB2LITE)_prf/PASS: $(RTL)/$(WB2LITE).v
113
$(WB2LITE)_prf/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
114
        sby -f $(WB2LITE).sby prf
115
 
116
$(WB2LITE)_cvr/PASS: $(RTL)/$(WB2LITE).v
117
$(WB2LITE)_cvr/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
118
        sby -f $(WB2LITE).sby cvr
119
 
120
$(DEMOAXI): $(DEMOAXI)_prf/PASS $(DEMOAXI)_cvr/PASS
121
$(DEMOAXI)_prf/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
122
        sby -f $(DEMOAXI).sby prf
123
$(DEMOAXI)_cvr/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
124
        sby -f $(DEMOAXI).sby cvr
125
 
126
.PHONY: $(XILINXDEMO)
127
$(XILINXDEMO): $(XILINXDEMO)_prf/PASS $(XILINXDEMO)_cvr/PASS
128
$(XILINXDEMO)_prf/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
129
        sby -f $(XILINXDEMO).sby prf
130
$(XILINXDEMO)_cvr/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
131
        sby -f $(XILINXDEMO).sby cvr
132
 
133
 
134
.PHONY: $(AXI2WB)
135
$(AXI2WB)/PASS: $(RTL)/$(AXI2WB).v $(AXI2WB).sby
136
$(AXI2WB)/PASS: $(WB)
137
$(AXI2WB)/PASS: faxi_slave.v
138
$(AXI2WB)/PASS: f_order.v
139
$(AXI2WB)/PASS: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
140
$(AXI2WB)/PASS: $(RTL)/wbarbiter.v
141
        echo "The AXI2WB bridge does not work yet, so I do not expect this one to pass"
142
        echo sby -f $(AXI2WB).sby
143
 
144
.PHONY: $(WBXBAR) $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
145
$(WBXBAR): $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
146
$(WBXBAR4x8): wbxbar_prf4x8_buflp/PASS
147
wbxbar_prf4x8_buflp/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
148
        sby -f $(WBXBAR).sby prf4x8_buflp
149
$(WBXBAR4x8): wbxbar_prf4x8_buf/PASS
150
wbxbar_prf4x8_buf/PASS:      $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
151
        sby -f $(WBXBAR).sby prf4x8_buf
152
$(WBXBAR4x8): wbxbar_prf4x8_lp/PASS
153
wbxbar_prf4x8_lp/PASS:       $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
154
        sby -f $(WBXBAR).sby prf4x8_lp
155
$(WBXBAR4x8): wbxbar_prf4x8_cheap/PASS
156
wbxbar_prf4x8_cheap/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
157
        sby -f $(WBXBAR).sby prf4x8_cheap
158
$(WBXBAR4x8): wbxbar_prf4x8_buflpko/PASS
159
wbxbar_prf4x8_buflpko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
160
        sby -f $(WBXBAR).sby prf4x8_buflpko
161
$(WBXBAR4x8): wbxbar_prf4x8_bufko/PASS
162
wbxbar_prf4x8_bufko/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
163
        sby -f $(WBXBAR).sby prf4x8_bufko
164
$(WBXBAR4x8): wbxbar_prf4x8_lpko/PASS
165
wbxbar_prf4x8_lpko/PASS:     $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
166
        sby -f $(WBXBAR).sby prf4x8_lpko
167
$(WBXBAR4x8): wbxbar_prf4x8_cheapko/PASS
168
wbxbar_prf4x8_cheapko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
169
        sby -f $(WBXBAR).sby prf4x8_cheapko
170
$(WBXBAR4x8): wbxbar_prf4x8_buflpkos/PASS
171
wbxbar_prf4x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
172
        sby -f $(WBXBAR).sby prf4x8_buflpkos
173
$(WBXBAR4x8): wbxbar_prf4x8_bufkos/PASS
174
wbxbar_prf4x8_bufkos/PASS:   $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
175
        sby -f $(WBXBAR).sby prf4x8_bufkos
176
$(WBXBAR4x8): wbxbar_prf4x8_lpkos/PASS
177
wbxbar_prf4x8_lpkos/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
178
        sby -f $(WBXBAR).sby prf4x8_lpkos
179
$(WBXBAR4x8): wbxbar_prf4x8_cheapkos/PASS
180
wbxbar_prf4x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
181
        sby -f $(WBXBAR).sby prf4x8_cheapkos
182
$(WBXBAR1x8): wbxbar_prf1x8_buflp/PASS
183
wbxbar_prf1x8_buflp/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
184
        sby -f $(WBXBAR).sby prf1x8_buflp
185
$(WBXBAR1x8): wbxbar_prf1x8_buf/PASS
186
wbxbar_prf1x8_buf/PASS:      $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
187
        sby -f $(WBXBAR).sby prf1x8_buf
188
$(WBXBAR1x8): wbxbar_prf1x8_lp/PASS
189
wbxbar_prf1x8_lp/PASS:       $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
190
        sby -f $(WBXBAR).sby prf1x8_lp
191
$(WBXBAR1x8): wbxbar_prf1x8_cheap/PASS
192
wbxbar_prf1x8_cheap/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
193
        sby -f $(WBXBAR).sby prf1x8_cheap
194
$(WBXBAR1x8): wbxbar_prf1x8_buflpko/PASS
195
wbxbar_prf1x8_buflpko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
196
        sby -f $(WBXBAR).sby prf1x8_buflpko
197
$(WBXBAR1x8): wbxbar_prf1x8_bufko/PASS
198
wbxbar_prf1x8_bufko/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
199
        sby -f $(WBXBAR).sby prf1x8_bufko
200
$(WBXBAR1x8): wbxbar_prf1x8_lpko/PASS
201
wbxbar_prf1x8_lpko/PASS:     $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
202
        sby -f $(WBXBAR).sby prf1x8_lpko
203
$(WBXBAR1x8): wbxbar_prf1x8_cheapko/PASS
204
wbxbar_prf1x8_cheapko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
205
        sby -f $(WBXBAR).sby prf1x8_cheapko
206
$(WBXBAR1x8): wbxbar_prf1x8_buflpkos/PASS
207
wbxbar_prf1x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
208
        sby -f $(WBXBAR).sby prf1x8_buflpkos
209
$(WBXBAR1x8): wbxbar_prf1x8_bufkos/PASS
210
wbxbar_prf1x8_bufkos/PASS:   $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
211
        sby -f $(WBXBAR).sby prf1x8_bufkos
212
$(WBXBAR1x8): wbxbar_prf1x8_lpkos/PASS
213
wbxbar_prf1x8_lpkos/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
214
        sby -f $(WBXBAR).sby prf1x8_lpkos
215
$(WBXBAR1x8): wbxbar_prf1x8_cheapkos/PASS
216
wbxbar_prf1x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
217
        sby -f $(WBXBAR).sby prf1x8_cheapkos
218
$(WBXBAR4x1): wbxbar_prf4x1_buflp/PASS
219
wbxbar_prf4x1_buflp/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
220
        sby -f $(WBXBAR).sby prf4x1_buflp
221
$(WBXBAR4x1): wbxbar_prf4x1_buf/PASS
222
wbxbar_prf4x1_buf/PASS:      $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
223
        sby -f $(WBXBAR).sby prf4x1_buf
224
$(WBXBAR4x1): wbxbar_prf4x1_lp/PASS
225
wbxbar_prf4x1_lp/PASS:       $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
226
        sby -f $(WBXBAR).sby prf4x1_lp
227
$(WBXBAR4x1): wbxbar_prf4x1_cheap/PASS
228
wbxbar_prf4x1_cheap/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
229
        sby -f $(WBXBAR).sby prf4x1_cheap
230
$(WBXBAR4x1): wbxbar_prf4x1_buflpko/PASS
231
wbxbar_prf4x1_buflpko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
232
        sby -f $(WBXBAR).sby prf4x1_buflpko
233
$(WBXBAR4x1): wbxbar_prf4x1_bufko/PASS
234
wbxbar_prf4x1_bufko/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
235
        sby -f $(WBXBAR).sby prf4x1_bufko
236
$(WBXBAR4x1): wbxbar_prf4x1_lpko/PASS
237
wbxbar_prf4x1_lpko/PASS:     $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
238
        sby -f $(WBXBAR).sby prf4x1_lpko
239
$(WBXBAR4x1): wbxbar_prf4x1_cheapko/PASS
240
wbxbar_prf4x1_cheapko/PASS:  $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
241
        sby -f $(WBXBAR).sby prf4x1_cheapko
242
$(WBXBAR4x1): wbxbar_prf4x1_buflpkos/PASS
243
wbxbar_prf4x1_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
244
        sby -f $(WBXBAR).sby prf4x1_buflpkos
245
$(WBXBAR4x1): wbxbar_prf4x1_bufkos/PASS
246
wbxbar_prf4x1_bufkos/PASS:   $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
247
        sby -f $(WBXBAR).sby prf4x1_bufkos
248
$(WBXBAR4x1): wbxbar_prf4x1_lpkos/PASS
249
wbxbar_prf4x1_lpkos/PASS:    $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
250
        sby -f $(WBXBAR).sby prf4x1_lpkos
251
$(WBXBAR4x1): wbxbar_prf4x1_cheapkos/PASS
252
wbxbar_prf4x1_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
253
        sby -f $(WBXBAR).sby prf4x1_cheapkos
254
 
255 10 dgisselq
.PHONY: clean
256
clean:
257 16 dgisselq
        rm -rf  $(WBARB)_prf/ $(WBARB)_cvr/
258
        rm -rf  $(WB2LITE)_cvr/ $(WB2LITE)_prf/
259
        rm -rf  $(RDLITE)_cvr/  $(RDLITE)_prf
260
        rm -rf  $(WRLITE)_cvr/  $(WRLITE)_prf
261
        rm -rf  $(AXLITE)_cvr/  $(AXLITE)_prf
262
        rm -rf  $(DEMOAXI)_cvr/ $(DEMOAXI)_prf
263
        @# The three broken cores, to include Xilinx's
264
        rm -rf  $(WB2AXI)/
265
        rm -rf  $(AXI2WB)/
266
        rm -rf  $(XILINXDEMO)_cvr/ $(XILINXDEMO)_prf
267
        # rm -f *.check

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.