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

1 files changed, 92 insertions, 0 deletions

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;