From 7a71af5845b0789d2a8169336d0e07a4c27beb1d Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Wed, 15 Mar 2023 07:47:24 +0100 Subject: testsuite: add a test for #2392 --- testsuite/ghdl-issues/issue2392/async_test-0.sby | 22 ++++++ testsuite/ghdl-issues/issue2392/async_test-1.sby | 22 ++++++ testsuite/ghdl-issues/issue2392/async_test-2.sby | 22 ++++++ testsuite/ghdl-issues/issue2392/async_test.sby | 22 ++++++ testsuite/ghdl-issues/issue2392/dut.vhdl | 51 +++++++++++++ testsuite/ghdl-issues/issue2392/tb_dut-0.vhdl | 97 ++++++++++++++++++++++++ testsuite/ghdl-issues/issue2392/tb_dut-1.vhdl | 97 ++++++++++++++++++++++++ testsuite/ghdl-issues/issue2392/tb_dut-2.vhdl | 97 ++++++++++++++++++++++++ testsuite/ghdl-issues/issue2392/tb_dut.vhdl | 97 ++++++++++++++++++++++++ testsuite/ghdl-issues/issue2392/testsuite.sh | 21 +++++ 10 files changed, 548 insertions(+) create mode 100644 testsuite/ghdl-issues/issue2392/async_test-0.sby create mode 100644 testsuite/ghdl-issues/issue2392/async_test-1.sby create mode 100644 testsuite/ghdl-issues/issue2392/async_test-2.sby create mode 100644 testsuite/ghdl-issues/issue2392/async_test.sby create mode 100644 testsuite/ghdl-issues/issue2392/dut.vhdl create mode 100644 testsuite/ghdl-issues/issue2392/tb_dut-0.vhdl create mode 100644 testsuite/ghdl-issues/issue2392/tb_dut-1.vhdl create mode 100644 testsuite/ghdl-issues/issue2392/tb_dut-2.vhdl create mode 100644 testsuite/ghdl-issues/issue2392/tb_dut.vhdl create mode 100755 testsuite/ghdl-issues/issue2392/testsuite.sh 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 -- cgit v1.2.3