ghdl-issue: add a testcase for ghdl/ghdl#2672

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

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;

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

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;

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;

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;

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

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;

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