testsuite: add a test, close ghdl/ghdl#2373

6 files changed, 230 insertions, 0 deletions

diff --git a/testsuite/ghdl-issues/issue2373/async_test-plus.sby b/testsuite/ghdl-issues/issue2373/async_test-plus.sby
new file mode 100644
index 0000000..de26b36
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/async_test-plus.sby
@@ -0,0 +1,23 @@
+[tasks]
+prove
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode bmc
+depth 50
+
+[engines]
+prove: smtbmc z3
+
+[script]
+ghdl --std=08 dut.vhdl tb_dut-plus.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut-star.vhdl
+tb_dut-plus.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2373/async_test-star.sby b/testsuite/ghdl-issues/issue2373/async_test-star.sby
new file mode 100644
index 0000000..ef26a1f
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/async_test-star.sby
@@ -0,0 +1,23 @@
+[tasks]
+prove
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode bmc
+depth 50
+
+[engines]
+prove: smtbmc z3
+
+[script]
+ghdl --std=08 dut.vhdl tb_dut-star.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut-star.vhdl
+tb_dut-plus.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2373/dut.vhdl b/testsuite/ghdl-issues/issue2373/dut.vhdl
new file mode 100644
index 0000000..2ab001a
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/dut.vhdl
@@ -0,0 +1,51 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity dut is
+	port(
+		clk_in: in std_logic;
+
+		a1_in: in std_logic;
+		b1_out: out std_logic;
+
+		a2_in: in std_logic;
+		b2_out: out std_logic
+	);
+end;
+
+architecture rtl of dut is
+	signal cnt: integer range 0 to 20 := 0;
+
+	signal a2_prev: std_logic := '0';
+begin
+	process(clk_in)
+	begin
+		if rising_edge(clk_in) then
+			if cnt /= 20 then
+				cnt <= cnt + 1;
+			end if;
+		end if;
+	end process;
+
+	process(clk_in)
+	begin
+		if rising_edge(clk_in) then
+			a2_prev <= a2_in;
+
+			b1_out <= not a1_in;
+			if cnt = 20 then
+				b1_out <= a1_in;
+			end if;
+		end if;
+	end process;
+
+	process(all)
+	begin
+		b2_out <= a2_prev;
+		if cnt = 20 then
+			b2_out <= not a2_in;
+		end if;
+		b2_out <= not a2_in;
+	end process;
+end;
+
diff --git a/testsuite/ghdl-issues/issue2373/tb_dut-plus.vhdl b/testsuite/ghdl-issues/issue2373/tb_dut-plus.vhdl
new file mode 100644
index 0000000..2397da2
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/tb_dut-plus.vhdl
@@ -0,0 +1,57 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity tb_dut is
+	port(
+		clk_in: in std_logic;
+
+		dut1_a1_in: in std_logic;
+		dut1_b1_out: out std_logic;
+		dut1_a2_in: in std_logic;
+		dut1_b2_out: out std_logic;
+
+		dut2_a1_in: in std_logic;
+		dut2_b1_out: out std_logic;
+		dut2_a2_in: in std_logic;
+		dut2_b2_out: out std_logic
+	);
+end;
+
+architecture tb of tb_dut is
+begin
+	dut_1: entity work.dut
+		port map(
+			clk_in => clk_in,
+	                a1_in => dut1_a1_in,
+			b1_out => dut1_b1_out,
+			a2_in => dut1_a2_in,
+			b2_out => dut1_b2_out
+		);
+
+	dut_2: entity work.dut
+		port map(
+			clk_in => clk_in,
+			a1_in => dut2_a1_in,
+			b1_out => dut2_b1_out,
+			a2_in => dut2_a2_in,
+			b2_out => dut2_b2_out
+		);
+
+
+
+	default clock is rising_edge(clk_in);
+
+--	stability_1: assert 
+--	  {(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[+];
+	  -- {(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[*1 to inf];
+--	  	dut1_a1_in /= dut2_a1_in and dut1_a2_in = dut2_a2_in} |->
+--	  {dut1_b1_out = dut2_b1_out}!;
+
+	stability_2: assert 
+		{(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[+];
+		-- {(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[*1 to inf];
+			dut1_a1_in = dut2_a1_in and dut1_a2_in /= dut2_a2_in} |->
+		{dut1_b2_out = dut2_b2_out}!;
+
+end;
+
diff --git a/testsuite/ghdl-issues/issue2373/tb_dut-star.vhdl b/testsuite/ghdl-issues/issue2373/tb_dut-star.vhdl
new file mode 100644
index 0000000..32dfd33
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/tb_dut-star.vhdl
@@ -0,0 +1,57 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity tb_dut is
+	port(
+		clk_in: in std_logic;
+
+		dut1_a1_in: in std_logic;
+		dut1_b1_out: out std_logic;
+		dut1_a2_in: in std_logic;
+		dut1_b2_out: out std_logic;
+
+		dut2_a1_in: in std_logic;
+		dut2_b1_out: out std_logic;
+		dut2_a2_in: in std_logic;
+		dut2_b2_out: out std_logic
+	);
+end;
+
+architecture tb of tb_dut is
+begin
+	dut_1: entity work.dut
+		port map(
+			clk_in => clk_in,
+	                a1_in => dut1_a1_in,
+			b1_out => dut1_b1_out,
+			a2_in => dut1_a2_in,
+			b2_out => dut1_b2_out
+		);
+
+	dut_2: entity work.dut
+		port map(
+			clk_in => clk_in,
+			a1_in => dut2_a1_in,
+			b1_out => dut2_b1_out,
+			a2_in => dut2_a2_in,
+			b2_out => dut2_b2_out
+		);
+
+
+
+	default clock is rising_edge(clk_in);
+
+--	stability_1: assert 
+--		{(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[+];
+--		{(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[*1 to inf];
+--			dut1_a1_in /= dut2_a1_in and dut1_a2_in = dut2_a2_in} |->
+--		{dut1_b1_out = dut2_b1_out}!;
+
+	stability_2: assert 
+--        {(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[+];
+	  {(dut1_a1_in = dut2_a1_in and dut1_a2_in = dut2_a2_in)[*1 to inf];
+		dut1_a1_in = dut2_a1_in and dut1_a2_in /= dut2_a2_in} |->
+		{dut1_b2_out = dut2_b2_out}!;
+
+end;
+
diff --git a/testsuite/ghdl-issues/issue2373/testsuite.sh b/testsuite/ghdl-issues/issue2373/testsuite.sh
new file mode 100755
index 0000000..deb3f23
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2373/testsuite.sh
@@ -0,0 +1,19 @@
+#!/bin/sh
+
+topdir=../..
+. $topdir/testenv.sh
+
+run_symbiyosys -fd work  async_test-plus.sby prove || true
+if ! grep -q "BMC failed" work/engine_0/logfile.txt; then
+    echo "failure expected"
+    exit 1
+fi
+
+run_symbiyosys -fd work  async_test-star.sby prove || true
+if ! grep -q "BMC failed" work/engine_0/logfile.txt; then
+    echo "failure expected"
+    exit 1
+fi
+
+clean
+echo OK