Add testcase for ticket24

3 files changed, 81 insertions, 0 deletions

diff --git a/testsuite/gna/ticket24/psl.ref b/testsuite/gna/ticket24/psl.ref
new file mode 100644
index 000000000..6a5588a3a
--- /dev/null
+++ b/testsuite/gna/ticket24/psl.ref
@@ -0,0 +1,27 @@
+{ "details" : [
+ { "directive": "assertion",
+   "name": ".psl(behav).a1",
+   "file": "psl.vhdl",
+   "line": 27,
+   "count": 0,
+   "status": "passed"},
+ { "directive": "assertion",
+   "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": 2,
+  "assert-failure": 0,
+  "assert-pass": 2,
+  "cover": 1,
+  "cover-failure": 0,
+  "cover-pass": 1}
+}
diff --git a/testsuite/gna/ticket24/psl.vhdl b/testsuite/gna/ticket24/psl.vhdl
new file mode 100644
index 000000000..a838b8fd2
--- /dev/null
+++ b/testsuite/gna/ticket24/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: assert always a |=> b;
+  -- psl a2: assert always a -> eventually! c;
+  -- psl c1: cover {a;b;c};
+end behav;
diff --git a/testsuite/gna/ticket24/testsuite.sh b/testsuite/gna/ticket24/testsuite.sh
new file mode 100755
index 000000000..96b37c948
--- /dev/null
+++ b/testsuite/gna/ticket24/testsuite.sh
@@ -0,0 +1,24 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+analyze -fpsl psl.vhdl
+elab_simulate -fpsl psl --psl-report=psl.out
+
+if ! cmp psl.out psl.ref; then
+    echo "report mismatch"
+    exit 1
+fi
+
+# 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']
+
+rm -f psl.out
+clean
+
+echo "Test successful"