testsuite/gna: add tests for #1721

3 files changed, 43 insertions, 0 deletions

diff --git a/testsuite/gna/issue1721/testsuite.sh b/testsuite/gna/issue1721/testsuite.sh
index f3245dd6b..a0fd8a206 100755
--- a/testsuite/gna/issue1721/testsuite.sh
+++ b/testsuite/gna/issue1721/testsuite.sh
@@ -12,6 +12,9 @@ analyze_failure top2.vhdl
 analyze top3.vhdl
 elab_simulate top3
 
+analyze_failure top4.vhdl
+analyze_failure top5.vhdl
+
 clean
 
 echo "Test successful"
diff --git a/testsuite/gna/issue1721/top4.vhdl b/testsuite/gna/issue1721/top4.vhdl
new file mode 100644
index 000000000..5a123ef1f
--- /dev/null
+++ b/testsuite/gna/issue1721/top4.vhdl
@@ -0,0 +1,21 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity top4 is
+end entity;
+
+architecture a of top4 is
+    signal a,b,c,d : std_logic := '0';
+    signal clk_sys, clk1, clk2 : std_logic;
+begin
+  -- psl default clock is clk_sys;
+
+  -- 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);
+end;
diff --git a/testsuite/gna/issue1721/top5.vhdl b/testsuite/gna/issue1721/top5.vhdl
new file mode 100644
index 000000000..e6a0866fb
--- /dev/null
+++ b/testsuite/gna/issue1721/top5.vhdl
@@ -0,0 +1,19 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+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
+  -- psl default clock is clk_sys;
+
+  -- 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;