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

4 files changed, 62 insertions, 0 deletions

diff --git a/testsuite/issues/issue4/counter8.vhdl b/testsuite/issues/issue4/counter8.vhdl
new file mode 100644
index 0000000..2067e23
--- /dev/null
+++ b/testsuite/issues/issue4/counter8.vhdl
@@ -0,0 +1,23 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity counter8 is
+  port (clk : in std_logic;
+        led0 : out std_logic);
+end counter8;
+
+architecture synth of counter8 is
+  
+begin
+
+  process (clk)
+    variable temp : unsigned (7 downto 0);
+  begin
+    if rising_edge(clk) then
+      temp:= temp + 1;
+      led0 <= temp(0);
+    end if;
+  end process;
+
+end synth;
diff --git a/testsuite/issues/issue4/no_vector.vhdl b/testsuite/issues/issue4/no_vector.vhdl
new file mode 100644
index 0000000..a3c2c46
--- /dev/null
+++ b/testsuite/issues/issue4/no_vector.vhdl
@@ -0,0 +1,16 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity no_vector is
+  port (led0: out std_logic);
+end no_vector;
+
+architecture synth of no_vector is
+
+signal nv : std_logic;
+
+begin
+  nv <= '1';
+  led0 <= nv;
+end synth;
diff --git a/testsuite/issues/issue4/testsuite.sh b/testsuite/issues/issue4/testsuite.sh
new file mode 100755
index 0000000..12c33cc
--- /dev/null
+++ b/testsuite/issues/issue4/testsuite.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+for f in no_vector counter8 vector; do
+  synth "${f}.vhdl -e ${f}"
+done
+
+clean
diff --git a/testsuite/issues/issue4/vector.vhdl b/testsuite/issues/issue4/vector.vhdl
new file mode 100644
index 0000000..de74ea9
--- /dev/null
+++ b/testsuite/issues/issue4/vector.vhdl
@@ -0,0 +1,16 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity vector is
+  port (led0: out std_logic);
+end vector;
+
+architecture synth of vector is
+
+signal v : std_logic_vector(7 downto 0);
+
+begin
+  v <= std_logic_vector'("10101010");
+  led0 <= v(0);
+end synth;