From 57cf7923209710dd45870ae42d38581747f81e99 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Tue, 16 Jun 2020 07:30:00 +0200 Subject: testsuite/gna: add a test for #1371 --- testsuite/gna/issue1371/incr_psl.vhdl | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 testsuite/gna/issue1371/incr_psl.vhdl (limited to 'testsuite/gna/issue1371/incr_psl.vhdl') 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; -- cgit v1.2.3