diff options
Diffstat (limited to 'testsuite/gna/issue2157/repro2.vhdl')
| -rw-r--r-- | testsuite/gna/issue2157/repro2.vhdl | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/testsuite/gna/issue2157/repro2.vhdl b/testsuite/gna/issue2157/repro2.vhdl new file mode 100644 index 000000000..1b0fd5b0f --- /dev/null +++ b/testsuite/gna/issue2157/repro2.vhdl @@ -0,0 +1,34 @@ +library ieee; + use ieee.std_logic_1164.all; + +entity repro is + port ( + a, c, d, e, f, x : std_logic; + b : std_logic_vector(3 downto 0); + clk : in std_logic + ); +end; + +architecture psl of repro is +begin + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + NEXT_EVENT_0_a : +-- assert always ((a and b = x"4") -> next_event_a(c)[1 to 2](b = x"4")) +-- assert always ((a and b = x"4") -> ({(not c)[*]; c; {[*0] | { (not c)[*]; c}}} |->(b = x"4"))) +-- assert always (a -> ({c; d; {[*0] | {(not e)[*];f}}} |->x)) +-- assert always (a -> ({c; {[*0] | {d[*]; e}}} |->x)) +-- assert always ({c; {[*0] | {d[*]; e}}} |->x) +-- assert never {c; {[*0] | {d[*]; e}}} +-- assert always ({c | {c; d[*]; e}} |->x) +-- assert always ({c; {d[*]; e}} |->x) + report "NEXT_EVENT_0_a failed"; +end architecture psl; + +-- next_event_a(b)[k:l](p) = {b[->k:l]} |-> p +-- b[->k:l] = b[->k] | ... | b[->l] +-- = {!b[*];b}[*k:l] +-- s[*i:j] = s[*i] | ... | s[*j] + +-- next_event_a(b)[k:l](p) = {{!b[*];b}[*k] | .. | {!b[*];b}[*l] } |-> p |