testsuite: add a test for #2392

10 files changed, 548 insertions, 0 deletions

diff --git a/testsuite/ghdl-issues/issue2392/async_test-0.sby b/testsuite/ghdl-issues/issue2392/async_test-0.sby
new file mode 100644
index 0000000..af08f14
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/async_test-0.sby
@@ -0,0 +1,22 @@
+[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-0.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut-0.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2392/async_test-1.sby b/testsuite/ghdl-issues/issue2392/async_test-1.sby
new file mode 100644
index 0000000..33c9078
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/async_test-1.sby
@@ -0,0 +1,22 @@
+[tasks]
+prove
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode bmc
+depth 50
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 dut.vhdl tb_dut-1.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut-1.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2392/async_test-2.sby b/testsuite/ghdl-issues/issue2392/async_test-2.sby
new file mode 100644
index 0000000..cc663fc
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/async_test-2.sby
@@ -0,0 +1,22 @@
+[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-2.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut-2.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2392/async_test.sby b/testsuite/ghdl-issues/issue2392/async_test.sby
new file mode 100644
index 0000000..734ed90
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/async_test.sby
@@ -0,0 +1,22 @@
+[tasks]
+prove
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+prove: mode bmc
+depth 50
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 dut.vhdl tb_dut.vhdl -e tb_dut
+prep -top tb_dut
+
+[files]
+dut.vhdl
+tb_dut.vhdl
+
diff --git a/testsuite/ghdl-issues/issue2392/dut.vhdl b/testsuite/ghdl-issues/issue2392/dut.vhdl
new file mode 100644
index 0000000..d21c825
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/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 := '0';
+
+		a2_in: in std_logic;
+		b2_out: out std_logic := '0'
+	);
+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/issue2392/tb_dut-0.vhdl b/testsuite/ghdl-issues/issue2392/tb_dut-0.vhdl
new file mode 100644
index 0000000..f1f5f07
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/tb_dut-0.vhdl
@@ -0,0 +1,97 @@
+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
+	signal all_inputs_equal: std_logic;
+	signal a1_differ: std_logic;
+	signal a2_differ: std_logic;
+
+	signal b1_equal: std_logic;
+	signal b2_equal: std_logic;
+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
+		);
+
+	-- Formal part =>
+
+	process(all)
+	begin
+		all_inputs_equal <= '1';
+		if dut1_a1_in /= dut2_a1_in or dut1_a2_in /= dut2_a2_in then
+			all_inputs_equal <= '0';
+		end if;
+
+		a1_differ <= '0';
+		if dut1_a1_in /= dut2_a1_in then
+			a1_differ <= '1';
+		end if;
+
+		a2_differ <= '0';
+		if dut1_a2_in /= dut2_a2_in then
+			a2_differ <= '1';
+		end if;
+
+		b1_equal <= '0';
+		if dut1_b1_out = dut2_b1_out then
+			b1_equal <= '1';
+		end if;
+
+		b2_equal <= '0';
+		if dut1_b2_out = dut2_b2_out then
+			b2_equal <= '1';
+		end if;
+	end process;
+
+	default clock is rising_edge(clk_in);
+
+	b1_nonasync: assert {all_inputs_equal[*1 to inf]; a1_differ} |-> {b1_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+--	b2_nonasync_1: assert {all_inputs_equal[*1 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+--	b2_nonasync_2: assert {all_inputs_equal[+]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_3: assert {all_inputs_equal[*2 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_4: assert {all_inputs_equal[*0 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_5: assert {all_inputs_equal[*]; a2_differ} |-> {b2_equal};
+
+
+	--cover_tester: cover {all_inputs_equal[*21]; a2_differ; all_inputs_equal[*5]};
+end;
diff --git a/testsuite/ghdl-issues/issue2392/tb_dut-1.vhdl b/testsuite/ghdl-issues/issue2392/tb_dut-1.vhdl
new file mode 100644
index 0000000..5997723
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/tb_dut-1.vhdl
@@ -0,0 +1,97 @@
+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
+	signal all_inputs_equal: std_logic;
+	signal a1_differ: std_logic;
+	signal a2_differ: std_logic;
+
+	signal b1_equal: std_logic;
+	signal b2_equal: std_logic;
+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
+		);
+
+	-- Formal part =>
+
+	process(all)
+	begin
+		all_inputs_equal <= '1';
+		if dut1_a1_in /= dut2_a1_in or dut1_a2_in /= dut2_a2_in then
+			all_inputs_equal <= '0';
+		end if;
+
+		a1_differ <= '0';
+		if dut1_a1_in /= dut2_a1_in then
+			a1_differ <= '1';
+		end if;
+
+		a2_differ <= '0';
+		if dut1_a2_in /= dut2_a2_in then
+			a2_differ <= '1';
+		end if;
+
+		b1_equal <= '0';
+		if dut1_b1_out = dut2_b1_out then
+			b1_equal <= '1';
+		end if;
+
+		b2_equal <= '0';
+		if dut1_b2_out = dut2_b2_out then
+			b2_equal <= '1';
+		end if;
+	end process;
+
+	default clock is rising_edge(clk_in);
+
+--	b1_nonasync: assert {all_inputs_equal[*1 to inf]; a1_differ} |-> {b1_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+	b2_nonasync_1: assert {all_inputs_equal[*1 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+--	b2_nonasync_2: assert {all_inputs_equal[+]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_3: assert {all_inputs_equal[*2 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_4: assert {all_inputs_equal[*0 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_5: assert {all_inputs_equal[*]; a2_differ} |-> {b2_equal};
+
+
+	--cover_tester: cover {all_inputs_equal[*21]; a2_differ; all_inputs_equal[*5]};
+end;
diff --git a/testsuite/ghdl-issues/issue2392/tb_dut-2.vhdl b/testsuite/ghdl-issues/issue2392/tb_dut-2.vhdl
new file mode 100644
index 0000000..e7553ec
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/tb_dut-2.vhdl
@@ -0,0 +1,97 @@
+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
+	signal all_inputs_equal: std_logic;
+	signal a1_differ: std_logic;
+	signal a2_differ: std_logic;
+
+	signal b1_equal: std_logic;
+	signal b2_equal: std_logic;
+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
+		);
+
+	-- Formal part =>
+
+	process(all)
+	begin
+		all_inputs_equal <= '1';
+		if dut1_a1_in /= dut2_a1_in or dut1_a2_in /= dut2_a2_in then
+			all_inputs_equal <= '0';
+		end if;
+
+		a1_differ <= '0';
+		if dut1_a1_in /= dut2_a1_in then
+			a1_differ <= '1';
+		end if;
+
+		a2_differ <= '0';
+		if dut1_a2_in /= dut2_a2_in then
+			a2_differ <= '1';
+		end if;
+
+		b1_equal <= '0';
+		if dut1_b1_out = dut2_b1_out then
+			b1_equal <= '1';
+		end if;
+
+		b2_equal <= '0';
+		if dut1_b2_out = dut2_b2_out then
+			b2_equal <= '1';
+		end if;
+	end process;
+
+	default clock is rising_edge(clk_in);
+
+--	b1_nonasync: assert {all_inputs_equal[*1 to inf]; a1_differ} |-> {b1_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+--	b2_nonasync_1: assert {all_inputs_equal[*1 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+	b2_nonasync_2: assert {all_inputs_equal[+]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_3: assert {all_inputs_equal[*2 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_4: assert {all_inputs_equal[*0 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_5: assert {all_inputs_equal[*]; a2_differ} |-> {b2_equal};
+
+
+	--cover_tester: cover {all_inputs_equal[*21]; a2_differ; all_inputs_equal[*5]};
+end;
diff --git a/testsuite/ghdl-issues/issue2392/tb_dut.vhdl b/testsuite/ghdl-issues/issue2392/tb_dut.vhdl
new file mode 100644
index 0000000..2a72d8d
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/tb_dut.vhdl
@@ -0,0 +1,97 @@
+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
+	signal all_inputs_equal: std_logic;
+	signal a1_differ: std_logic;
+	signal a2_differ: std_logic;
+
+	signal b1_equal: std_logic;
+	signal b2_equal: std_logic;
+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
+		);
+
+	-- Formal part =>
+
+	process(all)
+	begin
+		all_inputs_equal <= '1';
+		if dut1_a1_in /= dut2_a1_in or dut1_a2_in /= dut2_a2_in then
+			all_inputs_equal <= '0';
+		end if;
+
+		a1_differ <= '0';
+		if dut1_a1_in /= dut2_a1_in then
+			a1_differ <= '1';
+		end if;
+
+		a2_differ <= '0';
+		if dut1_a2_in /= dut2_a2_in then
+			a2_differ <= '1';
+		end if;
+
+		b1_equal <= '0';
+		if dut1_b1_out = dut2_b1_out then
+			b1_equal <= '1';
+		end if;
+
+		b2_equal <= '0';
+		if dut1_b2_out = dut2_b2_out then
+			b2_equal <= '1';
+		end if;
+	end process;
+
+	default clock is rising_edge(clk_in);
+
+	b1_nonasync: assert {all_inputs_equal[*1 to inf]; a1_differ} |-> {b1_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+	b2_nonasync_1: assert {all_inputs_equal[*1 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This _should_ generate an assert at cycle 20:
+	b2_nonasync_2: assert {all_inputs_equal[+]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_3: assert {all_inputs_equal[*2 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_4: assert {all_inputs_equal[*0 to inf]; a2_differ} |-> {b2_equal};
+
+	-- This generates an assert at cycle 20:
+	-- b2_nonasync_5: assert {all_inputs_equal[*]; a2_differ} |-> {b2_equal};
+
+
+	--cover_tester: cover {all_inputs_equal[*21]; a2_differ; all_inputs_equal[*5]};
+end;
diff --git a/testsuite/ghdl-issues/issue2392/testsuite.sh b/testsuite/ghdl-issues/issue2392/testsuite.sh
new file mode 100755
index 0000000..f1ba401
--- /dev/null
+++ b/testsuite/ghdl-issues/issue2392/testsuite.sh
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+topdir=../..
+. $topdir/testenv.sh
+
+run_symbiyosys -fd work  async_test-0.sby prove
+
+run_symbiyosys -fd work  async_test-1.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-2.sby prove || true
+if ! grep -q "BMC failed" work/engine_0/logfile.txt; then
+    echo "failure expected"
+    exit 1
+fi
+
+clean
+echo OK