From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 20 Oct 2017 11:16:24 +0000 (+0200)
Subject: Remove PSL example from tests/sva/
X-Git-Tag: yosys-0.8~289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=baddb017fe5eb72fbb65d6f89553dc2341663613;p=yosys.git

Remove PSL example from tests/sva/
---

diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 35c95a3e0..4c8e16542 100644
--- 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
index 6d765d5a9..000000000
--- 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;