1 files changed, 75 insertions, 0 deletions
diff --git a/testsuite/formal/gates/test_lsr.vhd b/testsuite/formal/gates/test_lsr.vhd
new file mode 100644
index 0000000..60ac66d
--- /dev/null
+++ b/testsuite/formal/gates/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;