testsuite/synth/psl01/sequence0.vhdl

   1 library ieee;
   2 use ieee.std_logic_1164.all;
   3 use ieee.numeric_std.all;
   4
   5 entity sequence0 is
   6  port (clk, rst: std_logic;
   7        cnt : out unsigned(3 downto 0));
   8 end sequence0;
   9
  10 architecture behav of sequence0 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  sequence seq is {val = 8; val = 9};
  27
  28  assert always seq |=> {val = 10} abort rst;
  29
  30  cover seq;
  31
  32 end behav;