diff options
author | Xiretza <Xiretza@users.noreply.github.com> | 2020-03-10 18:20:23 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-10 18:20:23 +0100 |
commit | d11471a86eebd0e041032bce74672744ec48ee61 (patch) | |
tree | 84bf28063e24841d64f29672b39e6bcaf1374f5d /testsuite/formal | |
parent | 33f046ca40aae8419e4ea3310cc0f76b537fdefe (diff) | |
download | ghdl-yosys-plugin-d11471a86eebd0e041032bce74672744ec48ee61.tar.gz ghdl-yosys-plugin-d11471a86eebd0e041032bce74672744ec48ee61.tar.bz2 ghdl-yosys-plugin-d11471a86eebd0e041032bce74672744ec48ee61.zip |
Add abs gate (#91)
Diffstat (limited to 'testsuite/formal')
-rw-r--r-- | testsuite/formal/abs/test_abs.sby | 13 | ||||
-rw-r--r-- | testsuite/formal/abs/test_abs.vhd | 37 | ||||
-rwxr-xr-x | testsuite/formal/abs/testsuite.sh | 9 |
3 files changed, 59 insertions, 0 deletions
diff --git a/testsuite/formal/abs/test_abs.sby b/testsuite/formal/abs/test_abs.sby new file mode 100644 index 0000000..0e4bc7c --- /dev/null +++ b/testsuite/formal/abs/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/abs/test_abs.vhd b/testsuite/formal/abs/test_abs.vhd new file mode 100644 index 0000000..3e711b2 --- /dev/null +++ b/testsuite/formal/abs/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/abs/testsuite.sh b/testsuite/formal/abs/testsuite.sh new file mode 100755 index 0000000..10ec36d --- /dev/null +++ b/testsuite/formal/abs/testsuite.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +topdir=../.. +. $topdir/testenv.sh + +formal "test_abs" + +clean +echo OK |