diff --git a/.gitignore b/.gitignore index adf4d5c..fc7b227 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .DS_Store formal/work +issues/work diff --git a/issues/Makefile b/issues/Makefile new file mode 100644 index 0000000..13f6d28 --- /dev/null +++ b/issues/Makefile @@ -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 diff --git a/issues/template.sby b/issues/template.sby new file mode 100644 index 0000000..fe3a495 --- /dev/null +++ b/issues/template.sby @@ -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 diff --git a/issues/tests.mk b/issues/tests.mk new file mode 100644 index 0000000..d64fc56 --- /dev/null +++ b/issues/tests.mk @@ -0,0 +1,4 @@ +psl_tests := \ +issue_1288 \ +issue_1292 \ +issue_1314 \ No newline at end of file