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, 79 insertions, 0 deletions

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;