aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rwxr-xr-xtestsuite/gna/issue1721/testsuite.sh3
-rw-r--r--testsuite/gna/issue1721/top4.vhdl21
-rw-r--r--testsuite/gna/issue1721/top5.vhdl19
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;