From 63bb08a0893209bd0b1f13e9ab5c3e585ed43514 Mon Sep 17 00:00:00 2001 From: Xiretza Date: Sat, 21 Mar 2020 20:48:32 +0100 Subject: Move formal tests for gates into single subdirectory --- testsuite/formal/abs/test_abs.sby | 13 ----- testsuite/formal/abs/test_abs.vhd | 37 --------------- testsuite/formal/abs/testsuite.sh | 9 ---- testsuite/formal/gates/test_abs.sby | 13 +++++ testsuite/formal/gates/test_abs.vhd | 37 +++++++++++++++ testsuite/formal/gates/test_asr.sby | 13 +++++ testsuite/formal/gates/test_asr.vhd | 79 +++++++++++++++++++++++++++++++ testsuite/formal/gates/test_lsl.sby | 13 +++++ testsuite/formal/gates/test_lsl.vhd | 92 ++++++++++++++++++++++++++++++++++++ testsuite/formal/gates/test_lsr.sby | 13 +++++ testsuite/formal/gates/test_lsr.vhd | 75 +++++++++++++++++++++++++++++ testsuite/formal/gates/testsuite.sh | 11 +++++ 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 | 11 ----- 19 files changed, 346 insertions(+), 355 deletions(-) delete mode 100644 testsuite/formal/abs/test_abs.sby delete mode 100644 testsuite/formal/abs/test_abs.vhd delete mode 100755 testsuite/formal/abs/testsuite.sh create mode 100644 testsuite/formal/gates/test_abs.sby create mode 100644 testsuite/formal/gates/test_abs.vhd create mode 100644 testsuite/formal/gates/test_asr.sby create mode 100644 testsuite/formal/gates/test_asr.vhd create mode 100644 testsuite/formal/gates/test_lsl.sby create mode 100644 testsuite/formal/gates/test_lsl.vhd create mode 100644 testsuite/formal/gates/test_lsr.sby create mode 100644 testsuite/formal/gates/test_lsr.vhd create mode 100755 testsuite/formal/gates/testsuite.sh delete mode 100644 testsuite/formal/shifts/test_asr.sby delete mode 100644 testsuite/formal/shifts/test_asr.vhd delete mode 100644 testsuite/formal/shifts/test_lsl.sby delete mode 100644 testsuite/formal/shifts/test_lsl.vhd delete mode 100644 testsuite/formal/shifts/test_lsr.sby delete mode 100644 testsuite/formal/shifts/test_lsr.vhd delete mode 100755 testsuite/formal/shifts/testsuite.sh (limited to 'testsuite') diff --git a/testsuite/formal/abs/test_abs.sby b/testsuite/formal/abs/test_abs.sby deleted file mode 100644 index 0e4bc7c..0000000 --- a/testsuite/formal/abs/test_abs.sby +++ /dev/null @@ -1,13 +0,0 @@ -[options] -#depth 6 -mode prove - -[engines] -smtbmc z3 - -[script] -ghdl --std=08 test_abs.vhd -e ent -prep -top ent - -[files] -test_abs.vhd diff --git a/testsuite/formal/abs/test_abs.vhd b/testsuite/formal/abs/test_abs.vhd deleted file mode 100644 index 3e711b2..0000000 --- a/testsuite/formal/abs/test_abs.vhd +++ /dev/null @@ -1,37 +0,0 @@ -library ieee; -use ieee.std_logic_1164.all; -use ieee.numeric_std.all; - -entity ent is - port ( - clk : in std_logic; - a : in signed(7 downto 0); - b : out signed(7 downto 0) - ); -end; - -architecture a of ent is -begin - process(clk) - begin - if rising_edge(clk) then - b <= abs a; - end if; - end process; - - formal: block - signal last_a : signed(7 downto 0); - signal has_run : std_logic := '0'; - begin - process(clk) - begin - if rising_edge(clk) then - has_run <= '1'; - last_a <= a; - end if; - end process; - - default clock is rising_edge(clk); - assert always has_run -> b >= 0 or (last_a = x"80" and last_a = b); - end block; -end; diff --git a/testsuite/formal/abs/testsuite.sh b/testsuite/formal/abs/testsuite.sh deleted file mode 100755 index 10ec36d..0000000 --- a/testsuite/formal/abs/testsuite.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -topdir=../.. -. $topdir/testenv.sh - -formal "test_abs" - -clean -echo OK diff --git a/testsuite/formal/gates/test_abs.sby b/testsuite/formal/gates/test_abs.sby new file mode 100644 index 0000000..0e4bc7c --- /dev/null +++ b/testsuite/formal/gates/test_abs.sby @@ -0,0 +1,13 @@ +[options] +#depth 6 +mode prove + +[engines] +smtbmc z3 + +[script] +ghdl --std=08 test_abs.vhd -e ent +prep -top ent + +[files] +test_abs.vhd diff --git a/testsuite/formal/gates/test_abs.vhd b/testsuite/formal/gates/test_abs.vhd new file mode 100644 index 0000000..3e711b2 --- /dev/null +++ b/testsuite/formal/gates/test_abs.vhd @@ -0,0 +1,37 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity ent is + port ( + clk : in std_logic; + a : in signed(7 downto 0); + b : out signed(7 downto 0) + ); +end; + +architecture a of ent is +begin + process(clk) + begin + if rising_edge(clk) then + b <= abs a; + end if; + end process; + + formal: block + signal last_a : signed(7 downto 0); + signal has_run : std_logic := '0'; + begin + process(clk) + begin + if rising_edge(clk) then + has_run <= '1'; + last_a <= a; + end if; + end process; + + default clock is rising_edge(clk); + assert always has_run -> b >= 0 or (last_a = x"80" and last_a = b); + end block; +end; diff --git a/testsuite/formal/gates/test_asr.sby b/testsuite/formal/gates/test_asr.sby new file mode 100644 index 0000000..bfc39e9 --- /dev/null +++ b/testsuite/formal/gates/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/gates/test_asr.vhd b/testsuite/formal/gates/test_asr.vhd new file mode 100644 index 0000000..dac8cd2 --- /dev/null +++ b/testsuite/formal/gates/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/gates/test_lsl.sby b/testsuite/formal/gates/test_lsl.sby new file mode 100644 index 0000000..280c16c --- /dev/null +++ b/testsuite/formal/gates/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/gates/test_lsl.vhd b/testsuite/formal/gates/test_lsl.vhd new file mode 100644 index 0000000..737f03b --- /dev/null +++ b/testsuite/formal/gates/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/gates/test_lsr.sby b/testsuite/formal/gates/test_lsr.sby new file mode 100644 index 0000000..aacce69 --- /dev/null +++ b/testsuite/formal/gates/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/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; diff --git a/testsuite/formal/gates/testsuite.sh b/testsuite/formal/gates/testsuite.sh new file mode 100755 index 0000000..7986d8c --- /dev/null +++ b/testsuite/formal/gates/testsuite.sh @@ -0,0 +1,11 @@ +#!/bin/sh + +topdir=../.. +. $topdir/testenv.sh + +for f in abs lsl lsr asr; do + formal "test_${f}" +done + +clean +echo OK diff --git a/testsuite/formal/shifts/test_asr.sby b/testsuite/formal/shifts/test_asr.sby deleted file mode 100644 index bfc39e9..0000000 --- a/testsuite/formal/shifts/test_asr.sby +++ /dev/null @@ -1,13 +0,0 @@ -[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 deleted file mode 100644 index dac8cd2..0000000 --- a/testsuite/formal/shifts/test_asr.vhd +++ /dev/null @@ -1,79 +0,0 @@ -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 deleted file mode 100644 index 280c16c..0000000 --- a/testsuite/formal/shifts/test_lsl.sby +++ /dev/null @@ -1,13 +0,0 @@ -[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 deleted file mode 100644 index 737f03b..0000000 --- a/testsuite/formal/shifts/test_lsl.vhd +++ /dev/null @@ -1,92 +0,0 @@ -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 deleted file mode 100644 index aacce69..0000000 --- a/testsuite/formal/shifts/test_lsr.sby +++ /dev/null @@ -1,13 +0,0 @@ -[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 deleted file mode 100644 index 60ac66d..0000000 --- a/testsuite/formal/shifts/test_lsr.vhd +++ /dev/null @@ -1,75 +0,0 @@ -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 deleted file mode 100755 index 935e995..0000000 --- a/testsuite/formal/shifts/testsuite.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -topdir=../.. -. $topdir/testenv.sh - -for f in lsl lsr asr; do - formal "test_${f}" -done - -clean -echo OK -- cgit v1.2.3