diff --git a/src/psl_sere_or.vhd b/src/psl_sere_or.vhd index 2e9cd3d..0dea4df 100644 --- a/src/psl_sere_or.vhd +++ b/src/psl_sere_or.vhd @@ -14,6 +14,7 @@ end entity psl_sere_or; architecture psl of psl_sere_or is signal req2, req4, busy, valid, done : std_logic; + signal req, wen, ren, ends : std_logic; begin @@ -25,22 +26,36 @@ begin SEQ_VALID : sequencer generic map ("___-_-____-_-_-_-__") port map (clk, valid); SEQ_DONE : sequencer generic map ("______-__________-_") port map (clk, done); + -- 0123456789012345678 + SEQ_REQ : sequencer generic map ("_-_______-__________") port map (clk, req); + SEQ_WEN : sequencer generic map ("___-_-_____-_-_-_-__") port map (clk, wen); + SEQ_ENDS : sequencer generic map ("_______-__________-_") port map (clk, ends); + -- All is sensitive to rising edge of clk default clock is rising_edge(clk); + -- Transfer started by req2 with 2 valids has to be finished by done -- This assertion holds SERE_0_a : assert always {req2 ; {valid[->2]} && {busy and not done}[+]} |=> {not busy and done}; + -- Transfer started by req4 with 4 valids has to be finished by done -- This assertion holds SERE_1_a : assert always {req4 ; {valid[->4]} && {busy and not done}[+]} |=> {not busy and done}; - -- SERE or operato + -- SERE or operator -- Combination of both assertions above -- This assertion holds - SERE_2_a : assert always {{req2 ; {valid[->2]} && {busy and not done}[+]} | - {req4 ; {valid[->4]} && {busy and not done}[+]}} |=> + SERE_2_a : assert always {{req2; {valid[->2]} && {busy and not done}[+]} | + {req4; {valid[->4]} && {busy and not done}[+]}} |=> {not busy and done}; + -- SERE or operator + -- Transfer started by req has to have 2 or 4 cycles write cycles, finished by ends + -- This assertion holds + SERE_3_a : assert always {req} |=> + {{{wen[=2]} && {not ends[+]}} | + {{wen[=4]} && {not ends[+]}}; ends}; + end architecture psl;