aboutsummaryrefslogtreecommitdiffstats
path: root/testsuite/gna
diff options
context:
space:
mode:
authorPepijn de Vos <pepijndevos@gmail.com>2019-08-07 04:20:14 +0200
committertgingold <tgingold@users.noreply.github.com>2019-08-07 04:20:14 +0200
commit0331772c3ef05bad40b748542939ccafab2a9c68 (patch)
treeca0dd705571b8a031c02b6934d9e9fe85151b042 /testsuite/gna
parentce416ec62d20f1a592835efe5cbe49856d7085a2 (diff)
downloadghdl-0331772c3ef05bad40b748542939ccafab2a9c68.tar.gz
ghdl-0331772c3ef05bad40b748542939ccafab2a9c68.tar.bz2
ghdl-0331772c3ef05bad40b748542939ccafab2a9c68.zip
Add support for PSL assumptions, used in formal verification (#880)
* vhdl: make the parser understand PSL assume * assume does not actually have report according to the spec. Just a property. * add SPL assume to semantic analysis * canonicalise PSL assume * add assume to annotations * add PSL assume to simulation code * statement -> directive * add assume to translation files * update ticked24 testcase * correctly parse assume * add assume testcase * refactor chunk of duplicated code
Diffstat (limited to 'testsuite/gna')
-rw-r--r--testsuite/gna/issue880/psl.ref30
-rw-r--r--testsuite/gna/issue880/psl.vhdl30
-rwxr-xr-xtestsuite/gna/issue880/testsuite.sh41
-rw-r--r--testsuite/gna/ticket24/psl.ref3
4 files changed, 104 insertions, 0 deletions
diff --git a/testsuite/gna/issue880/psl.ref b/testsuite/gna/issue880/psl.ref
new file mode 100644
index 000000000..5fd471f5d
--- /dev/null
+++ b/testsuite/gna/issue880/psl.ref
@@ -0,0 +1,30 @@
+{ "details" : [
+ { "directive": "assumption",
+ "name": ".psl(behav).a1",
+ "file": "psl.vhdl",
+ "line": 27,
+ "count": 0,
+ "status": "passed"},
+ { "directive": "assumption",
+ "name": ".psl(behav).a2",
+ "file": "psl.vhdl",
+ "line": 28,
+ "count": 0,
+ "status": "passed"},
+ { "directive": "cover",
+ "name": ".psl(behav).c1",
+ "file": "psl.vhdl",
+ "line": 29,
+ "count": 3,
+ "status": "covered"}],
+ "summary" : {
+ "assert": 0,
+ "assert-failure": 0,
+ "assert-pass": 0,
+ "assume": 2,
+ "assume-failure": 0,
+ "assume-pass": 2,
+ "cover": 1,
+ "cover-failure": 0,
+ "cover-pass": 1}
+}
diff --git a/testsuite/gna/issue880/psl.vhdl b/testsuite/gna/issue880/psl.vhdl
new file mode 100644
index 000000000..a1e203f5f
--- /dev/null
+++ b/testsuite/gna/issue880/psl.vhdl
@@ -0,0 +1,30 @@
+entity psl is
+end;
+
+architecture behav of psl is
+ signal a, b, c : bit;
+ signal clk : bit;
+ subtype wf_type is bit_vector (0 to 7);
+ constant wave_a : wf_type := "10010100";
+ constant wave_b : wf_type := "01001010";
+ constant wave_c : wf_type := "00100101";
+begin
+ process
+ begin
+ for i in wf_type'range loop
+ clk <= '0';
+ wait for 1 ns;
+ a <= wave_a (i);
+ b <= wave_b (i);
+ c <= wave_c (i);
+ clk <= '1';
+ wait for 1 ns;
+ end loop;
+ wait;
+ end process;
+
+ -- psl default clock is (clk'event and clk = '1');
+ -- psl a1: assume always a |=> b;
+ -- psl a2: assume always a -> eventually! c;
+ -- psl c1: cover {a;b;c};
+end behav;
diff --git a/testsuite/gna/issue880/testsuite.sh b/testsuite/gna/issue880/testsuite.sh
new file mode 100755
index 000000000..136317e17
--- /dev/null
+++ b/testsuite/gna/issue880/testsuite.sh
@@ -0,0 +1,41 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+GHDL_STD_FLAGS="-fpsl"
+analyze psl.vhdl
+elab psl
+if ghdl_has_feature psl psl; then
+ simulate psl --psl-report=psl.out
+
+ if ! diff --strip-trailing-cr psl.out psl.ref > /dev/null; then
+ echo "report mismatch"
+ exit 1
+ fi
+
+ rm -f psl.out
+fi
+clean
+
+# Using vhdl 08
+GHDL_STD_FLAGS="-fpsl --std=08"
+analyze psl.vhdl
+elab -fpsl psl
+if ghdl_has_feature psl psl; then
+ simulate psl --psl-report=psl.out
+
+ diff --strip-trailing-cr -q psl.out psl.ref
+
+ rm -f psl.out
+fi
+clean
+
+# Usage example (python 2.7):
+#
+# import json
+# d=json.load(open("psl.out"))
+# print d['summary']
+# {u'assert-pass': 2, u'cover': 1, ... }
+# print d['summary']['assert']
+
+echo "Test successful"
diff --git a/testsuite/gna/ticket24/psl.ref b/testsuite/gna/ticket24/psl.ref
index 6a5588a3a..9cd8cdb35 100644
--- a/testsuite/gna/ticket24/psl.ref
+++ b/testsuite/gna/ticket24/psl.ref
@@ -21,6 +21,9 @@
"assert": 2,
"assert-failure": 0,
"assert-pass": 2,
+ "assume": 0,
+ "assume-failure": 0,
+ "assume-pass": 0,
"cover": 1,
"cover-failure": 0,
"cover-pass": 1}