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/formal
    from Rev 25 to Rev 26
    ↔ Reverse comparison
  •

Rev 25 → Rev 26

/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/
/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
/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
/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
/ufifo.sby
5,7 → 5,7
smtbmc
 
[script]
read -sv -DUFIFO -formal ufifo.v
read -formal -DUFIFO ufifo.v
prep -top ufifo
 
[files]
/.
. Property changes : Modified: svn:ignore ## -8,3 +8,8 ## txuartlite_verific txuartlite_yosys ufifo +rxuartlite_cvr +rxuartlite_prf +txuartlite_cvr +txuartlite_prf +txuart

powered by: WebSVN 2.1.0

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