diff options
Diffstat (limited to 'testsuite/formal')
-rw-r--r-- | testsuite/formal/shifts/test_asr.sby | 13 | ||||
-rw-r--r-- | testsuite/formal/shifts/test_asr.vhd | 79 | ||||
-rw-r--r-- | testsuite/formal/shifts/test_lsl.sby | 13 | ||||
-rw-r--r-- | testsuite/formal/shifts/test_lsl.vhd | 92 | ||||
-rw-r--r-- | testsuite/formal/shifts/test_lsr.sby | 13 | ||||
-rw-r--r-- | testsuite/formal/shifts/test_lsr.vhd | 75 | ||||
-rwxr-xr-x | testsuite/formal/shifts/testsuite.sh | 7 |
7 files changed, 292 insertions, 0 deletions
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 |