aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-09-07 12:40:19 +0200
committerClifford Wolf <clifford@clifford.at>2016-09-07 12:40:19 +0200
commit44d6feba2aab35eb8fbb504e41dfba6b471a74da (patch)
tree2275e57b8278bd28cda58cd6d704da800b62430a /Makefile
parentda3749819197875c10eeec54551401ac19090902 (diff)
downloadpicorv32-44d6feba2aab35eb8fbb504e41dfba6b471a74da.tar.gz
picorv32-44d6feba2aab35eb8fbb504e41dfba6b471a74da.zip
Using assertpmux in "make check"
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 347fcb8..c03792f 100644
--- a/Makefile
+++ b/Makefile
@@ -23,11 +23,12 @@ check: check-yices
check-%: check.smt2
yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd check.smt2
- yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd -i check.smt2
+ yosys-smtbmc -s $(subst check-,,$@) -t 20 --dump-vcd check.vcd -i check.smt2
check.smt2: picorv32.v
yosys -v2 -p 'read_verilog -formal picorv32.v' \
-p 'prep -top picorv32 -nordff' \
+ -p 'assertpmux -noinit; opt -fast' \
-p 'write_smt2 -wires check.smt2'
test_sp: testbench_sp.vvp firmware/firmware.hex