testsuite: Add formal tests (#57)

* Add formal tests for shift operations

* ci: build ghdl/synth:formal and run test suites in it

* add testsuite/formal/testsuite.sh

* create testsuite/issues

* ci: remove a level of grouping

* testenv: fix SYMBIYOSYS

* refactor

* testsuite/formal/shifts: Add check for shifts > vector length

24 files changed, 337 insertions, 20 deletions

diff --git a/testsuite/formal/shifts/test_asr.sby b/testsuite/formal/shifts/test_asr.sby
new file mode 100644
index 0000000..bfc39e9
--- /dev/null
+++ b/testsuite/formal/shifts/test_asr.sby
@@ -0,0 +1,13 @@
+[options]
+depth 20
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_asr.vhd -e test_asr
+prep -top test_asr
+
+[files]
+test_asr.vhd
diff --git a/testsuite/formal/shifts/test_asr.vhd b/testsuite/formal/shifts/test_asr.vhd
new file mode 100644
index 0000000..dac8cd2
--- /dev/null
+++ b/testsuite/formal/shifts/test_asr.vhd
@@ -0,0 +1,79 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+entity test_asr is
+  port (
+    -- globals
+    reset : in  std_logic;
+    clk   : in  std_logic;
+    -- inputs
+    sig   : in  signed(7 downto 0);
+    -- outputs
+    asr   : out signed(7 downto 0)
+  );
+end entity test_asr;
+
+
+architecture rtl of test_asr is
+
+  signal index : natural;
+
+begin
+
+  process (clk) is
+  begin
+    if rising_edge(clk) then
+      if reset = '1' then
+        index <= 0;
+        asr   <= x"00";
+      else
+        asr <= shift_right(sig, index);
+        if index < natural'high then
+          index <= index + 1;
+        end if;
+      end if;
+    end if;
+  end process;
+
+  Formal : block is
+
+    signal sig_d   : signed(7 downto 0);
+    signal sig_d_7 : signed(7 downto 0);
+
+  begin
+
+    default clock is rising_edge(clk);
+    restrict {reset[*1]; not reset[+]}[*1];
+
+    -- Register inputs
+    -- Workaround for missing prev() PSL function
+    process (clk) is
+    begin
+      if rising_edge(clk) then
+        sig_d <= sig;
+      end if;
+    end process;
+
+    -- helper signal for sign extension
+    sig_d_7 <= (others => sig_d(7));
+
+    assert reset -> next asr = "00000000";
+    -- Workaround for missing IIR_PREDEFINED_IEEE_NUMERIC_STD_EQ_SGN_INT
+    -- Comparing with hex literals like x"00" in PSL code generates an error:
+    -- no declaration for ""
+
+    shift_aright_0 : assert always not reset and index = 0 -> next asr = sig_d;
+    shift_aright_1 : assert always not reset and index = 1 -> next asr = sig_d_7(7) & sig_d(7 downto 1);
+    shift_aright_2 : assert always not reset and index = 2 -> next asr = sig_d_7(7 downto 6) & sig_d(7 downto 2);
+    shift_aright_3 : assert always not reset and index = 3 -> next asr = sig_d_7(7 downto 5) & sig_d(7 downto 3);
+    shift_aright_4 : assert always not reset and index = 4 -> next asr = sig_d_7(7 downto 4) & sig_d(7 downto 4);
+    shift_aright_5 : assert always not reset and index = 5 -> next asr = sig_d_7(7 downto 3) & sig_d(7 downto 5);
+    shift_aright_6 : assert always not reset and index = 6 -> next asr = sig_d_7(7 downto 2) & sig_d(7 downto 6);
+    shift_aright_7 : assert always not reset and index = 7 -> next asr = sig_d_7(7 downto 1) & sig_d(7);
+    shift_aright_8 : assert always not reset and index >= 8 -> next asr = sig_d_7;
+
+  end block Formal;
+
+end architecture rtl;
diff --git a/testsuite/formal/shifts/test_lsl.sby b/testsuite/formal/shifts/test_lsl.sby
new file mode 100644
index 0000000..280c16c
--- /dev/null
+++ b/testsuite/formal/shifts/test_lsl.sby
@@ -0,0 +1,13 @@
+[options]
+depth 20
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_lsl.vhd -e test_lsl
+prep -top test_lsl
+
+[files]
+test_lsl.vhd
diff --git a/testsuite/formal/shifts/test_lsl.vhd b/testsuite/formal/shifts/test_lsl.vhd
new file mode 100644
index 0000000..737f03b
--- /dev/null
+++ b/testsuite/formal/shifts/test_lsl.vhd
@@ -0,0 +1,92 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+entity test_lsl is
+  port (
+    -- globals
+    reset : in  std_logic;
+    clk   : in  std_logic;
+    -- inputs
+    unsig : in  unsigned(7 downto 0);
+    sig   : in  signed(7 downto 0);
+    -- outputs
+    lslu   : out unsigned(7 downto 0);
+    lsls   : out signed(7 downto 0)
+  );
+end entity test_lsl;
+
+
+architecture rtl of test_lsl is
+
+  signal index : natural;
+
+begin
+
+  process (clk) is
+  begin
+    if rising_edge(clk) then
+      if reset = '1' then
+        index <= 0;
+        lslu  <= x"00";
+        lsls  <= x"00";
+      else
+        lslu <= shift_left(unsig, index);
+        lsls <= shift_left(sig, index);
+        if index < natural'high then
+          index <= index + 1;
+        end if;
+      end if;
+    end if;
+  end process;
+
+  Formal : block is
+
+    signal uns_d : unsigned(7 downto 0);
+    signal sig_d : signed(7 downto 0);
+
+  begin
+
+    default clock is rising_edge(clk);
+    restrict {reset[*1]; not reset[+]}[*1];
+
+    -- Register inputs
+    -- Workaround for missing prev() PSL function
+    process (clk) is
+    begin
+      if rising_edge(clk) then
+        uns_d <= unsig;
+        sig_d <= sig;
+      end if;
+    end process;
+
+    assert reset -> next lslu = 0;
+    assert reset -> next lsls = "00000000";
+    -- Workaround for missing IIR_PREDEFINED_IEEE_NUMERIC_STD_EQ_SGN_INT
+    -- Comparing with hex literals like x"00" in PSL code generates an error:
+    -- no declaration for ""
+
+    shift_left_uns_0 : assert always not reset and index = 0 -> next lslu = uns_d;
+    shift_left_uns_1 : assert always not reset and index = 1 -> next lslu = uns_d(6 downto 0) & '0';
+    shift_left_uns_2 : assert always not reset and index = 2 -> next lslu = uns_d(5 downto 0) & "00";
+    shift_left_uns_3 : assert always not reset and index = 3 -> next lslu = uns_d(4 downto 0) & "000";
+    shift_left_uns_4 : assert always not reset and index = 4 -> next lslu = uns_d(3 downto 0) & "0000";
+    shift_left_uns_5 : assert always not reset and index = 5 -> next lslu = uns_d(2 downto 0) & "00000";
+    shift_left_uns_6 : assert always not reset and index = 6 -> next lslu = uns_d(1 downto 0) & "000000";
+    shift_left_uns_7 : assert always not reset and index = 7 -> next lslu = uns_d(0) & "0000000";
+    shift_left_uns_8 : assert always not reset and index >= 8 -> next lslu = 0;
+
+    shift_left_sgn_0 : assert always not reset and index = 0 -> next lsls = sig_d;
+    shift_left_sgn_1 : assert always not reset and index = 1 -> next lsls = sig_d(6 downto 0) & '0';
+    shift_left_sgn_2 : assert always not reset and index = 2 -> next lsls = sig_d(5 downto 0) & "00";
+    shift_left_sgn_3 : assert always not reset and index = 3 -> next lsls = sig_d(4 downto 0) & "000";
+    shift_left_sgn_4 : assert always not reset and index = 4 -> next lsls = sig_d(3 downto 0) & "0000";
+    shift_left_sgn_5 : assert always not reset and index = 5 -> next lsls = sig_d(2 downto 0) & "00000";
+    shift_left_sgn_6 : assert always not reset and index = 6 -> next lsls = sig_d(1 downto 0) & "000000";
+    shift_left_sgn_7 : assert always not reset and index = 7 -> next lsls = sig_d(0) & "0000000";
+    shift_left_sgn_8 : assert always not reset and index >= 8 -> next lsls = "00000000";
+
+  end block Formal;
+
+end architecture rtl;
diff --git a/testsuite/formal/shifts/test_lsr.sby b/testsuite/formal/shifts/test_lsr.sby
new file mode 100644
index 0000000..aacce69
--- /dev/null
+++ b/testsuite/formal/shifts/test_lsr.sby
@@ -0,0 +1,13 @@
+[options]
+depth 20
+mode prove
+
+[engines]
+smtbmc z3
+
+[script]
+ghdl --std=08 test_lsr.vhd -e test_lsr
+prep -top test_lsr
+
+[files]
+test_lsr.vhd
diff --git a/testsuite/formal/shifts/test_lsr.vhd b/testsuite/formal/shifts/test_lsr.vhd
new file mode 100644
index 0000000..60ac66d
--- /dev/null
+++ b/testsuite/formal/shifts/test_lsr.vhd
@@ -0,0 +1,75 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+entity test_lsr is
+  port (
+    -- globals
+    reset : in  std_logic;
+    clk   : in  std_logic;
+    -- inputs
+    unsig : in  unsigned(7 downto 0);
+    -- outputs
+    lsr   : out unsigned(7 downto 0)
+  );
+end entity test_lsr;
+
+
+architecture rtl of test_lsr is
+
+  signal index : natural;
+
+begin
+
+  process (clk) is
+  begin
+    if rising_edge(clk) then
+      if reset = '1' then
+        index <= 0;
+        lsr  <= x"00";
+      else
+        lsr <= shift_right(unsig, index);
+        if index < natural'high then
+          index <= index + 1;
+        end if;
+      end if;
+    end if;
+  end process;
+
+  Formal : block is
+
+    signal uns_d : unsigned(7 downto 0);
+
+  begin
+
+    default clock is rising_edge(clk);
+    restrict {reset[*1]; not reset[+]}[*1];
+
+    -- Register inputs
+    -- Workaround for missing prev() PSL function
+    process (clk) is
+    begin
+      if rising_edge(clk) then
+        uns_d <= unsig;
+      end if;
+    end process;
+
+    assert reset -> next lsr = 0;
+    -- Workaround for missing IIR_PREDEFINED_IEEE_NUMERIC_STD_EQ_SGN_INT
+    -- Comparing with hex literals like x"00" in PSL code generates an error:
+    -- no declaration for ""
+
+    shift_right_0 : assert always not reset and index = 0 -> next lsr = uns_d;
+    shift_right_1 : assert always not reset and index = 1 -> next lsr = '0' & uns_d(7 downto 1);
+    shift_right_2 : assert always not reset and index = 2 -> next lsr = "00" & uns_d(7 downto 2);
+    shift_right_3 : assert always not reset and index = 3 -> next lsr = "000" & uns_d(7 downto 3);
+    shift_right_4 : assert always not reset and index = 4 -> next lsr = "0000" & uns_d(7 downto 4);
+    shift_right_5 : assert always not reset and index = 5 -> next lsr = "00000" & uns_d(7 downto 5);
+    shift_right_6 : assert always not reset and index = 6 -> next lsr = "000000" & uns_d(7 downto 6);
+    shift_right_7 : assert always not reset and index = 7 -> next lsr = "0000000" & uns_d(7);
+    shift_right_8 : assert always not reset and index >= 8 -> next lsr = 0;
+
+  end block Formal;
+
+end architecture rtl;
diff --git a/testsuite/formal/shifts/testsuite.sh b/testsuite/formal/shifts/testsuite.sh
new file mode 100755
index 0000000..38eb376
--- /dev/null
+++ b/testsuite/formal/shifts/testsuite.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+for f in lsl lsr asr; do
+  formal "test_${f}"
+done
+
+clean
diff --git a/testsuite/issue11/test_nand.vhdl b/testsuite/issues/issue11/test_nand.vhdl
index ae60966..ae60966 100644
--- a/testsuite/issue11/test_nand.vhdl
+++ b/testsuite/issues/issue11/test_nand.vhdl
diff --git a/testsuite/issue11/test_nor.vhdl b/testsuite/issues/issue11/test_nor.vhdl
index f5f911e..f5f911e 100644
--- a/testsuite/issue11/test_nor.vhdl
+++ b/testsuite/issues/issue11/test_nor.vhdl
diff --git a/testsuite/issue11/test_or.vhdl b/testsuite/issues/issue11/test_or.vhdl
index d39d064..d39d064 100644
--- a/testsuite/issue11/test_or.vhdl
+++ b/testsuite/issues/issue11/test_or.vhdl
diff --git a/testsuite/issue11/test_xnor.vhdl b/testsuite/issues/issue11/test_xnor.vhdl
index 4a706f0..4a706f0 100644
--- a/testsuite/issue11/test_xnor.vhdl
+++ b/testsuite/issues/issue11/test_xnor.vhdl
diff --git a/testsuite/issue11/test_xor.vhdl b/testsuite/issues/issue11/test_xor.vhdl
index b856745..b856745 100644
--- a/testsuite/issue11/test_xor.vhdl
+++ b/testsuite/issues/issue11/test_xor.vhdl
diff --git a/testsuite/issue11/testsuite.sh b/testsuite/issues/issue11/testsuite.sh
index e281ee9..7aecfc9 100755
--- a/testsuite/issue11/testsuite.sh
+++ b/testsuite/issues/issue11/testsuite.sh
@@ -1,7 +1,5 @@
 #!/bin/sh
 
-. ../testenv.sh
-
 for f in or xor nor nand xnor; do
   synth "test_${f}.vhdl -e test_${f}"
 done
diff --git a/testsuite/issue4/counter8.vhdl b/testsuite/issues/issue4/counter8.vhdl
index 2067e23..2067e23 100644
--- a/testsuite/issue4/counter8.vhdl
+++ b/testsuite/issues/issue4/counter8.vhdl
diff --git a/testsuite/issue4/no_vector.vhdl b/testsuite/issues/issue4/no_vector.vhdl
index a3c2c46..a3c2c46 100644
--- a/testsuite/issue4/no_vector.vhdl
+++ b/testsuite/issues/issue4/no_vector.vhdl
diff --git a/testsuite/issue4/testsuite.sh b/testsuite/issues/issue4/testsuite.sh
index 49ead4d..12c33cc 100755
--- a/testsuite/issue4/testsuite.sh
+++ b/testsuite/issues/issue4/testsuite.sh
@@ -1,7 +1,5 @@
 #!/bin/sh
 
-. ../testenv.sh
-
 for f in no_vector counter8 vector; do
   synth "${f}.vhdl -e ${f}"
 done
diff --git a/testsuite/issue4/vector.vhdl b/testsuite/issues/issue4/vector.vhdl
index de74ea9..de74ea9 100644
--- a/testsuite/issue4/vector.vhdl
+++ b/testsuite/issues/issue4/vector.vhdl
diff --git a/testsuite/issue6/testsuite.sh b/testsuite/issues/issue6/testsuite.sh
index c1b6e25..4d4b9ca 100755
--- a/testsuite/issue6/testsuite.sh
+++ b/testsuite/issues/issue6/testsuite.sh
@@ -1,7 +1,5 @@
 #!/bin/sh
 
-. ../testenv.sh
-
 synth 'vector.vhdl -e vector'
 
 clean
diff --git a/testsuite/issue6/vector.vhdl b/testsuite/issues/issue6/vector.vhdl
index 255c0b5..255c0b5 100644
--- a/testsuite/issue6/vector.vhdl
+++ b/testsuite/issues/issue6/vector.vhdl
diff --git a/testsuite/issue7/ref.vhdl b/testsuite/issues/issue7/ref.vhdl
index 63dc225..63dc225 100644
--- a/testsuite/issue7/ref.vhdl
+++ b/testsuite/issues/issue7/ref.vhdl
diff --git a/testsuite/issue7/testsuite.sh b/testsuite/issues/issue7/testsuite.sh
index bdafcca..76cf299 100755
--- a/testsuite/issue7/testsuite.sh
+++ b/testsuite/issues/issue7/testsuite.sh
@@ -1,7 +1,5 @@
 #!/bin/sh
 
-. ../testenv.sh
-
 run_yosys -Q -q -p "ghdl ref.vhdl -e vector ref; write_verilog ref.v"
 run_yosys -Q -q -p "ghdl ref.vhdl vector.vhdl -e vector synth; write_verilog vector.v"
 
diff --git a/testsuite/issue7/vector.vhdl b/testsuite/issues/issue7/vector.vhdl
index 3ab2e24..3ab2e24 100644
--- a/testsuite/issue7/vector.vhdl
+++ b/testsuite/issues/issue7/vector.vhdl
diff --git a/testsuite/testenv.sh b/testsuite/testenv.sh
index 23c67e0..b736b91 100644
--- a/testsuite/testenv.sh
+++ b/testsuite/testenv.sh
@@ -12,6 +12,10 @@ if [ x"$YOSYS" = x ]; then
     YOSYS="yosys -m ../../ghdl.so"
 fi
 
+if [ x"$SYMBIYOSYS" = x ]; then
+    SYMBIYOSYS="sby"
+fi
+
 cmd ()
 {
     echo "· $@"
@@ -23,6 +27,11 @@ run_yosys ()
     cmd $YOSYS "$@"
 }
 
+run_symbiyosys ()
+{
+    cmd $SYMBIYOSYS --yosys "$YOSYS" "$@"
+}
+
 analyze ()
 {
     printf "${ANSI_BLUE}Analyze $@ $ANSI_NOCOLOR\n"
@@ -36,10 +45,15 @@ synth ()
     travis_finish "synth"
 }
 
+formal ()
+{
+    travis_start "formal" "Verify $@"
+    run_symbiyosys -f -d work $@.sby
+    travis_finish "formal"
+}
+
 clean ()
 {
-    travis_start "rm" "Remove work library"
     "$GHDL" --remove $GHDL_STD_FLAGS
     rm -f out.blif
-    travis_finish "rm"
 }
diff --git a/testsuite/testsuite.sh b/testsuite/testsuite.sh
index 943c66e..f4f938d 100755
--- a/testsuite/testsuite.sh
+++ b/testsuite/testsuite.sh
@@ -1,24 +1,43 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 cd "$(dirname $0)"
 . ../utils.sh
 
+run_suite () {
+  . ../testenv.sh
+  for d in */; do
+      if [ -f $d/testsuite.sh ]; then
+          printf "${ANSI_DARKCYAN}test $d ${ANSI_NOCOLOR}\n"
+          cd $d
+          if . ./testsuite.sh; then
+              printf "${ANSI_GREEN}OK${ANSI_NOCOLOR}\n"
+          else
+              printf "${ANSI_RED}FAILED!${ANSI_NOCOLOR}\n"
+              exit 1
+          fi
+          cd ..
+      else
+          printf "${ANSI_YELLOW}Skip $d (no testsuite.sh)${ANSI_NOCOLOR}\n"
+      fi
+      clean
+  done
+}
+
 for d in */; do
-    if [ -f $d/testsuite.sh ]; then
-        travis_start "test" "$d" "$ANSI_CYAN"
-        cd $d
+    cd $d
+    printf "${ANSI_CYAN}test $d ${ANSI_NOCOLOR}\n"
+    if [ -f ./testsuite.sh ]; then
         if ./testsuite.sh; then
-            printf "${ANSI_GREEN}OK$ANSI_NOCOLOR\n"
+            printf "${ANSI_GREEN}OK${ANSI_NOCOLOR}\n"
         else
-            printf "${ANSI_RED}FAILED!$ANSI_NOCOLOR\n"
+            printf "${ANSI_RED}FAILED!${ANSI_NOCOLOR}\n"
             exit 1
         fi
-        cd ..
-        travis_finish "test"
     else
-        printf "${ANSI_YELLOW}Skip $d (no testsuite.sh)$ANSI_NOCOLOR\n"
+        run_suite
     fi
+    cd ..
 done
 
-printf "${ANSI_GREEN}All tests are OK$ANSI_NOCOLOR\n"
+printf "${ANSI_GREEN}All tests are OK${ANSI_NOCOLOR}\n"
 exit 0