aboutsummaryrefslogtreecommitdiffstats
path: root/testsuite/formal/gates
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/formal/gates')
-rw-r--r--testsuite/formal/gates/test_abs.sby13
-rw-r--r--testsuite/formal/gates/test_abs.vhd37
-rw-r--r--testsuite/formal/gates/test_asr.sby13
-rw-r--r--testsuite/formal/gates/test_asr.vhd79
-rw-r--r--testsuite/formal/gates/test_lsl.sby13
-rw-r--r--testsuite/formal/gates/test_lsl.vhd92
-rw-r--r--testsuite/formal/gates/test_lsr.sby13
-rw-r--r--testsuite/formal/gates/test_lsr.vhd75
-rwxr-xr-xtestsuite/formal/gates/testsuite.sh11
9 files changed, 346 insertions, 0 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 02:35:25 +0000