Add simple VHDL+PSL example

[yosys.git] / tests / sva / vhdlpsl00.vhd

diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd
new file mode 100644 (file)
index 0000000..6d765d5
--- /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;