Remove PSL example from tests/sva/

diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 35c95a3e048a521a059188106117aa551ea8defc..4c8e16542d516479cd1fa699c3bc3d07311940b5 100644 (file)
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -29,7 +29,7 @@ generate_sby() {
        fi
 
        if [ -f $prefix.vhd ]; then
-               echo "verific -vhdpsl $prefix.vhd"
+               echo "verific -vhdl $prefix.vhd"
        fi
 
        cat <<- EOT

diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd
deleted file mode 100644 (file)
index 6d765d5..0000000
--- a/tests/sva/vhdlpsl00.vhd
+++ /dev/null
@@ -1,34 +0,0 @@
-library ieee;
-use ieee.std_logic_1164.all;
-use ieee.std_logic_unsigned.all;
-use ieee.numeric_std.all;
-
-entity top is
-       port (
-               clk : in std_logic;
-               rst : in std_logic;
-               up : in std_logic;
-               down : in std_logic;
-               cnt : buffer std_logic_vector(7 downto 0)
-       );
-end entity;
-
-architecture rtl of top is
-begin
-       process (clk) begin
-               if rising_edge(clk) then
-                       if rst = '1' then
-                               cnt <= std_logic_vector(to_unsigned(0, 8));
-                       elsif up = '1' then
-                               cnt <= cnt + std_logic_vector(to_unsigned(1, 8));
-                       elsif down = '1' then
-                               cnt <= cnt - std_logic_vector(to_unsigned(1, 8));
-                       end if;
-               end if;
-       end process;
-
-       -- PSL default clock is (rising_edge(clk));
-       -- PSL assume always ( down -> not up );
-       -- PSL assert always ( up |=> (cnt = prev(cnt) + std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
-       -- PSL assert always ( down |=> (cnt = prev(cnt) - std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
-end architecture;