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

2 files changed, 21 insertions, 0 deletions

diff --git a/testsuite/issues/issue6/testsuite.sh b/testsuite/issues/issue6/testsuite.sh
new file mode 100755
index 0000000..4d4b9ca
--- /dev/null
+++ b/testsuite/issues/issue6/testsuite.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+synth 'vector.vhdl -e vector'
+
+clean
diff --git a/testsuite/issues/issue6/vector.vhdl b/testsuite/issues/issue6/vector.vhdl
new file mode 100644
index 0000000..255c0b5
--- /dev/null
+++ b/testsuite/issues/issue6/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(1); --- But led0 <= v(0) works ok
+end synth;