From 205225940055320bbe26253aca292771b1799cc4 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Thu, 9 Mar 2023 07:28:55 +0100 Subject: testsuite: add a test, close ghdl/ghdl#2373 --- .../ghdl-issues/issue2373/async_test-plus.sby | 23 +++++++++ .../ghdl-issues/issue2373/async_test-star.sby | 23 +++++++++ testsuite/ghdl-issues/issue2373/dut.vhdl | 51 +++++++++++++++++++ testsuite/ghdl-issues/issue2373/tb_dut-plus.vhdl | 57 ++++++++++++++++++++++ testsuite/ghdl-issues/issue2373/tb_dut-star.vhdl | 57 ++++++++++++++++++++++ testsuite/ghdl-issues/issue2373/testsuite.sh | 19 ++++++++ 6 files changed, 230 insertions(+) create mode 100644 testsuite/ghdl-issues/issue2373/async_test-plus.sby create mode 100644 testsuite/ghdl-issues/issue2373/async_test-star.sby create mode 100644 testsuite/ghdl-issues/issue2373/dut.vhdl create mode 100644 testsuite/ghdl-issues/issue2373/tb_dut-plus.vhdl create mode 100644 testsuite/ghdl-issues/issue2373/tb_dut-star.vhdl create mode 100755 testsuite/ghdl-issues/issue2373/testsuite.sh 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 -- cgit v1.2.3