From dbd1c189a8fff1e7c322ffd7264ea339bf911115 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Wed, 15 Mar 2023 07:45:53 +0100
Subject: testsuite: add a test for #2392

---
 .../ghdl-issues/issue2392b/compare_psl_p_plus.sby  | 20 ++++++
 .../ghdl-issues/issue2392b/compare_psl_p_plus.vhdl | 77 ++++++++++++++++++++++
 testsuite/ghdl-issues/issue2392b/psl_p_plus.vhdl   | 22 +++++++
 testsuite/ghdl-issues/issue2392b/psl_p_plus.ys     | 12 ++++
 testsuite/ghdl-issues/issue2392b/testsuite.sh      | 10 +++
 5 files changed, 141 insertions(+)
 create mode 100644 testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.sby
 create mode 100644 testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.vhdl
 create mode 100644 testsuite/ghdl-issues/issue2392b/psl_p_plus.vhdl
 create mode 100644 testsuite/ghdl-issues/issue2392b/psl_p_plus.ys
 create mode 100755 testsuite/ghdl-issues/issue2392b/testsuite.sh

diff --git a/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.sby b/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.sby
new file mode 100644
index 0000000..44cf671
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.sby
@@ -0,0 +1,20 @@
+[tasks]
+compare
+cover
+
+[options]
+compare: mode bmc
+cover: mode cover
+depth 100
+
+[engines]
+smtbmc z3
+
+[script]
+read_verilog synth_psl_p_plus.v
+ghdl --std=08 compare_psl_p_plus.vhdl -e compare_psl_p_plus
+prep -top compare_psl_p_plus
+
+[files]
+synth_psl_p_plus.v
+compare_psl_p_plus.vhdl
diff --git a/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.vhdl b/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.vhdl
new file mode 100644
index 0000000..90f9d3a
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392b/compare_psl_p_plus.vhdl
@@ -0,0 +1,77 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity compare_psl_p_plus is
+    port(
+        clk_in: in std_logic;
+		a_in: in std_logic;
+		b_in: in std_logic;
+		c_in: in std_logic
+    );
+end;
+
+architecture rtl of compare_psl_p_plus is
+    component psl_p_plus is
+        port(
+            clk_in: in std_logic;
+            a_in: in std_logic;
+            b_in: in std_logic;
+            c_in: in std_logic;
+            \p_plus_psl.A\: out std_logic;
+            \p_plus_psl.EN\: out std_logic
+        );
+    end component;
+	
+	signal first_cycle: std_logic := '1';
+	signal nda_r0: std_logic := '0';
+	signal nda_res: std_logic;
+
+    signal p_plus_psl_a: std_logic;
+    signal p_plus_psl_en: std_logic;
+    signal p_plus_psl: std_logic;
+begin
+    dut: psl_p_plus
+        port map(
+            clk_in => clk_in,
+            a_in => a_in,
+            b_in => b_in,
+            c_in => c_in,
+            \p_plus_psl.A\ => p_plus_psl_a,
+            \p_plus_psl.EN\ => p_plus_psl_en
+        );
+	
+	p_plus_psl <= p_plus_psl_en and p_plus_psl_a;
+	
+	reference_model_sync_pr: process(clk_in)
+	begin
+		if rising_edge(clk_in) then
+			first_cycle <= '0';
+		
+			nda_r0 <= '0';
+			if first_cycle = '1' and a_in = '1' then
+				nda_r0 <= '1';
+			end if;
+			if nda_r0 = '1' and a_in = '1' then
+				nda_r0 <= '1';
+			end if;
+		end if;
+	end process;
+	
+	reference_model_async_pr: process(all)
+	begin
+		nda_res <= '1';
+		if nda_r0 = '1' and b_in = '1' and c_in = '0' then
+			nda_res <= '0';
+		end if;
+	end process;
+	
+    
+    default clock is rising_edge(clk_in);
+
+    comparison_assert: postponed assert nda_res = p_plus_psl;
+
+    cover_psl: cover {true; true; p_plus_psl = '0'};
+
+    cover_psl_first: cover {true; true; [*]; p_plus_psl = '0'};
+end;
+
diff --git a/testsuite/ghdl-issues/issue2392b/psl_p_plus.vhdl b/testsuite/ghdl-issues/issue2392b/psl_p_plus.vhdl
new file mode 100644
index 0000000..522ce86
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392b/psl_p_plus.vhdl
@@ -0,0 +1,22 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity psl_p_plus is
+	generic(
+		DATA_BITS: natural := 8
+	);
+	port(
+		clk_in: in std_logic;
+		
+		a_in: in std_logic;
+		b_in: in std_logic;
+		c_in: in std_logic
+	);
+end;
+
+architecture psl of psl_p_plus is
+begin
+	default clock is rising_edge(clk_in);
+	
+	p_plus_psl: assert {a_in[+]; b_in} |-> {c_in};
+end;
diff --git a/testsuite/ghdl-issues/issue2392b/psl_p_plus.ys b/testsuite/ghdl-issues/issue2392b/psl_p_plus.ys
new file mode 100644
index 0000000..d1a4972
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392b/psl_p_plus.ys
@@ -0,0 +1,12 @@
+ghdl --std=08 psl_p_plus.vhdl -e psl_p_plus
+
+flatten
+rename -enumerate -pattern unnamed_assert_% t:$assert
+rename -enumerate -pattern unnamed_assume_% t:$assume
+rename -enumerate -pattern unnamed_cover_% t:$cover
+
+expose -evert t:$assert t:$assume t:$cover
+
+opt
+
+write_verilog synth_psl_p_plus.v
diff --git a/testsuite/ghdl-issues/issue2392b/testsuite.sh b/testsuite/ghdl-issues/issue2392b/testsuite.sh
new file mode 100755
index 0000000..66e1f8c
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392b/testsuite.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+topdir=../..
+. $topdir/testenv.sh
+
+run_yosys psl_p_plus.ys
+
+run_symbiyosys -f compare_psl_p_plus.sby compare cover
+
+echo OK
-- 
cgit v1.2.3