From 8c273a68cf38366a7e1cfd2df50d9025d9af7cce Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 16 May 2020 03:12:34 +0200 Subject: [PATCH] Issues can be built using make now --- .gitignore | 1 + issues/Makefile | 19 +++++++++++++++++++ issues/template.sby | 16 ++++++++++++++++ issues/tests.mk | 4 ++++ 4 files changed, 40 insertions(+) create mode 100644 issues/Makefile create mode 100644 issues/template.sby create mode 100644 issues/tests.mk 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