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

Subversion Repositories wbuart32

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /wbuart32/trunk/bench
    from Rev 25 to Rev 26
    ↔ Reverse comparison
  •

Rev 25 → Rev 26

/cpp/Makefile
46,7 → 46,7
##
################################################################################
##
## Copyright (C) 2015-2016, Gisselquist Technology, LLC
## Copyright (C) 2015-2019, Gisselquist Technology, LLC
##
## This program is free software (firmware): you can redistribute it and/or
## modify it under the terms of the GNU General Public License as published
176,4 → 176,6
rm -f ./mkspeech ./speech.hex
rm -rf $(OBJDIR)/
 
ifneq ($(MAKECMDGOALS),clean)
-include $(OBJDIR)/depends.txt
endif
/cpp/helloworld.cpp
12,7 → 12,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/cpp/linetest.cpp
20,7 → 20,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/cpp/mkspeech.cpp
12,7 → 12,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/cpp/speechtest.cpp
17,7 → 17,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/cpp/uartsim.cpp
11,7 → 11,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/cpp/uartsim.h
14,7 → 14,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
/formal/Makefile
15,7 → 15,7
##
################################################################################
##
## Copyright (C) 2017, Gisselquist Technology, LLC
## Copyright (C) 2017-2019, Gisselquist Technology, LLC
##
## This program is free software (firmware): you can redistribute it and/or
## modify it under the terms of the GNU General Public License as published
38,52 → 38,38
################################################################################
##
##
TESTS := ufifo txuartlite rxuartlite
TESTS := ufifo txuartlite rxuartlite txuart
.PHONY: $(TESTS)
all: $(TESTS)
RTL := ../../rtl
SMTBMC := yosys-smtbmc
# SOLVER := -s z3
SOLVER := -s yices
# BMCARGS := --presat $(SOLVER)
BMCARGS := $(SOLVER)
INDARGS := $(SOLVER) -i
 
FIFO := ufifo
TX := txuartlite
TX := txuart
TXLITE:= txuartlite
RX := rxuartlite
 
$(FIFO).smt2: $(RTL)/$(FIFO).v $(FIFO).ys
yosys -ql $(FIFO).yslog -s $(FIFO).ys
.PHONY: $(FIFO) $(TX) $(RX) $(TXLITE)
$(FIFO): $(FIFO)/PASS
$(TX): $(TX)/PASS
$(RX): $(RX)_prf/PASS $(RX)_cvr/PASS
$(TXLITE): $(TXLITE)_cvr/PASS $(TXLITE)_prf/PASS
 
$(TX).smt2: $(RTL)/$(TX).v $(TX).ys
yosys -ql $(TX).yslog -s $(TX).ys
$(TX)/PASS: $(TX).sby $(RTL)/$(TX).v
sby -f $(TX).sby
 
$(RX).smt2: $(RTL)/$(RX).v $(RX).ys
yosys -ql $(RX).yslog -s $(RX).ys
$(RX)_prf/PASS: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby prf
$(RX)_cvr/PASS: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby cvr
 
$(FIFO) : $(FIFO).check
$(FIFO).check: $(FIFO).smt2
$(SMTBMC) --presat $(BMCARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
$(SMTBMC) $(INDARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
touch $@
$(TXLITE)_cvr/PASS: $(TXLITE).sby $(RTL)/$(TXLITE).v
sby -f $(TXLITE).sby cvr
$(TXLITE)_prf/PASS: $(TXLITE).sby $(RTL)/$(TXLITE).v
sby -f $(TXLITE).sby prf
 
$(TX) : $(TX).check
$(TX).check: $(TX).smt2
$(SMTBMC) --presat $(BMCARGS) -t 90 --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 $@
$(FIFO)/PASS: $(FIFO).sby $(RTL)/$(FIFO).v
sby -f $(FIFO).sby
 
$(RX) : $(RX).check
$(RX).check: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby
touch $@
 
 
.PHONY: clean
clean:
rm -f $(FIFO).smt2 $(FIFO)*.vcd
rm -f $(TX).smt2 $(TX)*.vcd
rm -rf $(RX)_one/ $(RX)_two/
rm -f *.check
rm -rf $(FIFO)/ $(RX)_*/ $(TX)/ $(TXLITE)_cvr/ $(TXLITE)_prf/
/formal/rxuartlite.sby
1,21 → 1,20
[tasks]
one
two
prf
cvr
 
[options]
mode prove
prf: mode prove
cvr: mode cover
multiclock on
one: depth 20
two: depth 120
prf: depth 110
cvr: depth 720
 
[engines]
smtbmc
smtbmc boolector
 
[script]
read -define F_OPT_CLK2FFLOGIC
read -define RXUARTLITE
one: read -sv -formal rxuartlite.v
two: read -sv -D PHASE_TWO -formal rxuartlite.v
prf: read -formal -DRXUARTLITE -D PHASE_TWO rxuartlite.v
cvr: read -formal -DRXUARTLITE -D PHASE_TWO rxuartlite.v
chparam -set CLOCKS_PER_BAUD 16 rxuartlite
prep -top rxuartlite
# opt_merge -share_all
/formal/txuart.sby
0,0 → 1,13
[options]
mode prove
depth 10
 
[engines]
smtbmc boolector
 
[script]
read -formal -DTXUART txuart.v
prep -top txuart
 
[files]
../../rtl/txuart.v
/formal/txuartlite.sby
1,27 → 1,18
[tasks]
verific
yosys
cvr
prf
 
[options]
mode prove
prf: mode prove
cvr: mode cover
depth 90
expect pass
 
[engines]
smtbmc yices
smtbmc boolector
 
[script]
verific:
verific -vlog-define VERIFIC_SVA
verific -sv txuartlite.v
verific -import -extnets -all txuartlite
read -formal -DTXUARTLITE txuartlite.v
prep -top txuartlite
--
 
yosys:
read_verilog -DTXUARTLITE -formal txuartlite.v
prep -top txuartlite
--
 
[files]
../../rtl/txuartlite.v
/formal/ufifo.sby
5,7 → 5,7
smtbmc
 
[script]
read -sv -DUFIFO -formal ufifo.v
read -formal -DUFIFO ufifo.v
prep -top ufifo
 
[files]
/formal
formal Property changes : Modified: svn:ignore ## -8,3 +8,8 ## txuartlite_verific txuartlite_yosys ufifo +rxuartlite_cvr +rxuartlite_prf +txuartlite_cvr +txuartlite_prf +txuart Index: verilog/Makefile =================================================================== --- verilog/Makefile (revision 25) +++ verilog/Makefile (revision 26) @@ -68,7 +68,8 @@ ################################################################################ ## ## -all: test +.PHONY: all +all: test tags YYMMDD=`date +%Y%m%d` CXX := g++ FBDIR := . @@ -75,45 +76,37 @@ VDIRFB:= $(FBDIR)/obj_dir RTLDR := ../../rtl VERILATOR := verilator -VFLAGS := -Wall --MMD --trace -y ../../rtl -cc +VFLAGS := -Wall --MMD --trace -y $(RTLDR) -cc .PHONY: test testline testhello speechfifo test: testline testhello speechfifo -testline: $(VDIRFB)/Vlinetest__ALL.a -testhello: $(VDIRFB)/Vhelloworld__ALL.a +testline: $(VDIRFB)/Vlinetest__ALL.a +testhello: $(VDIRFB)/Vhelloworld__ALL.a speechfifo: $(VDIRFB)/Vspeechfifo__ALL.a -$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp -$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.mk -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: linetest.v -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: $(RTLDR)/rxuart.v $(RTLDR)/txuart.v -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: $(RTLDR)/rxuartlite.v $(RTLDR)/txuartlite.v +$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.cpp +$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.cpp +$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.cpp -$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp -$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.mk -$(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp $(VDIRFB)/Vhelloworld.mk: helloworld.v -$(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp $(VDIRFB)/Vhelloworld.mk: $(RTLDR)/txuartlite.v $(RTLDR)/txuart.v - -SPEECHSRCS := $(addprefix $(RTLDR)/,rxuart.v txuart.v rxuartlite.v txuartlite.v ufifo.v wbuart.v) -SPEECHVFILES:= $(addprefix $(VDIRFB)/,Vspeechfifo.h Vspeechfifo.cpp Vspeechfifo.mk) -$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.h $(VDIRFB)/Vspeechfifo.cpp -$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.mk -$(SPEECHVFILES): speechfifo.v $(SPEECHSRCS) - -$(VDIRFB)/V%.cpp $(VDIRFB)/V%.h $(VDIRFB)/V%.mk: $(FBDIR)/%.v +$(VDIRFB)/V%.mk: $(VDIRFB)/%.h +$(VDIRFB)/V%.h: $(VDIRFB)/%.cpp +$(VDIRFB)/V%.cpp: $(FBDIR)/%.v $(VERILATOR) $(VFLAGS) $*.v -$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.mk +$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.cpp cd $(VDIRFB); make -f V$*.mk +tags: $(wildcard *.v) $(wildcard $(RTLDR)/*.v) + ctags *.v $(RTLDR)/*.v + .PHONY: clean clean: - rm -rf $(VDIRFB)/*.mk - rm -rf $(VDIRFB)/*.cpp - rm -rf $(VDIRFB)/*.h - rm -rf $(VDIRFB)/ + rm -rf tags $(VDIRFB)/ -DIRS := $(wildcard $(VDIRFB)/*.d) -ifneq ($(DIRS),) --include $(DIRS) +DEPS := $(wildcard $(VDIRFB)/*.d) + +ifneq ($(MAKECMDGOALS),clean) +ifneq ($(DEPS),) +include $(DEPS) endif +endif
/verilog
verilog Property changes : Modified: svn:ignore ## -1,3 +1,4 ## obj_dir speech.hex speech.inc +tags

powered by: WebSVN 2.1.0

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