From b405a27654f326eb1117c0eda8e7389a64fc5c94 Mon Sep 17 00:00:00 2001
From: "T. Meissner" <programming@goodcleanfun.de>
Date: Mon, 7 Oct 2019 19:13:46 +0200
Subject: 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
---
 testsuite/formal/shifts/test_asr.sby    | 13 +++++
 testsuite/formal/shifts/test_asr.vhd    | 79 ++++++++++++++++++++++++++++
 testsuite/formal/shifts/test_lsl.sby    | 13 +++++
 testsuite/formal/shifts/test_lsl.vhd    | 92 +++++++++++++++++++++++++++++++++
 testsuite/formal/shifts/test_lsr.sby    | 13 +++++
 testsuite/formal/shifts/test_lsr.vhd    | 75 +++++++++++++++++++++++++++
 testsuite/formal/shifts/testsuite.sh    |  7 +++
 testsuite/issue11/test_nand.vhdl        | 14 -----
 testsuite/issue11/test_nor.vhdl         | 14 -----
 testsuite/issue11/test_or.vhdl          | 14 -----
 testsuite/issue11/test_xnor.vhdl        | 14 -----
 testsuite/issue11/test_xor.vhdl         | 14 -----
 testsuite/issue11/testsuite.sh          |  9 ----
 testsuite/issue4/counter8.vhdl          | 23 ---------
 testsuite/issue4/no_vector.vhdl         | 16 ------
 testsuite/issue4/testsuite.sh           |  9 ----
 testsuite/issue4/vector.vhdl            | 16 ------
 testsuite/issue6/testsuite.sh           |  7 ---
 testsuite/issue6/vector.vhdl            | 16 ------
 testsuite/issue7/ref.vhdl               | 13 -----
 testsuite/issue7/testsuite.sh           | 20 -------
 testsuite/issue7/vector.vhdl            | 29 -----------
 testsuite/issues/issue11/test_nand.vhdl | 14 +++++
 testsuite/issues/issue11/test_nor.vhdl  | 14 +++++
 testsuite/issues/issue11/test_or.vhdl   | 14 +++++
 testsuite/issues/issue11/test_xnor.vhdl | 14 +++++
 testsuite/issues/issue11/test_xor.vhdl  | 14 +++++
 testsuite/issues/issue11/testsuite.sh   |  7 +++
 testsuite/issues/issue4/counter8.vhdl   | 23 +++++++++
 testsuite/issues/issue4/no_vector.vhdl  | 16 ++++++
 testsuite/issues/issue4/testsuite.sh    |  7 +++
 testsuite/issues/issue4/vector.vhdl     | 16 ++++++
 testsuite/issues/issue6/testsuite.sh    |  5 ++
 testsuite/issues/issue6/vector.vhdl     | 16 ++++++
 testsuite/issues/issue7/ref.vhdl        | 13 +++++
 testsuite/issues/issue7/testsuite.sh    | 18 +++++++
 testsuite/issues/issue7/vector.vhdl     | 29 +++++++++++
 testsuite/testenv.sh                    | 18 ++++++-
 testsuite/testsuite.sh                  | 39 ++++++++++----
 39 files changed, 557 insertions(+), 240 deletions(-)
 create mode 100644 testsuite/formal/shifts/test_asr.sby
 create mode 100644 testsuite/formal/shifts/test_asr.vhd
 create mode 100644 testsuite/formal/shifts/test_lsl.sby
 create mode 100644 testsuite/formal/shifts/test_lsl.vhd
 create mode 100644 testsuite/formal/shifts/test_lsr.sby
 create mode 100644 testsuite/formal/shifts/test_lsr.vhd
 create mode 100755 testsuite/formal/shifts/testsuite.sh
 delete mode 100644 testsuite/issue11/test_nand.vhdl
 delete mode 100644 testsuite/issue11/test_nor.vhdl
 delete mode 100644 testsuite/issue11/test_or.vhdl
 delete mode 100644 testsuite/issue11/test_xnor.vhdl
 delete mode 100644 testsuite/issue11/test_xor.vhdl
 delete mode 100755 testsuite/issue11/testsuite.sh
 delete mode 100644 testsuite/issue4/counter8.vhdl
 delete mode 100644 testsuite/issue4/no_vector.vhdl
 delete mode 100755 testsuite/issue4/testsuite.sh
 delete mode 100644 testsuite/issue4/vector.vhdl
 delete mode 100755 testsuite/issue6/testsuite.sh
 delete mode 100644 testsuite/issue6/vector.vhdl
 delete mode 100644 testsuite/issue7/ref.vhdl
 delete mode 100755 testsuite/issue7/testsuite.sh
 delete mode 100644 testsuite/issue7/vector.vhdl
 create mode 100644 testsuite/issues/issue11/test_nand.vhdl
 create mode 100644 testsuite/issues/issue11/test_nor.vhdl
 create mode 100644 testsuite/issues/issue11/test_or.vhdl
 create mode 100644 testsuite/issues/issue11/test_xnor.vhdl
 create mode 100644 testsuite/issues/issue11/test_xor.vhdl
 create mode 100755 testsuite/issues/issue11/testsuite.sh
 create mode 100644 testsuite/issues/issue4/counter8.vhdl
 create mode 100644 testsuite/issues/issue4/no_vector.vhdl
 create mode 100755 testsuite/issues/issue4/testsuite.sh
 create mode 100644 testsuite/issues/issue4/vector.vhdl
 create mode 100755 testsuite/issues/issue6/testsuite.sh
 create mode 100644 testsuite/issues/issue6/vector.vhdl
 create mode 100644 testsuite/issues/issue7/ref.vhdl
 create mode 100755 testsuite/issues/issue7/testsuite.sh
 create mode 100644 testsuite/issues/issue7/vector.vhdl

(limited to 'testsuite')

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/issue11/test_nand.vhdl
deleted file mode 100644
index ae60966..0000000
--- a/testsuite/issue11/test_nand.vhdl
+++ /dev/null
@@ -1,14 +0,0 @@
-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/issue11/test_nor.vhdl b/testsuite/issue11/test_nor.vhdl
deleted file mode 100644
index f5f911e..0000000
--- a/testsuite/issue11/test_nor.vhdl
+++ /dev/null
@@ -1,14 +0,0 @@
-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/issue11/test_or.vhdl b/testsuite/issue11/test_or.vhdl
deleted file mode 100644
index d39d064..0000000
--- a/testsuite/issue11/test_or.vhdl
+++ /dev/null
@@ -1,14 +0,0 @@
-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/issue11/test_xnor.vhdl b/testsuite/issue11/test_xnor.vhdl
deleted file mode 100644
index 4a706f0..0000000
--- a/testsuite/issue11/test_xnor.vhdl
+++ /dev/null
@@ -1,14 +0,0 @@
-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/issue11/test_xor.vhdl b/testsuite/issue11/test_xor.vhdl
deleted file mode 100644
index b856745..0000000
--- a/testsuite/issue11/test_xor.vhdl
+++ /dev/null
@@ -1,14 +0,0 @@
-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/issue11/testsuite.sh b/testsuite/issue11/testsuite.sh
deleted file mode 100755
index e281ee9..0000000
--- a/testsuite/issue11/testsuite.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-. ../testenv.sh
-
-for f in or xor nor nand xnor; do
-  synth "test_${f}.vhdl -e test_${f}"
-done
-
-clean
diff --git a/testsuite/issue4/counter8.vhdl b/testsuite/issue4/counter8.vhdl
deleted file mode 100644
index 2067e23..0000000
--- a/testsuite/issue4/counter8.vhdl
+++ /dev/null
@@ -1,23 +0,0 @@
-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/issue4/no_vector.vhdl b/testsuite/issue4/no_vector.vhdl
deleted file mode 100644
index a3c2c46..0000000
--- a/testsuite/issue4/no_vector.vhdl
+++ /dev/null
@@ -1,16 +0,0 @@
-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/issue4/testsuite.sh b/testsuite/issue4/testsuite.sh
deleted file mode 100755
index 49ead4d..0000000
--- a/testsuite/issue4/testsuite.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-. ../testenv.sh
-
-for f in no_vector counter8 vector; do
-  synth "${f}.vhdl -e ${f}"
-done
-
-clean
diff --git a/testsuite/issue4/vector.vhdl b/testsuite/issue4/vector.vhdl
deleted file mode 100644
index de74ea9..0000000
--- a/testsuite/issue4/vector.vhdl
+++ /dev/null
@@ -1,16 +0,0 @@
-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/issue6/testsuite.sh b/testsuite/issue6/testsuite.sh
deleted file mode 100755
index c1b6e25..0000000
--- a/testsuite/issue6/testsuite.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-
-. ../testenv.sh
-
-synth 'vector.vhdl -e vector'
-
-clean
diff --git a/testsuite/issue6/vector.vhdl b/testsuite/issue6/vector.vhdl
deleted file mode 100644
index 255c0b5..0000000
--- a/testsuite/issue6/vector.vhdl
+++ /dev/null
@@ -1,16 +0,0 @@
-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/issue7/ref.vhdl b/testsuite/issue7/ref.vhdl
deleted file mode 100644
index 63dc225..0000000
--- a/testsuite/issue7/ref.vhdl
+++ /dev/null
@@ -1,13 +0,0 @@
-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/issue7/testsuite.sh b/testsuite/issue7/testsuite.sh
deleted file mode 100755
index bdafcca..0000000
--- a/testsuite/issue7/testsuite.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/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"
-
-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/issue7/vector.vhdl b/testsuite/issue7/vector.vhdl
deleted file mode 100644
index 3ab2e24..0000000
--- a/testsuite/issue7/vector.vhdl
+++ /dev/null
@@ -1,29 +0,0 @@
-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;
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;
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
-- 
cgit v1.2.3