diff options
-rwxr-xr-x | testsuite/gna/issue1721/testsuite.sh | 3 | ||||
-rw-r--r-- | testsuite/gna/issue1721/top4.vhdl | 21 | ||||
-rw-r--r-- | testsuite/gna/issue1721/top5.vhdl | 19 |
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; |