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;  | 
