diff options
Diffstat (limited to 'testsuite/gna/issue1371/incr_psl.vhdl')
-rw-r--r-- | testsuite/gna/issue1371/incr_psl.vhdl | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/testsuite/gna/issue1371/incr_psl.vhdl b/testsuite/gna/issue1371/incr_psl.vhdl new file mode 100644 index 000000000..87e0d8c0b --- /dev/null +++ b/testsuite/gna/issue1371/incr_psl.vhdl @@ -0,0 +1,26 @@ +library IEEE; +use IEEE.STD_LOGIC_1164.ALL; +use IEEE.NUMERIC_STD.ALL; + +-- This could be combinational but GHDL does not support @(True) PSL yet +entity incr_psl is + Port ( + clk: in STD_LOGIC; + in_val: in UNSIGNED(7 downto 0); + out_val: out UNSIGNED(7 downto 0) + ); +end entity; + +architecture Behavioral of incr_psl is + signal out_val_internal: UNSIGNED(7 downto 0); +begin + out_val_internal <= in_val + 1; + out_val <= out_val_internal; + -- psl default clock is rising_edge(clk); + + -- The combination of the two below work + -- psl assert always (in_val = 0 -> out_val_internal = 1); + -- psl assert always (out_val_internal = 1 -> in_val = 0); + -- This causes an error + -- psl assert always (in_val = 0 <-> out_val_internal = 1); +end Behavioral; |