diff --git a/testsuite/ghdl-issues/issue2672/prove_01-orig.sby b/testsuite/ghdl-issues/issue2672/prove_01-orig.sby new file mode 100644 index 0000000..107385c --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01-orig.sby @@ -0,0 +1,24 @@ +[tasks] +bmc +prove_1 +prove_2 + +[options] +bmc: mode bmc +depth 20 +prove_1: mode prove +prove_1: depth 30 +prove_2: mode prove +prove_2: depth 30 + +[engines] +smtbmc boolector +prove_1: smtbmc boolector +prove_2: smtbmc yices + +[script] +ghdl --std=08 prove_01-orig.vhdl -e prove_01 +prep -top prove_01 + +[files] +prove_01-orig.vhdl diff --git a/testsuite/ghdl-issues/issue2672/prove_01-orig.vhdl b/testsuite/ghdl-issues/issue2672/prove_01-orig.vhdl new file mode 100644 index 0000000..8d258f9 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01-orig.vhdl @@ -0,0 +1,46 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity prove_01 is + port( + clk_in: in std_logic; + sreset_in: in std_logic; + + a_in: in std_logic; + + b_out: out std_logic + ); +end; + +architecture rtl of prove_01 is + signal state: unsigned(7 downto 0); +begin + process(clk_in) + begin + if rising_edge(clk_in) then + if a_in = '1' then + state <= (state + 1) mod 32; + end if; + if state = 0 then + b_out <= a_in; + else + b_out <= '0'; + end if; + + if sreset_in = '1' then + state <= (others => '0'); + b_out <= '0'; + end if; + end if; + end process; + + default clock is rising_edge(clk_in); + + a_1: assume {sreset_in[*2]}; + a_2: assume {not sreset_in; sreset_in} |=> {sreset_in}; + a_3: assume always {not a_in; a_in} |=> {a_in}; + a_4: assume always {a_in; not a_in} |=> {not a_in}; + + f_1: assert always {b_out='1'} |=> {b_out='0'[*31]} abort prev(sreset_in); +end; diff --git a/testsuite/ghdl-issues/issue2672/prove_01.sby b/testsuite/ghdl-issues/issue2672/prove_01.sby new file mode 100644 index 0000000..2d05f2e --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01.sby @@ -0,0 +1,24 @@ +[tasks] +bmc +prove_1 +prove_2 + +[options] +bmc: mode bmc +depth 20 +prove_1: mode prove +prove_1: depth 7 +prove_2: mode prove +prove_2: depth 7 + +[engines] +smtbmc boolector +prove_1: smtbmc boolector +prove_2: smtbmc yices + +[script] +ghdl --std=08 prove_01b.vhdl -e prove_01 +prep -top prove_01 + +[files] +prove_01b.vhdl diff --git a/testsuite/ghdl-issues/issue2672/prove_01.vhdl b/testsuite/ghdl-issues/issue2672/prove_01.vhdl new file mode 100644 index 0000000..8d258f9 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01.vhdl @@ -0,0 +1,46 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity prove_01 is + port( + clk_in: in std_logic; + sreset_in: in std_logic; + + a_in: in std_logic; + + b_out: out std_logic + ); +end; + +architecture rtl of prove_01 is + signal state: unsigned(7 downto 0); +begin + process(clk_in) + begin + if rising_edge(clk_in) then + if a_in = '1' then + state <= (state + 1) mod 32; + end if; + if state = 0 then + b_out <= a_in; + else + b_out <= '0'; + end if; + + if sreset_in = '1' then + state <= (others => '0'); + b_out <= '0'; + end if; + end if; + end process; + + default clock is rising_edge(clk_in); + + a_1: assume {sreset_in[*2]}; + a_2: assume {not sreset_in; sreset_in} |=> {sreset_in}; + a_3: assume always {not a_in; a_in} |=> {a_in}; + a_4: assume always {a_in; not a_in} |=> {not a_in}; + + f_1: assert always {b_out='1'} |=> {b_out='0'[*31]} abort prev(sreset_in); +end; diff --git a/testsuite/ghdl-issues/issue2672/prove_01b-orig.vhdl b/testsuite/ghdl-issues/issue2672/prove_01b-orig.vhdl new file mode 100644 index 0000000..bbcb851 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01b-orig.vhdl @@ -0,0 +1,53 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity prove_01 is + port( + clk_in: in std_logic; + sreset_in: in std_logic; + + a_in: in std_logic; + b_out: out std_logic; + c_out: out std_logic + ); +end; + +architecture rtl of prove_01 is + signal state: unsigned(7 downto 0); +begin + process(clk_in) + begin + if rising_edge(clk_in) then + if a_in = '1' then + state <= (state + 1) mod 32; + end if; + if state = 0 then + b_out <= a_in; + else + b_out <= '0'; + end if; + + + if sreset_in = '1' then + state <= (others => '0'); + b_out <= '0'; + end if; + end if; + end process; + + c_out <= a_in; + + default clock is rising_edge(clk_in); + + a_1: assume {sreset_in[*2]}; + a_2: assume {not sreset_in; sreset_in} |=> {sreset_in}; + a_3: assume always {not a_in; a_in} |=> {a_in}; + a_4: assume always {a_in; not a_in} |=> {not a_in}; + + f_test: assert always {not c_out; c_out} |=> c_out; + + f_1: assert always {b_out='1'} |=> {b_out='0'[*31]} abort prev(sreset_in); + + f_2: assert always state <= 31 abort sreset_in; +end; diff --git a/testsuite/ghdl-issues/issue2672/prove_01b.vhdl b/testsuite/ghdl-issues/issue2672/prove_01b.vhdl new file mode 100644 index 0000000..8562439 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/prove_01b.vhdl @@ -0,0 +1,48 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity prove_01 is + port( + clk_in: in std_logic; + sreset_in: in std_logic; + + a_in: in std_logic; + b_out: out std_logic + ); +end; + +architecture rtl of prove_01 is + signal state: unsigned(2 downto 0); +begin + process(clk_in) + begin + if rising_edge(clk_in) then + if a_in = '1' then + state <= (state + 1) mod 32; + end if; + if state = 0 then + b_out <= a_in; + else + b_out <= '0'; + end if; + + + if sreset_in = '1' then + state <= (others => '0'); + b_out <= '0'; + end if; + end if; + end process; + + default clock is rising_edge(clk_in); + + a_1: assume {sreset_in[*2]}; + a_2: assume {not sreset_in; sreset_in} |=> {sreset_in}; + a_3: assume always {not a_in; a_in} |=> {a_in}; + a_4: assume always {a_in; not a_in} |=> {not a_in}; + + f_1: assert always ({b_out='1'} |=> {b_out='0'[*7]}) abort sreset_in; + +-- f_2: assert always state <= 31 abort sreset_in; +end; diff --git a/testsuite/ghdl-issues/issue2672/repro.sby b/testsuite/ghdl-issues/issue2672/repro.sby new file mode 100644 index 0000000..9ab4d86 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/repro.sby @@ -0,0 +1,16 @@ +[tasks] +prove_1 + +[options] +prove_1: mode prove +prove_1: depth 7 + +[engines] +prove_1: smtbmc boolector + +[script] +ghdl --std=08 repro.vhdl -e +prep -top repro + +[files] +repro.vhdl diff --git a/testsuite/ghdl-issues/issue2672/repro.vhdl b/testsuite/ghdl-issues/issue2672/repro.vhdl new file mode 100644 index 0000000..08ad0df --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/repro.vhdl @@ -0,0 +1,42 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity repro is + port ( + clk_in: in std_logic; + sreset_in: in std_logic; + + a_in: in std_logic; + b_out: out std_logic + ); +end; + +architecture rtl of repro is + signal pipe: std_logic_vector(3 downto 0) := (others => '0'); +begin + process(clk_in) + begin + if rising_edge(clk_in) then + if false and sreset_in = '1' then + pipe <= (others => '0'); + b_out <= '0'; + else + b_out <= pipe(3); + pipe <= pipe(2 downto 0) & a_in; + end if; + end if; + end process; + + default clock is rising_edge(clk_in); + +-- a_1: assume {sreset_in[*2]}; + + -- a_in must be stable for 2 cycles.prove_2: mode prove + a_2: restrict {not a_in; [*]}; + a_3: assume always {not a_in; a_in} |=> {a_in}; + + f_1: assert always {b_out='0'; b_out='1'} |=> {b_out='1'}; -- abort sreset_in; + +-- f_2: assert always state <= 31 abort sreset_in; +end; diff --git a/testsuite/ghdl-issues/issue2672/testsuite.sh b/testsuite/ghdl-issues/issue2672/testsuite.sh new file mode 100755 index 0000000..bf8c5a6 --- /dev/null +++ b/testsuite/ghdl-issues/issue2672/testsuite.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +topdir=../.. +. $topdir/testenv.sh + +run_symbiyosys -fd work repro.sby prove_1 +#run_symbiyosys -fd work prove_01-orig.sby prove_1 + +clean +echo OK