testsuite/gna: add a test for #1371

2 files changed, 36 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;
diff --git a/testsuite/gna/issue1371/testsuite.sh b/testsuite/gna/issue1371/testsuite.sh
new file mode 100755
index 000000000..c13fca038
--- /dev/null
+++ b/testsuite/gna/issue1371/testsuite.sh
@@ -0,0 +1,10 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+export GHDL_STD_FLAGS=-fpsl
+analyze incr_psl.vhdl
+
+clean
+
+echo "Test successful"