From b405a27654f326eb1117c0eda8e7389a64fc5c94 Mon Sep 17 00:00:00 2001 From: "T. Meissner" Date: Mon, 7 Oct 2019 19:13:46 +0200 Subject: 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 --- testsuite/formal/shifts/test_lsr.vhd | 75 ++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 testsuite/formal/shifts/test_lsr.vhd (limited to 'testsuite/formal/shifts/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; -- cgit v1.2.3