|
|
- library ieee;
- use ieee.std_logic_1164.all;
-
- use work.pkg.all;
-
-
- entity psl_sere_non_consecutive_goto_repetition is
- port (
- clk : in std_logic
- );
- end entity psl_sere_non_consecutive_goto_repetition;
-
-
- architecture psl of psl_sere_non_consecutive_goto_repetition is
-
- signal req, busy, done : std_logic;
-
- begin
-
-
- -- 012345678
- SEQ_REQ : sequencer generic map ("_-_______") port map (clk, req);
- SEQ_BUSY : sequencer generic map ("__-_-_-__") port map (clk, busy);
- SEQ_DONE : sequencer generic map ("_______-_") port map (clk, done);
-
-
- -- All is sensitive to rising edge of clk
- default clock is rising_edge(clk);
-
- -- Non consecutive repetition of 3 cycles without padding
- -- busy has to hold on 3 cycles between req & done
- -- This assertion holds
- SERE_0_a : assert always {req} |=> {busy[->3]; done};
-
- -- Non consecutive repetition of 2 to 4 cycles without padding
- -- busy has to hold on 2 to 4 cycles between req & done
- -- This assertion holds
- SERE_1_a : assert always {req} |=> {busy[->2 to 4]; done};
-
- -- Non consecutive repetition of 5 cycles without padding
- -- busy has to hold on 5 cycles between req & done
- -- This assertion holds -> possible PITFALL!
- -- RHS is underspecified, nothing prevents done to hold between or together
- -- with holding busy. For intentioned behaviour, the behaviour of done
- -- has to be described more specificly (see SERE_3_a)
- SERE_2_a : assert always {req} |=> {busy[->5]; done};
-
- -- Non consecutive repetition of 3 cycles without padding
- -- busy has to hold on exactly 3 cycles between req & and the first done
- -- This is a more exact version of the assertions before using
- -- the length-matching and SERE operator &&
- -- This assertion holds
- SERE_3_a : assert always {req} |=> {{{busy[->3]} && {not done[+]}}; done};
-
- -- Non consecutive repetition of 4 cycles without padding
- -- busy has to hold on exactly 4 cycles between req & and the first done
- -- This assertion doesn't hold at cycle 7
- SERE_4_a : assert always {req} |=> {{{busy[->4]} && {not done[+]}}; done};
-
- -- Equivalent to SERE_3_a
- -- This assertion holds
- SERE_5_a : assert always {req} |=> {{{busy[=2]; busy[->]} && {not done[+]}}; done};
-
- -- Stop simulation after longest running sequencer is finished
- -- Simulation only code by using pragmas
- -- synthesis translate_off
- stop_sim(clk, 9);
- -- synthesis translate_on
-
-
- end architecture psl;
|