testsuite/synth/psl01/property0.vhdl

   1 library ieee;
   2 use ieee.std_logic_1164.all;
   3 use ieee.numeric_std.all;
   4
   5 entity property0 is
   6  port (clk, rst: std_logic;
   7        cnt : out unsigned(3 downto 0));
   8 end property0;
   9
  10 architecture behav of property0 is
  11  signal val : unsigned (3 downto 0);
  12  default clock is rising_edge(clk);
  13 begin
  14  process(clk)
  15  begin
  16    if rising_edge(clk) then
  17      if rst = '1' then
  18        val <= (others => '0');
  19      else
  20        val <= val + 1;
  21      end if;
  22    end if;
  23  end process;
  24  cnt <= val;
  25
  26  property prop is always {val = 8} |=> {val = 9} abort rst;
  27
  28  assert prop;
  29
  30 end behav;