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

Subversion Repositories wb2axip

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

Go to most recent revision | 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
## Copyright (C) 2017, 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
TESTS := wbm2axisp wbarbiter # axim2wbsp
42
.PHONY: $(TESTS)
43
all: $(TESTS)
44
RTL := ../../rtl
45
SMTBMC  := yosys-smtbmc
46
# SOLVER  := -s z3
47
SOLVER  := -s yices
48
# SOLVER  := -s boolector
49
BMCARGS := --presat $(SOLVER)
50
# BMCARGS := $(SOLVER)
51
INDARGS := $(SOLVER) -i
52
 
53
WBARB    := wbarbiter
54
WB2AXI   := wbm2axisp
55
AXI2WB   := axim2wbsp
56
 
57
$(WBARB).smt2: $(RTL)/$(WBARB).v fwb_master.v fwb_slave.v $(WBARB).ys
58
        yosys -ql $(WBARB).yslog -s $(WBARB).ys
59
 
60
$(WB2AXI).smt2: $(RTL)/$(WB2AXI).v $(WB2AXI).ys fwb_slave.v faxi_master.v
61
        yosys -ql $(WB2AXI).yslog -s $(WB2AXI).ys
62
 
63
$(AXI2WB).smt2: $(RTL)/$(AXI2WB).v $(AXI2WB).ys fwb_master.v faxi_slave.v
64
$(AXI2WB).smt2: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
65
$(AXI2WB).smt2: $(RTL)/wbarbiter.v
66
        yosys -ql $(AXI2WB).yslog -s $(AXI2WB).ys
67
 
68
$(WBARB) : $(WBARB).check
69
$(WBARB).check: $(WBARB).smt2
70
        rm -f $@
71
        $(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WBARB).vcd $(WBARB).smt2
72
        $(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WBARB).vcd $(WBARB).smt2
73
        touch $@
74
 
75
$(WB2AXI) : $(WB2AXI).check
76
$(WB2AXI).check: $(WB2AXI).smt2
77
        rm -f $@
78
        $(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
79
        $(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
80
        touch $@
81
 
82
$(AXI2WB) : $(AXI2WB).check
83
$(AXI2WB).check: $(AXI2WB).smt2
84
        rm -f $@
85
        $(SMTBMC) $(BMCARGS) -t 60 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
86
        $(SMTBMC) $(INDARGS) -t 58 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
87
        touch $@
88
 
89
.PHONY: clean
90
clean:
91
        rm -f  $(WBARB).smt2  $(WBARB).yslog   $(WBARB)*.vcd
92
        rm -f  $(WB2AXI).smt2 $(WB2AXI).yslog  $(WB2AXI)*.vcd
93
        rm -f  $(AXI2WB).smt2 $(AXI2WB).yslog  $(AXI2WB)*.vcd
94
        rm -f *.check

powered by: WebSVN 2.1.0

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