1 files changed, 34 insertions, 0 deletions
diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd
new file mode 100644
index 000000000..6d765d5a9
--- /dev/null
+++ b/tests/sva/vhdlpsl00.vhd
@@ -0,0 +1,34 @@
+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;