testsuite/gna: add a test for #1721

3 files changed, 80 insertions, 0 deletions

diff --git a/testsuite/gna/issue1721/orig.vhdl b/testsuite/gna/issue1721/orig.vhdl
new file mode 100644
index 000000000..c4c32111d
--- /dev/null
+++ b/testsuite/gna/issue1721/orig.vhdl
@@ -0,0 +1,52 @@
+entity top5 is
+end entity;
+
+architecture a of top5 is
+    signal a,b,c,d : std_logic := '0';
+    signal clk_sys, clk1, clk2 : std_logic;
+begin
+
+  -- Following throws bug occured with:
+  --  "psl.sem_property: cannot handle N_CLOCKED_SER"
+  -- Clocked SERE shall be allowed according to 6.1.1.1 of PSL LRM 2003
+  -- psl my_seq : assert never {a;b;c} @ rising_edge(clk_sys);
+
+  -- Following throws bug occured with: "build_sere_fa: cannot handle N_IMP_SEQ"
+  -- This is strange because with "always" this is working.
+  -- According to PSL LRM 2003 FL_Property production for "always" is the
+  -- same as for "never":
+  --   FL_Property ::=
+  --        always FL_Property
+  --      | always Sequence
+  --
+  --   FL_Property ::=
+  --        never FL_Property
+  --      | never Sequence
+  -- Therefore I think if sequence implication works with one, it shall work
+  -- also with other.
+  -- psl my_seq : assert never {a} |=> {b; c};
+
+  -- Following error is thrown: "translate_psl_expr: cannot handle N_IMP_BOOL"
+  -- Combination of "never" + implication is not very usefull, since
+  -- implication is always true apart from case where 1 -> 0, therefore it
+  -- will mostly fail, however, it should not crash tool (the same goes for
+  -- previous case too)
+  -- psl my_seq : assert never (a -> b);
+
+  -- Following error is thrown:
+  --  "top.vhd:43:28:error: operand of a 'never' operator must be a boolean
+  --   or a sequence"
+  -- While for "assert always", this works. IMHO this should work for both,
+  -- equally since productions for never|always are the same.
+  -- It is not true that operand of never must be a boolean or a sequence.
+  -- It can be FL_property or sequence, which is much wider set.
+  -- psl my_seq : assert never (a) -> eventually! (b);
+  
+  -- Following error is thrown:
+  -- "top.vhd:43:58:error: left-hand side operand of logical '->' must be
+  --  a boolean"
+  -- This is not true, LHS and RHS of implication shall be FL_Property, not
+  -- just boolean (6.2.1.6.1)
+  -- psl my_seq : assert always (a -> next b -> next c -> next d);
+
+end;
diff --git a/testsuite/gna/issue1721/testsuite.sh b/testsuite/gna/issue1721/testsuite.sh
new file mode 100755
index 000000000..70c249139
--- /dev/null
+++ b/testsuite/gna/issue1721/testsuite.sh
@@ -0,0 +1,12 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+export GHDL_STD_FLAGS=-fpsl
+
+analyze top1.vhdl
+elab_simulate top1
+
+clean
+
+echo "Test successful"
diff --git a/testsuite/gna/issue1721/top1.vhdl b/testsuite/gna/issue1721/top1.vhdl
new file mode 100644
index 000000000..821e1ba91
--- /dev/null
+++ b/testsuite/gna/issue1721/top1.vhdl
@@ -0,0 +1,16 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity top1 is
+end entity;
+
+architecture a of top1 is
+    signal a,b,c,d : std_logic := '0';
+    signal clk_sys, clk1, clk2 : std_logic;
+begin
+
+  -- Following throws bug occured with:
+  --  "psl.sem_property: cannot handle N_CLOCKED_SER"
+  -- Clocked SERE shall be allowed according to 6.1.1.1 of PSL LRM 2003
+  -- psl my_seq : assert never {a;b;c} @ rising_edge(clk_sys);
+end a;