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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [bench/] [formal/] [Makefile] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 209 dgisselq
################################################################################
2
##
3
## Filename:    Makefile
4
##
5
## Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
##
7
## Purpose:     To direct the formal verification of particular components of
8
##              the ZipCPU.
9
##
10
## Targets:     The default target, all, tests all of the components within
11
##              this module.
12
##
13
## Creator:     Dan Gisselquist, Ph.D.
14
##              Gisselquist Technology, LLC
15
##
16
################################################################################
17
##
18
## Copyright (C) 2017-2019, Gisselquist Technology, LLC
19
##
20
## This program is free software (firmware): you can redistribute it and/or
21
## modify it under the terms of  the GNU General Public License as published
22
## by the Free Software Foundation, either version 3 of the License, or (at
23
## your option) any later version.
24
##
25
## This program is distributed in the hope that it will be useful, but WITHOUT
26
## ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
27
## FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
28
## for more details.
29
##
30
## You should have received a copy of the GNU General Public License along
31
## with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
32
## target there if the PDF file isn't present.)  If not, see
33
##  for a copy.
34
##
35
## License:     GPL, v3, as defined and found on www.gnu.org,
36
##              http://www.gnu.org/licenses/gpl.html
37
##
38
##
39
################################################################################
40
##
41
##
42
TESTS := prefetch dblfetch pfcache memops pipemem idecode div
43
TESTS += zipmmu ziptimer zipcounter zipjiffies wbwatchdog zipmmu icontrol wbdmac
44
TESTS += busdelay wbpriarbiter wbdblpriarb cpuops cpu dcache zipcpu
45
.PHONY: $(TESTS)
46
all: $(TESTS)
47
RTL := ../../rtl
48
 
49
SMTBMC  := yosys-smtbmc
50
# SOLVER  := -s z3
51
SOLVER  := -s yices
52
# SOLVER  := -s boolector
53
BMCARGS := --presat $(SOLVER)
54
INDARGS := $(SOLVER) -i
55
 
56
PFONE  := prefetch
57
PFTWO  := dblfetch
58
PFCACHE:= pfcache
59
WBDLY  := busdelay
60
PRIARB := wbpriarbiter
61
DBL    := wbdblpriarb
62
PIPE   := pipemem
63
MEM    := memops
64
MMU    := zipmmu
65
TMR    := ziptimer
66
CNT    := zipcounter
67
JIF    := zipjiffies
68
WDG    := wbwatchdog
69
INT    := icontrol
70
DCD    := idecode
71
DMA    := wbdmac
72
ALU    := cpuops
73
DIV    := div
74
CPU    := zipcpu
75
DCACHE := dcache
76
.PHONY: cpu
77
cpu: zipcpu
78
 
79
MASTER := $(RTL)/ex/fwb_master.v
80
SLAVE  := $(RTL)/ex/fwb_slave.v
81
 
82
.PHONY: $(PFONE)
83
$(PFONE) : $(PFONE)/PASS
84
$(PFONE)/PASS: $(PFONE).sby $(RTL)/core/$(PFONE).v $(MASTER)
85
        sby -f $(PFONE).sby
86
 
87
.PHONY: $(PFTWO)
88
$(PFTWO) : $(PFTWO)/PASS
89
$(PFTWO)/PASS: $(PFTWO).sby $(RTL)/core/$(PFTWO).v $(MASTER)
90
        sby -f $(PFTWO).sby
91
 
92
 
93
.PHONY: $(PFCACHE)
94
$(PFCACHE): $(PFCACHE)_prf/PASS $(PFCACHE)_cvr/PASS
95
$(PFCACHE)_prf/PASS: $(PFCACHE).sby $(RTL)/core/$(PFCACHE).v $(MASTER)
96
        sby -f $(PFCACHE).sby prf
97
$(PFCACHE)_cvr/PASS: $(PFCACHE).sby $(RTL)/core/$(PFCACHE).v $(MASTER)
98
        sby -f $(PFCACHE).sby cvr
99
 
100
.PHONY: $(WBDLY)
101
$(WBDLY): $(WBDLY)/PASS
102
$(WBDLY)/PASS: $(WBDLY).sby $(RTL)/ex/$(WBDLY).v $(MASTER) $(SLAVE)
103
        sby -f $(WBDLY).sby
104
 
105
.PHONY: $(PRIARB)
106
$(PRIARB): $(PRIARB)/PASS
107
$(PRIARB)/PASS: $(PRIARB).sby $(RTL)/ex/$(PRIARB).v $(MASTER) $(SLAVE)
108
        sby -f $(PRIARB).sby
109
 
110
.PHONY: $(DBL)
111
$(DBL): $(DBL)/PASS
112
$(DBL)/PASS: $(DBL).sby $(RTL)/ex/$(DBL).v $(MASTER) $(SLAVE) $(DBL).ys
113
        sby -f $(DBL).sby
114
 
115
.PHONY: $(MEM)
116
$(MEM): $(MEM)_cover/PASS $(MEM)_proof/PASS
117
$(MEM)_proof/PASS: $(MEM).sby $(RTL)/core/$(MEM).v $(MASTER)
118
        sby -f $(MEM).sby proof
119
$(MEM)_cover/PASS: $(MEM).sby $(RTL)/core/$(MEM).v $(MASTER)
120
        sby -f $(MEM).sby cover
121
 
122
.PHONY: $(PIPE)
123
$(PIPE): $(PIPE)_lcl_aligned_lock/PASS
124
$(PIPE): $(PIPE)_lcl_aligned_nolock/PASS
125
$(PIPE): $(PIPE)_lcl_noaligned_lock/PASS
126
$(PIPE): $(PIPE)_lcl_noaligned_nolock/PASS
127
$(PIPE): $(PIPE)_nolcl_aligned_lock/PASS
128
$(PIPE): $(PIPE)_nolcl_aligned_nolock/PASS
129
$(PIPE): $(PIPE)_nolcl_noaligned_lock/PASS
130
$(PIPE): $(PIPE)_nolcl_noaligned_nolock/PASS
131
$(PIPE)_lcl_aligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
132
        sby -f $(PIPE).sby lcl_aligned_lock
133
$(PIPE)_lcl_aligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
134
        sby -f $(PIPE).sby lcl_aligned_nolock
135
$(PIPE)_lcl_noaligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
136
        sby -f $(PIPE).sby lcl_noaligned_lock
137
$(PIPE)_lcl_noaligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
138
        sby -f $(PIPE).sby lcl_noaligned_nolock
139
$(PIPE)_nolcl_aligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
140
        sby -f $(PIPE).sby nolcl_aligned_lock
141
$(PIPE)_nolcl_aligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
142
        sby -f $(PIPE).sby nolcl_aligned_nolock
143
$(PIPE)_nolcl_noaligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
144
        sby -f $(PIPE).sby nolcl_noaligned_lock
145
$(PIPE)_nolcl_noaligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
146
        sby -f $(PIPE).sby nolcl_noaligned_nolock
147
 
148
.PHONY: $(MMU)
149
$(MMU): $(MMU)/PASS
150
$(MMU)/PASS: $(MMU).sby $(RTL)/peripherals/$(MMU).v $(MASTER) $(SLAVE)
151
        sby -f $(MMU).sby
152
 
153
.PHONY: $(TMR)
154
$(TMR): $(TMR)/PASS
155
$(TMR)/PASS: $(TMR).sby $(RTL)/peripherals/$(TMR).v $(SLAVE) $(TMR).ys
156
        sby -f $(TMR).sby
157
 
158
.PHONY: $(CNT)
159
$(CNT): $(CNT)/PASS
160
$(CNT)/PASS: $(CNT).sby $(RTL)/peripherals/$(CNT).v $(SLAVE)
161
        sby -f $(CNT).sby
162
 
163
.PHONY: $(JIF)
164
$(JIF): $(JIF)/PASS
165
$(JIF)/PASS: $(JIF).sby $(RTL)/peripherals/$(JIF).v $(SLAVE)
166
        sby -f $(JIF).sby
167
 
168
.PHONY: $(WDG)
169
$(WDG): $(WDG)/PASS
170
$(WDG)/PASS: $(WDG).sby $(RTL)/peripherals/$(WDG).v $(SLAVE)
171
        sby -f $(WDG).sby
172
 
173
.PHONY: $(INT)
174
$(INT): $(INT)/PASS
175
$(INT)/PASS: $(INT).sby $(RTL)/peripherals/$(INT).v $(SLAVE)
176
        sby -f $(INT).sby
177
 
178
.PHONY: $(DCD)
179
$(DCD): $(DCD)_pipe_div_mpy_cis_opipe/PASS
180
$(DCD): $(DCD)_pipe_div_mpy_cis_nopipe/PASS
181
$(DCD): $(DCD)_pipe_div_mpy_nocis_pipe/PASS
182
$(DCD): $(DCD)_pipe_div_mpy_nocis_nopipe/PASS
183
$(DCD): $(DCD)_pipe_div_nompy_nocis_nopipe/PASS
184
$(DCD): $(DCD)_pipe_nodiv_nompy_nocis_nopipe/PASS
185
$(DCD): $(DCD)_nopipe_nodiv_nompy_nocis_nopipe/PASS
186
 
187
$(DCD)_pipe_div_mpy_cis_opipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
188
        sby -f $(DCD).sby pipe_div_mpy_cis_opipe
189
$(DCD)_pipe_div_mpy_cis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
190
        sby -f $(DCD).sby pipe_div_mpy_cis_nopipe
191
$(DCD)_pipe_div_mpy_nocis_pipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
192
        sby -f $(DCD).sby pipe_div_mpy_nocis_pipe
193
$(DCD)_pipe_div_mpy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
194
        sby -f $(DCD).sby pipe_div_mpy_nocis_nopipe
195
$(DCD)_pipe_div_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
196
        sby -f $(DCD).sby pipe_div_nompy_nocis_nopipe
197
$(DCD)_pipe_nodiv_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
198
        sby -f $(DCD).sby pipe_nodiv_nompy_nocis_nopipe
199
$(DCD)_nopipe_nodiv_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
200
        sby -f $(DCD).sby nopipe_nodiv_nompy_nocis_nopipe
201
 
202
 
203
.PHONY: $(DMA)
204
$(DMA): $(DMA)/PASS
205
$(DMA)/PASS: $(RTL)/peripherals/$(DMA).v $(MASTER) $(SLAVE) $(DMA).sby
206
        sby -f $(DMA).sby
207
 
208
.PHONY: $(ALU)
209
$(ALU): $(ALU)/PASS
210
$(ALU)/PASS: $(ALU).sby $(RTL)/core/$(ALU).v abs_mpy.v
211
        sby -f $(ALU).sby
212
 
213
DCACHE_FILES := $(DCACHE).sby $(RTL)/core/dcache.v $(MASTER) $(RTL)/core/iscachable.v
214
 
215
.PHONY: $(DCACHE)
216
$(DCACHE) : $(DCACHE)_full/PASS $(DCACHE)_full_single/PASS $(DCACHE)_bare/PASS
217
$(DCACHE) : $(DCACHE)_nolock_nolocal/PASS $(DCACHE)_nolock_system/PASS
218
$(DCACHE) : $(DCACHE)_piped/PASS $(DCACHE)_cover/PASS $(DCACHE)_cover_pipe/PASS
219
$(DCACHE)_full/PASS: $(DCACHE_FILES)
220
        sby -f $(DCACHE).sby full
221
$(DCACHE)_full_single/PASS: $(DCACHE_FILES)
222
        sby -f $(DCACHE).sby full_single
223
 
224
$(DCACHE)_bare/PASS: $(DCACHE_FILES)
225
        sby -f $(DCACHE).sby bare
226
 
227
$(DCACHE)_nolock_nolocal/PASS: $(DCACHE_FILES)
228
        sby -f $(DCACHE).sby nolock_nolocal
229
 
230
$(DCACHE)_nolock_system/PASS: $(DCACHE_FILES)
231
        sby -f $(DCACHE).sby nolock_system
232
 
233
$(DCACHE)_piped/PASS: $(DCACHE_FILES)
234
        sby -f $(DCACHE).sby piped
235
 
236
$(DCACHE)_cover/PASS: $(DCACHE_FILES)
237
        sby -f $(DCACHE).sby cover
238
 
239
$(DCACHE)_cover_pipe/PASS: $(DCACHE_FILES)
240
        sby -f $(DCACHE).sby cover_pipe
241
 
242
.PHONY: $(DIV)
243
$(DIV) : $(DIV)/PASS
244
$(DIV)/PASS: $(DIV).sby $(RTL)/core/div.v
245
        sby -f $(DIV).sby
246
 
247
.PHONY: $(CPU)
248
$(CPU): $(CPU)_dcache/PASS $(CPU)_piped/PASS
249
$(CPU): $(CPU)_nopipe/PASS $(CPU)_lowlogic/PASS $(CPU)_ice40/PASS
250
CPUDEPS:= $(RTL)/core/$(CPU).v $(RTL)/core/cpuops.v $(RTL)/core/idecode.v \
251
        $(RTL)/core/pipemem.v $(RTL)/core/memops.v        \
252
        $(RTL)/ex/wbdblpriarb.v $(RTL)/ex/fwb_counter.v $(RTL)/cpudefs.v  \
253
        f_idecode.v abs_div.v abs_prefetch.v abs_mpy.v $(MASTER) $(SLAVE)  \
254
        $(CPU).sby
255
$(CPU)_dcache/PASS: $(CPUDEPS) $(RTL)/core/dcache.v $(RTL)/core/iscachable.v
256
        sby -f $(CPU).sby dcache
257
 
258
$(CPU)_piped/PASS: $(CPUDEPS)
259
        sby -f $(CPU).sby piped
260
 
261
$(CPU)_nopipe/PASS: $(CPUDEPS)
262
        sby -f $(CPU).sby nopipe
263
 
264
$(CPU)_lowlogic/PASS: $(CPUDEPS)
265
        sby -f $(CPU).sby lowlogic
266
 
267
$(CPU)_ice40/PASS: $(CPUDEPS)
268
        sby -f $(CPU).sby ice40
269
 
270
.PHONY: clean
271
clean:
272
        rm -rf $(PFONE)*/     $(PFTWO)*/      $(PFCACHE)*/
273
        rm -f $(WBDLY).smt2   $(WBDLY)*.vcd   $(WBDLY).yslog
274
        rm -f $(PRIARB).smt2  $(PRIARB)*.vcd  $(PRIARB).yslog
275
        rm -f $(DBL).smt2     $(DBL)*.vcd     $(DBL).yslog
276
        rm -rf $(MEM)*/       $(PIPE)*/       $(MMU)*/
277
        rm -rf $(TMR)*/       $(CNT)*/        $(JIF)*/
278
        rm -rf $(WDG)*/       $(INT)*/        $(DCD)_*/
279
        rm -rf $(DMA)*/       $(ALU)*/        $(DIV)*/
280
        rm -rf $(DCACHE)_*/
281
        rm -rf $(CPU)_*/
282
        rm -f *.check

powered by: WebSVN 2.1.0

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