| Line 36... |
Line 36... |
## http://www.gnu.org/licenses/gpl.html
|
## http://www.gnu.org/licenses/gpl.html
|
##
|
##
|
################################################################################
|
################################################################################
|
##
|
##
|
##
|
##
|
TESTS := ufifo
|
TESTS := ufifo txuartlite rxuartlite
|
.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 49... |
Line 49... |
BMCARGS := $(SOLVER)
|
BMCARGS := $(SOLVER)
|
INDARGS := $(SOLVER) -i
|
INDARGS := $(SOLVER) -i
|
|
|
FIFO := ufifo
|
FIFO := ufifo
|
TX := txuartlite
|
TX := txuartlite
|
|
RX := rxuartlite
|
|
|
$(FIFO).smt2: $(RTL)/$(FIFO).v
|
$(FIFO).smt2: $(RTL)/$(FIFO).v $(FIFO).ys
|
yosys -ql $(FIFO).yslog -s $(FIFO).ys
|
yosys -ql $(FIFO).yslog -s $(FIFO).ys
|
|
|
$(TX).smt2: $(RTL)/$(TX).v
|
$(TX).smt2: $(RTL)/$(TX).v $(TX).ys
|
yosys -ql $(TX).yslog -s $(TX).ys
|
yosys -ql $(TX).yslog -s $(TX).ys
|
|
|
|
$(RX).smt2: $(RTL)/$(RX).v $(RX).ys
|
|
yosys -ql $(RX).yslog -s $(RX).ys
|
|
|
$(FIFO) : $(FIFO).check
|
$(FIFO) : $(FIFO).check
|
$(FIFO).check: $(FIFO).smt2
|
$(FIFO).check: $(FIFO).smt2
|
$(SMTBMC) --presat $(BMCARGS) -t 24 --dump-vcd $(FIFO).vcd $(FIFO).smt2
|
$(SMTBMC) --presat $(BMCARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
|
$(SMTBMC) $(INDARGS) -t 24 --dump-vcd $(FIFO).vcd $(FIFO).smt2
|
$(SMTBMC) $(INDARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
|
touch $@
|
touch $@
|
|
|
$(TX) : $(TX).check
|
$(TX) : $(TX).check
|
$(TX).check: $(TX).smt2
|
$(TX).check: $(TX).smt2
|
$(SMTBMC) --presat $(BMCARGS) -t 200 --dump-vcd $(TX).vcd $(TX).smt2
|
$(SMTBMC) --presat $(BMCARGS) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
|
$(SMTBMC) $(INDARGS) -t 200 --dump-vcd $(TX).vcd $(TX).smt2
|
$(SMTBMC) $(INDARGS) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
|
|
$(SMTBMC) -c $(SOLVER) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
|
|
touch $@
|
|
|
|
$(RX) : $(RX).check
|
|
$(RX).check: $(RX).sby $(RTL)/$(RX).v
|
|
sby -f $(RX).sby
|
touch $@
|
touch $@
|
|
|
|
|
.PHONY: clean
|
.PHONY: clean
|
clean:
|
clean:
|
rm -f $(FIFO).smt2 $(FIFO)*.vcd
|
rm -f $(FIFO).smt2 $(FIFO)*.vcd
|
rm -f $(TX).smt2 $(TX)*.vcd
|
rm -f $(TX).smt2 $(TX)*.vcd
|
|
rm -rf $(RX)_one/ $(RX)_two/
|
rm -f *.check
|
rm -f *.check
|
