diff options
Diffstat (limited to 'testsuite/synth/issue662/psl_rose.vhdl')
| -rw-r--r-- | testsuite/synth/issue662/psl_rose.vhdl | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/testsuite/synth/issue662/psl_rose.vhdl b/testsuite/synth/issue662/psl_rose.vhdl new file mode 100644 index 000000000..83e9a6c04 --- /dev/null +++ b/testsuite/synth/issue662/psl_rose.vhdl @@ -0,0 +1,25 @@ +library ieee; +use ieee.std_logic_1164.all; + +entity psl_rose is + port (clk, a, b : in std_logic + ); +end entity psl_rose; + + +architecture psl of psl_rose is +begin + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- This assertion holds + ROSE_0_a : assert always {not a; a} |-> rose(a); + + -- This assertion holds + ROSE_1_a : assert always (rose(a) -> (prev(a) = '0' and a = '1')); + + -- This assertion should fail at cycle 11 + ROSE_2_a : assert always rose(a) -> b; + +end architecture psl; |
