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

15 files changed, 220 insertions, 0 deletions

diff --git a/testsuite/issues/issue11/test_nand.vhdl b/testsuite/issues/issue11/test_nand.vhdl
new file mode 100644
index 0000000..ae60966
--- /dev/null
+++ b/testsuite/issues/issue11/test_nand.vhdl
@@ -0,0 +1,14 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity test_nand is port (
+    sel0, sel1: in std_logic;
+    c: out std_logic);
+end test_nand;
+
+architecture synth of test_nand is
+begin
+
+    c <= sel1 nand sel0;
+
+end synth;
diff --git a/testsuite/issues/issue11/test_nor.vhdl b/testsuite/issues/issue11/test_nor.vhdl
new file mode 100644
index 0000000..f5f911e
--- /dev/null
+++ b/testsuite/issues/issue11/test_nor.vhdl
@@ -0,0 +1,14 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity test_nor is port (
+    sel0, sel1: in std_logic;
+    c: out std_logic);
+end test_nor;
+
+architecture synth of test_nor is
+begin
+
+    c <= sel1 nor sel0;
+
+end synth;
diff --git a/testsuite/issues/issue11/test_or.vhdl b/testsuite/issues/issue11/test_or.vhdl
new file mode 100644
index 0000000..d39d064
--- /dev/null
+++ b/testsuite/issues/issue11/test_or.vhdl
@@ -0,0 +1,14 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity test_or is port (
+    sel0, sel1: in std_logic;
+    c: out std_logic);
+end test_or;
+
+architecture synth of test_or is
+begin
+
+    c <= sel1 or sel0;
+
+end synth;
diff --git a/testsuite/issues/issue11/test_xnor.vhdl b/testsuite/issues/issue11/test_xnor.vhdl
new file mode 100644
index 0000000..4a706f0
--- /dev/null
+++ b/testsuite/issues/issue11/test_xnor.vhdl
@@ -0,0 +1,14 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity test_xnor is port (
+    sel0, sel1: in std_logic;
+    c: out std_logic);
+end test_xnor;
+
+architecture synth of test_xnor is
+begin
+
+    c <= sel1 xnor sel0;
+
+end synth;
diff --git a/testsuite/issues/issue11/test_xor.vhdl b/testsuite/issues/issue11/test_xor.vhdl
new file mode 100644
index 0000000..b856745
--- /dev/null
+++ b/testsuite/issues/issue11/test_xor.vhdl
@@ -0,0 +1,14 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity test_xor is port (
+    sel0, sel1: in std_logic;
+    c: out std_logic);
+end test_xor;
+
+architecture synth of test_xor is
+begin
+
+    c <= sel1 xor sel0;
+
+end synth;
diff --git a/testsuite/issues/issue11/testsuite.sh b/testsuite/issues/issue11/testsuite.sh
new file mode 100755
index 0000000..7aecfc9
--- /dev/null
+++ b/testsuite/issues/issue11/testsuite.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+for f in or xor nor nand xnor; do
+  synth "test_${f}.vhdl -e test_${f}"
+done
+
+clean
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;
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;
diff --git a/testsuite/issues/issue7/ref.vhdl b/testsuite/issues/issue7/ref.vhdl
new file mode 100644
index 0000000..63dc225
--- /dev/null
+++ b/testsuite/issues/issue7/ref.vhdl
@@ -0,0 +1,13 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity vector is
+  port (led0, led1, led2, led3, led4, led5, led6, led7: out std_logic);
+end vector;
+
+architecture ref of vector is
+  signal v : std_logic_vector(7 downto 0);
+begin
+  -- It works ok
+  (led7, led6, led5, led4, led3, led2, led1, led0) <= std_logic_vector'("10101010");
+end;
diff --git a/testsuite/issues/issue7/testsuite.sh b/testsuite/issues/issue7/testsuite.sh
new file mode 100755
index 0000000..76cf299
--- /dev/null
+++ b/testsuite/issues/issue7/testsuite.sh
@@ -0,0 +1,18 @@
+#!/bin/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"
+
+run_yosys -Q -p '
+ read_verilog ref.v
+ rename vector ref
+
+ read_verilog vector.v
+ equiv_make ref vector equiv
+
+ hierarchy -top equiv
+ equiv_simple
+ equiv_status -assert'
+
+clean
+rm -f *.v
diff --git a/testsuite/issues/issue7/vector.vhdl b/testsuite/issues/issue7/vector.vhdl
new file mode 100644
index 0000000..3ab2e24
--- /dev/null
+++ b/testsuite/issues/issue7/vector.vhdl
@@ -0,0 +1,29 @@
+architecture synth of vector is
+
+signal v : std_logic_vector(7 downto 0);
+
+begin
+
+  -- It works ok
+  --(led7, led6, led5, led4, led3, led2, led1, led0) <= std_logic_vector'("10101010");
+
+  -- It is assigned in reverse order (led7 should be MSB, but it is assigned
+  -- the lsb. led0 should be the lsb, but is assigned as the MSB)
+  v <= std_logic_vector'("10101010");
+  led7 <= v(7);
+  led6 <= v(6);
+  led5 <= v(5);
+  led4 <= v(4);
+  led3 <= v(3);
+  led2 <= v(2);
+  led1 <= v(1);
+  led0 <= v(0);
+
+end synth;
+
+architecture ok of vector is
+  signal v : std_logic_vector(7 downto 0);
+begin
+  -- It works ok
+  (led7, led6, led5, led4, led3, led2, led1, led0) <= std_logic_vector'("10101010");
+end ok;