You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
71 lines
2.4 KiB
71 lines
2.4 KiB
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;
|