URL
https://opencores.org/ocsvn/wbuart32/wbuart32/trunk
Subversion Repositories wbuart32
Compare Revisions
- This comparison shows the changes necessary to convert path
/wbuart32
- from Rev 21 to Rev 22
- ↔ Reverse comparison
Rev 21 → Rev 22
/trunk/bench/formal/Makefile
38,7 → 38,7
################################################################################ |
## |
## |
TESTS := ufifo |
TESTS := ufifo txuartlite rxuartlite |
.PHONY: $(TESTS) |
all: $(TESTS) |
RTL := ../../rtl |
51,28 → 51,39
|
FIFO := ufifo |
TX := txuartlite |
RX := rxuartlite |
|
$(FIFO).smt2: $(RTL)/$(FIFO).v |
$(FIFO).smt2: $(RTL)/$(FIFO).v $(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 |
|
$(RX).smt2: $(RTL)/$(RX).v $(RX).ys |
yosys -ql $(RX).yslog -s $(RX).ys |
|
$(FIFO) : $(FIFO).check |
$(FIFO).check: $(FIFO).smt2 |
$(SMTBMC) --presat $(BMCARGS) -t 24 --dump-vcd $(FIFO).vcd $(FIFO).smt2 |
$(SMTBMC) $(INDARGS) -t 24 --dump-vcd $(FIFO).vcd $(FIFO).smt2 |
$(SMTBMC) --presat $(BMCARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2 |
$(SMTBMC) $(INDARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2 |
touch $@ |
|
$(TX) : $(TX).check |
$(TX).check: $(TX).smt2 |
$(SMTBMC) --presat $(BMCARGS) -t 200 --dump-vcd $(TX).vcd $(TX).smt2 |
$(SMTBMC) $(INDARGS) -t 200 --dump-vcd $(TX).vcd $(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 $@ |
|
$(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 |
/trunk/bench/formal/rxuartlite.sby
0,0 → 1,22
[tasks] |
one |
two |
|
[options] |
mode prove |
multiclock on |
one: depth 20 |
two: depth 120 |
|
[engines] |
smtbmc |
|
[script] |
one: read_verilog -D RXUARTLITE -formal rxuartlite.v |
two: read_verilog -D RXUARTLITE -D PHASE_TWO -formal rxuartlite.v |
chparam -set CLOCKS_PER_BAUD 16 rxuartlite |
prep -top rxuartlite |
# opt_merge -share_all |
|
[files] |
../../rtl/rxuartlite.v |
/trunk/bench/formal/rxuartlite.ys
0,0 → 1,6
read_verilog -D TXUARTLITE -formal ../../rtl/rxuartlite.v |
chparam -set CLOCKS_PER_BAUD 16 |
prep -top rxuartlite -nordff |
clk2fflogic |
opt -share_all |
write_smt2 -wires rxuartlite.smt2 |
/trunk/bench/formal/txuartlite.sby
0,0 → 1,27
[tasks] |
verific |
yosys |
|
[options] |
mode prove |
depth 90 |
expect pass |
|
[engines] |
smtbmc yices |
|
[script] |
verific: |
verific -vlog-define VERIFIC_SVA |
verific -sv txuartlite.v |
verific -import -extnets -all txuartlite |
prep -top txuartlite |
-- |
|
yosys: |
read_verilog -DTXUARTLITE -formal txuartlite.v |
prep -top txuartlite |
-- |
|
[files] |
txuartlite.v |
/trunk/bench/formal/txuartlite.ys
1,5 → 1,4
read_verilog -D TXUARTLITE -formal ../../rtl/txuartlite.v |
prep -top txuartlite -nordff |
clk2fflogic |
opt -share_all |
write_smt2 -wires txuartlite.smt2 |
/trunk/bench/formal/ufifo.ys
1,5 → 1,4
read_verilog -D UFIFO -formal ../../rtl/ufifo.v |
prep -top ufifo -nordff |
clk2fflogic |
opt -share_all |
write_smt2 -wires ufifo.smt2 |