From d68ea88578cf67085c872f51cbde5d8e05fc507e Mon Sep 17 00:00:00 2001 From: tmeissner Date: Fri, 15 May 2020 15:10:57 +0200 Subject: [PATCH] Add more asserts using variants of [*] --- src/psl_sere_consecutive_repetition.vhd | 33 +++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/psl_sere_consecutive_repetition.vhd b/src/psl_sere_consecutive_repetition.vhd index b455175..7fefcaa 100644 --- a/src/psl_sere_consecutive_repetition.vhd +++ b/src/psl_sere_consecutive_repetition.vhd @@ -14,6 +14,8 @@ end entity psl_sere_consecutive_repetition; architecture psl of psl_sere_consecutive_repetition is signal a, b, c : std_logic; + signal d, e, f : std_logic; + signal g, h, i : std_logic; begin @@ -23,6 +25,16 @@ begin SEQ_B : sequencer generic map ("__----___") port map (clk, b); SEQ_C : sequencer generic map ("______-__") port map (clk, c); + -- 012345 + SEQ_D : sequencer generic map ("_-____") port map (clk, d); + SEQ_E : sequencer generic map ("______") port map (clk, e); + SEQ_F : sequencer generic map ("__-___") port map (clk, f); + + -- 012345678 + SEQ_G : sequencer generic map ("_-_______") port map (clk, g); + SEQ_H : sequencer generic map ("__-_-_-__") port map (clk, h); + SEQ_I : sequencer generic map ("_______-_") port map (clk, i); + -- All is sensitive to rising edge of clk default clock is rising_edge(clk); @@ -42,5 +54,26 @@ begin -- This assertion holds SERE_4_a : assert always {a} |=> {b[+]; c}; + -- This assertion holds + SERE_5_a : assert always {d} |=> {e[*]; f}; + + -- This assertion doesn't hold at cycle 2 + SERE_6_a : assert always {d} |=> {e[+]; f}; + + -- This assertion doesn't hold at cycle 3 + SERE_7_a : assert always {g} |=> {h[*3]; i}; + + -- This assertion doesn't hold at cycle 3 + SERE_8_a : assert always {g} |=> {h[*2 to 4]; i}; + + -- This assertion doesn't hold at cycle 3 + SERE_9_a : assert always {g} |=> {h[*]; i}; + + -- This assertion doesn't hold at cycle 3 + SERE_10_a : assert always {g} |=> {h[+]; i}; + + -- This assertion holds + SERE_11_a : assert always {g} |=> {[*5]; i}; + end architecture psl;