| Line 13... |
Line 13... |
## Creator: Dan Gisselquist, Ph.D.
|
## Creator: Dan Gisselquist, Ph.D.
|
## Gisselquist Technology, LLC
|
## Gisselquist Technology, LLC
|
##
|
##
|
################################################################################
|
################################################################################
|
##
|
##
|
## Copyright (C) 2017, Gisselquist Technology, LLC
|
## Copyright (C) 2017-2018, Gisselquist Technology, LLC
|
##
|
##
|
## This program is free software (firmware): you can redistribute it and/or
|
## This file is part of the pipelined Wishbone to AXI converter project, a
|
## modify it under the terms of the GNU General Public License as published
|
## project that contains multiple bus bridging designs and formal bus property
|
## by the Free Software Foundation, either version 3 of the License, or (at
|
## sets.
|
## your option) any later version.
|
##
|
##
|
## The bus bridge designs and property sets are free RTL designs: you can
|
## This program is distributed in the hope that it will be useful, but WITHOUT
|
## redistribute them and/or modify any of them under the terms of the GNU
|
## ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
## Lesser General Public License as published by the Free Software Foundation,
|
## FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
## either version 3 of the License, or (at your option) any later version.
|
## for more details.
|
##
|
##
|
## The bus bridge designs and property sets are distributed in the hope that
|
## You should have received a copy of the GNU General Public License along
|
## they will be useful, but WITHOUT ANY WARRANTY; without even the implied
|
## with this program. (It's in the $(ROOT)/doc directory. Run make with no
|
## warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
## target there if the PDF file isn't present.) If not, see
|
## GNU Lesser General Public License for more details.
|
|
##
|
|
## You should have received a copy of the GNU Lesser General Public License
|
|
## along with these designs. (It's in the $(ROOT)/doc directory. Run make
|
|
## with no target there if the PDF file isn't present.) If not, see
|
## for a copy.
|
## for a copy.
|
##
|
##
|
## License: GPL, v3, as defined and found on www.gnu.org,
|
## License: LGPL, v3, as defined and found on www.gnu.org,
|
## http://www.gnu.org/licenses/gpl.html
|
## http://www.gnu.org/licenses/lgpl.html
|
##
|
##
|
################################################################################
|
################################################################################
|
##
|
##
|
##
|
##
|
TESTS := wbm2axisp wbarbiter # axim2wbsp
|
TESTS := wbarbiter wbm2axilite axilrd2wbsp axilwr2wbsp demoaxi axlite2wbsp wbxbar # wbm2axisp axim2wbsp
|
.PHONY: $(TESTS)
|
.PHONY: $(TESTS)
|
all: $(TESTS)
|
all: $(TESTS)
|
RTL := ../../rtl
|
RTL := ../../rtl
|
SMTBMC := yosys-smtbmc
|
SMTBMC := yosys-smtbmc
|
# SOLVER := -s z3
|
# SOLVER := -s z3
|
| Line 48... |
Line 52... |
# SOLVER := -s boolector
|
# SOLVER := -s boolector
|
BMCARGS := --presat $(SOLVER)
|
BMCARGS := --presat $(SOLVER)
|
# BMCARGS := $(SOLVER)
|
# BMCARGS := $(SOLVER)
|
INDARGS := $(SOLVER) -i
|
INDARGS := $(SOLVER) -i
|
|
|
|
DEMOAXI := demoaxi
|
WBARB := wbarbiter
|
WBARB := wbarbiter
|
WB2AXI := wbm2axisp
|
WB2AXI := wbm2axisp
|
AXI2WB := axim2wbsp
|
AXI2WB := axim2wbsp
|
|
WB2LITE := wbm2axilite
|
$(WBARB).smt2: $(RTL)/$(WBARB).v fwb_master.v fwb_slave.v $(WBARB).ys
|
RDLITE := axilrd2wbsp
|
yosys -ql $(WBARB).yslog -s $(WBARB).ys
|
WRLITE := axilwr2wbsp
|
|
AXLITE := axlite2wbsp
|
$(WB2AXI).smt2: $(RTL)/$(WB2AXI).v $(WB2AXI).ys fwb_slave.v faxi_master.v
|
XILINXDEMO := xlnxdemo
|
yosys -ql $(WB2AXI).yslog -s $(WB2AXI).ys
|
WBXBAR := wbxbar
|
|
WBXBAR4x8 := wbxbar4x8
|
$(AXI2WB).smt2: $(RTL)/$(AXI2WB).v $(AXI2WB).ys fwb_master.v faxi_slave.v
|
WBXBAR1x8 := wbxbar1x8
|
$(AXI2WB).smt2: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
|
WBXBAR4x1 := wbxbar4x1
|
$(AXI2WB).smt2: $(RTL)/wbarbiter.v
|
WB := fwb_master.v fwb_slave.v
|
yosys -ql $(AXI2WB).yslog -s $(AXI2WB).ys
|
|
|
.PHONY: $(WBARB) $(WB2AXI) $(RDLITE) $(WRLITE) $(AXLITE) $(WB2LITE) $(DEMOAXI)
|
$(WBARB) : $(WBARB).check
|
|
$(WBARB).check: $(WBARB).smt2
|
$(WBARB): $(WBARB)_prf/PASS $(WBARB)_cvr/PASS
|
rm -f $@
|
$(WBARB)_prf/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
|
$(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WBARB).vcd $(WBARB).smt2
|
sby -f $(WBARB).sby
|
$(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WBARB).vcd $(WBARB).smt2
|
$(WBARB)_cvr/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
|
touch $@
|
sby -f $(WBARB).sby
|
|
|
$(WB2AXI) : $(WB2AXI).check
|
.PHONY: $(WB2AXI)
|
$(WB2AXI).check: $(WB2AXI).smt2
|
$(WB2AXI): $(WB2AXI)/PASS
|
rm -f $@
|
$(WB2AXI)/PASS: $(RTL)/$(WB2AXI).v $(WB2AXI).sby $(WB)
|
$(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
|
sby -f $(WB2AXI).sby
|
$(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
|
|
touch $@
|
$(RDLITE): $(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS
|
|
$(RDLITE)_prf/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
|
$(AXI2WB) : $(AXI2WB).check
|
sby -f $(RDLITE).sby prf
|
$(AXI2WB).check: $(AXI2WB).smt2
|
$(RDLITE)_cvr/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
|
rm -f $@
|
sby -f $(RDLITE).sby cvr
|
$(SMTBMC) $(BMCARGS) -t 60 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
|
|
$(SMTBMC) $(INDARGS) -t 58 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
|
$(WRLITE): $(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
|
touch $@
|
$(WRLITE)_prf/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
|
|
sby -f $(WRLITE).sby prf
|
|
$(WRLITE)_cvr/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
|
|
sby -f $(WRLITE).sby cvr
|
|
|
|
$(AXLITE): $(AXLITE)_prf/PASS $(AXLITE)_cvr/PASS
|
|
AXLITE_DEPS := $(RTL)/$(RDLITE).v $(RTL)/$(WRLITE).v \
|
|
$(RTL)/$(WBARB).v fwb_master.v faxil_slave.v \
|
|
$(AXLITE).sby $(RTL)/$(AXLITE).v \
|
|
$(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS \
|
|
$(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
|
|
|
|
$(AXLITE)_prf/PASS: $(AXLITE_DEPS)
|
|
sby -f $(AXLITE).sby prf
|
|
|
|
$(AXLITE)_cvr/PASS: $(AXLITE_DEPS)
|
|
sby -f $(AXLITE).sby cvr
|
|
|
|
.PHONY: $(WB2LITE)
|
|
$(WB2LITE): $(WB2LITE)_cvr/PASS $(WB2LITE)_prf/PASS
|
|
$(WB2LITE)_prf/PASS: $(RTL)/$(WB2LITE).v
|
|
$(WB2LITE)_prf/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
|
|
sby -f $(WB2LITE).sby prf
|
|
|
|
$(WB2LITE)_cvr/PASS: $(RTL)/$(WB2LITE).v
|
|
$(WB2LITE)_cvr/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
|
|
sby -f $(WB2LITE).sby cvr
|
|
|
|
$(DEMOAXI): $(DEMOAXI)_prf/PASS $(DEMOAXI)_cvr/PASS
|
|
$(DEMOAXI)_prf/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
|
|
sby -f $(DEMOAXI).sby prf
|
|
$(DEMOAXI)_cvr/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
|
|
sby -f $(DEMOAXI).sby cvr
|
|
|
|
.PHONY: $(XILINXDEMO)
|
|
$(XILINXDEMO): $(XILINXDEMO)_prf/PASS $(XILINXDEMO)_cvr/PASS
|
|
$(XILINXDEMO)_prf/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
|
|
sby -f $(XILINXDEMO).sby prf
|
|
$(XILINXDEMO)_cvr/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
|
|
sby -f $(XILINXDEMO).sby cvr
|
|
|
|
|
|
.PHONY: $(AXI2WB)
|
|
$(AXI2WB)/PASS: $(RTL)/$(AXI2WB).v $(AXI2WB).sby
|
|
$(AXI2WB)/PASS: $(WB)
|
|
$(AXI2WB)/PASS: faxi_slave.v
|
|
$(AXI2WB)/PASS: f_order.v
|
|
$(AXI2WB)/PASS: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
|
|
$(AXI2WB)/PASS: $(RTL)/wbarbiter.v
|
|
echo "The AXI2WB bridge does not work yet, so I do not expect this one to pass"
|
|
echo sby -f $(AXI2WB).sby
|
|
|
|
.PHONY: $(WBXBAR) $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
|
|
$(WBXBAR): $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
|
|
$(WBXBAR4x8): wbxbar_prf4x8_buflp/PASS
|
|
wbxbar_prf4x8_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_buflp
|
|
$(WBXBAR4x8): wbxbar_prf4x8_buf/PASS
|
|
wbxbar_prf4x8_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_buf
|
|
$(WBXBAR4x8): wbxbar_prf4x8_lp/PASS
|
|
wbxbar_prf4x8_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_lp
|
|
$(WBXBAR4x8): wbxbar_prf4x8_cheap/PASS
|
|
wbxbar_prf4x8_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_cheap
|
|
$(WBXBAR4x8): wbxbar_prf4x8_buflpko/PASS
|
|
wbxbar_prf4x8_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_buflpko
|
|
$(WBXBAR4x8): wbxbar_prf4x8_bufko/PASS
|
|
wbxbar_prf4x8_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_bufko
|
|
$(WBXBAR4x8): wbxbar_prf4x8_lpko/PASS
|
|
wbxbar_prf4x8_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_lpko
|
|
$(WBXBAR4x8): wbxbar_prf4x8_cheapko/PASS
|
|
wbxbar_prf4x8_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_cheapko
|
|
$(WBXBAR4x8): wbxbar_prf4x8_buflpkos/PASS
|
|
wbxbar_prf4x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_buflpkos
|
|
$(WBXBAR4x8): wbxbar_prf4x8_bufkos/PASS
|
|
wbxbar_prf4x8_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_bufkos
|
|
$(WBXBAR4x8): wbxbar_prf4x8_lpkos/PASS
|
|
wbxbar_prf4x8_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_lpkos
|
|
$(WBXBAR4x8): wbxbar_prf4x8_cheapkos/PASS
|
|
wbxbar_prf4x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x8_cheapkos
|
|
$(WBXBAR1x8): wbxbar_prf1x8_buflp/PASS
|
|
wbxbar_prf1x8_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_buflp
|
|
$(WBXBAR1x8): wbxbar_prf1x8_buf/PASS
|
|
wbxbar_prf1x8_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_buf
|
|
$(WBXBAR1x8): wbxbar_prf1x8_lp/PASS
|
|
wbxbar_prf1x8_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_lp
|
|
$(WBXBAR1x8): wbxbar_prf1x8_cheap/PASS
|
|
wbxbar_prf1x8_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_cheap
|
|
$(WBXBAR1x8): wbxbar_prf1x8_buflpko/PASS
|
|
wbxbar_prf1x8_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_buflpko
|
|
$(WBXBAR1x8): wbxbar_prf1x8_bufko/PASS
|
|
wbxbar_prf1x8_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_bufko
|
|
$(WBXBAR1x8): wbxbar_prf1x8_lpko/PASS
|
|
wbxbar_prf1x8_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_lpko
|
|
$(WBXBAR1x8): wbxbar_prf1x8_cheapko/PASS
|
|
wbxbar_prf1x8_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_cheapko
|
|
$(WBXBAR1x8): wbxbar_prf1x8_buflpkos/PASS
|
|
wbxbar_prf1x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_buflpkos
|
|
$(WBXBAR1x8): wbxbar_prf1x8_bufkos/PASS
|
|
wbxbar_prf1x8_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_bufkos
|
|
$(WBXBAR1x8): wbxbar_prf1x8_lpkos/PASS
|
|
wbxbar_prf1x8_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_lpkos
|
|
$(WBXBAR1x8): wbxbar_prf1x8_cheapkos/PASS
|
|
wbxbar_prf1x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf1x8_cheapkos
|
|
$(WBXBAR4x1): wbxbar_prf4x1_buflp/PASS
|
|
wbxbar_prf4x1_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_buflp
|
|
$(WBXBAR4x1): wbxbar_prf4x1_buf/PASS
|
|
wbxbar_prf4x1_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_buf
|
|
$(WBXBAR4x1): wbxbar_prf4x1_lp/PASS
|
|
wbxbar_prf4x1_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_lp
|
|
$(WBXBAR4x1): wbxbar_prf4x1_cheap/PASS
|
|
wbxbar_prf4x1_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_cheap
|
|
$(WBXBAR4x1): wbxbar_prf4x1_buflpko/PASS
|
|
wbxbar_prf4x1_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_buflpko
|
|
$(WBXBAR4x1): wbxbar_prf4x1_bufko/PASS
|
|
wbxbar_prf4x1_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_bufko
|
|
$(WBXBAR4x1): wbxbar_prf4x1_lpko/PASS
|
|
wbxbar_prf4x1_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_lpko
|
|
$(WBXBAR4x1): wbxbar_prf4x1_cheapko/PASS
|
|
wbxbar_prf4x1_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_cheapko
|
|
$(WBXBAR4x1): wbxbar_prf4x1_buflpkos/PASS
|
|
wbxbar_prf4x1_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_buflpkos
|
|
$(WBXBAR4x1): wbxbar_prf4x1_bufkos/PASS
|
|
wbxbar_prf4x1_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_bufkos
|
|
$(WBXBAR4x1): wbxbar_prf4x1_lpkos/PASS
|
|
wbxbar_prf4x1_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_lpkos
|
|
$(WBXBAR4x1): wbxbar_prf4x1_cheapkos/PASS
|
|
wbxbar_prf4x1_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
|
|
sby -f $(WBXBAR).sby prf4x1_cheapkos
|
|
|
.PHONY: clean
|
.PHONY: clean
|
clean:
|
clean:
|
rm -f $(WBARB).smt2 $(WBARB).yslog $(WBARB)*.vcd
|
rm -rf $(WBARB)_prf/ $(WBARB)_cvr/
|
rm -f $(WB2AXI).smt2 $(WB2AXI).yslog $(WB2AXI)*.vcd
|
rm -rf $(WB2LITE)_cvr/ $(WB2LITE)_prf/
|
rm -f $(AXI2WB).smt2 $(AXI2WB).yslog $(AXI2WB)*.vcd
|
rm -rf $(RDLITE)_cvr/ $(RDLITE)_prf
|
rm -f *.check
|
rm -rf $(WRLITE)_cvr/ $(WRLITE)_prf
|
|
rm -rf $(AXLITE)_cvr/ $(AXLITE)_prf
|
|
rm -rf $(DEMOAXI)_cvr/ $(DEMOAXI)_prf
|
|
@# The three broken cores, to include Xilinx's
|
|
rm -rf $(WB2AXI)/
|
|
rm -rf $(AXI2WB)/
|
|
rm -rf $(XILINXDEMO)_cvr/ $(XILINXDEMO)_prf
|
|
# rm -f *.check
|
