@ -1,2 +1,3 @@ | |||||
.DS_Store | .DS_Store | ||||
formal/work | formal/work | ||||
issues/work |
@ -0,0 +1,19 @@ | |||||
include tests.mk | |||||
.PHONY: all clean | |||||
all: ${psl_tests} | |||||
%: %.vhd work/%.sby | |||||
ghdl --synth --std=08 $@.vhd -e issue > work/$@_synth.vhd | |||||
-sby --yosys "yosys -m ghdl" -f -d work/$@ work/$@.sby bmc | |||||
work/%.sby: template.sby | |||||
mkdir -p work | |||||
sed 's/__ISSUE__/$(basename $(notdir $@))/g' $< > $@ | |||||
clean: | |||||
rm -rf work |
@ -0,0 +1,16 @@ | |||||
[tasks] | |||||
bmc | |||||
[options] | |||||
depth 25 | |||||
bmc: mode bmc | |||||
[engines] | |||||
bmc: smtbmc z3 | |||||
[script] | |||||
bmc: ghdl --std=08 __ISSUE__.vhd -e issue | |||||
prep -top issue | |||||
[files] | |||||
__ISSUE__.vhd |
@ -0,0 +1,4 @@ | |||||
psl_tests := \ | |||||
issue_1288 \ | |||||
issue_1292 \ | |||||
issue_1314 |