diff options
Diffstat (limited to 'testsuite/formal')
-rw-r--r-- | testsuite/formal/gates/test_minmax.sby | 12 | ||||
-rw-r--r-- | testsuite/formal/gates/test_minmax.vhd | 57 | ||||
-rwxr-xr-x | testsuite/formal/gates/testsuite.sh | 2 |
3 files changed, 70 insertions, 1 deletions
diff --git a/testsuite/formal/gates/test_minmax.sby b/testsuite/formal/gates/test_minmax.sby new file mode 100644 index 0000000..c7d103a --- /dev/null +++ b/testsuite/formal/gates/test_minmax.sby @@ -0,0 +1,12 @@ +[options] +mode prove + +[engines] +smtbmc z3 + +[script] +ghdl --std=08 test_minmax.vhd -e ent +prep -top ent + +[files] +test_minmax.vhd diff --git a/testsuite/formal/gates/test_minmax.vhd b/testsuite/formal/gates/test_minmax.vhd new file mode 100644 index 0000000..8cd760c --- /dev/null +++ b/testsuite/formal/gates/test_minmax.vhd @@ -0,0 +1,57 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity ent is + port ( + clk : in std_logic; + a : in std_logic_vector(7 downto 0); + b : in std_logic_vector(7 downto 0); + min_sgn : out signed(7 downto 0); + max_sgn : out signed(7 downto 0); + min_uns : out unsigned(7 downto 0); + max_uns : out unsigned(7 downto 0) + ); +end; + +architecture a of ent is +begin + process(clk) + begin + if rising_edge(clk) then + min_sgn <= minimum(signed(a), signed(b)); + max_sgn <= maximum(signed(a), signed(b)); + + min_uns <= minimum(unsigned(a), unsigned(b)); + max_uns <= maximum(unsigned(a), unsigned(b)); + end if; + end process; + + formal: block + signal prev_a : std_logic_vector(7 downto 0); + signal prev_b : std_logic_vector(7 downto 0); + signal has_run : std_logic := '0'; + begin + process(clk) + begin + if rising_edge(clk) then + has_run <= '1'; + prev_a <= a; + prev_b <= b; + end if; + end process; + + default clock is rising_edge(clk); + assert eventually! has_run; + + assert always has_run and signed(prev_a) <= signed(prev_b) -> + min_sgn = signed(prev_a) and max_sgn = signed(prev_b); + assert always has_run and signed(prev_a) >= signed(prev_b) -> + min_sgn = signed(prev_b) and max_sgn = signed(prev_a); + + assert always has_run and unsigned(prev_a) <= unsigned(prev_b) -> + min_uns = unsigned(prev_a) and max_uns = unsigned(prev_b); + assert always has_run and unsigned(prev_a) >= unsigned(prev_b) -> + min_uns = unsigned(prev_b) and max_uns = unsigned(prev_a); + end block; +end; diff --git a/testsuite/formal/gates/testsuite.sh b/testsuite/formal/gates/testsuite.sh index 7986d8c..d4bcf98 100755 --- a/testsuite/formal/gates/testsuite.sh +++ b/testsuite/formal/gates/testsuite.sh @@ -3,7 +3,7 @@ topdir=../.. . $topdir/testenv.sh -for f in abs lsl lsr asr; do +for f in abs minmax lsl lsr asr; do formal "test_${f}" done |