library ieee;
  use ieee.std_logic_1164.all;

use work.pkg.all;


entity psl_rose is
  port (
    clk : in std_logic
  );
end entity psl_rose;


architecture psl of psl_rose is

  signal a, b : std_logic;

begin


  --                              01234567890
  SEQ_A : sequencer generic map ("_--__-_---_") port map (clk, a);
  SEQ_B : sequencer generic map ("_-___-_-___") port map (clk, b);


  -- All is sensitive to rising edge of clk
  default clock is rising_edge(clk);

  -- This assertion holds
  ROSE_0_a : assert always (rose(a) -> b);

  -- This assertion holds
  ROSE_1_a : assert always {not a; a} |-> rose(a);

  -- This assertion holds
  ROSE_2_a : assert always (rose(a) -> (not prev(a) and a));

  -- Workaround needed before rose() is implemented
  -- With VHDL glue logic generating the
  -- previous value of a and simple comparing the two values
  d_reg : block is
    signal a_prev : std_logic := '0';
  begin
    process (clk) is
    begin
      if rising_edge(clk) then
        a_prev <= a;
      end if;
    end process;
    ROSE_3_a : assert always (a and not a_prev -> b);
  end block d_reg;

  -- Another workaround by using simple SERE concatenation on LHS
  ROSE_4_a : assert always {not a; a} |-> b;

  -- Stop simulation after longest running sequencer is finished
  -- Simulation only code by using pragmas
  -- synthesis translate_off
  stop_sim(clk, 11);
  -- synthesis translate_on


end architecture psl;