diff --git a/sim/Makefile b/sim/Makefile index c14de31..fdc4b29 100644 --- a/sim/Makefile +++ b/sim/Makefile @@ -14,7 +14,7 @@ all: ${psl_tests} ghdl -a --std=$(VHD_STD) --workdir=work/$@ ../src/$@.vhd ghdl -a --std=$(VHD_STD) --workdir=work/$@ work/$@/testbench.vhd ghdl -e --std=$(VHD_STD) --workdir=work/$@ -o work/$@/tb_$@ tb_$@ - cd work/$@; ghdl -r --std=$(VHD_STD) tb_$@ --wave=$@.ghw --psl-report=$@_psl_coverage.json --stop-time=50ns + cd work/$@; ghdl -r --std=$(VHD_STD) tb_$@ --wave=$@.ghw --psl-report=$@_psl_coverage.json work/%/testbench.vhd: template.vhd mkdir -p work; mkdir -p $(dir $@) diff --git a/sim/template.vhd b/sim/template.vhd index 6d64f47..b143792 100644 --- a/sim/template.vhd +++ b/sim/template.vhd @@ -14,7 +14,7 @@ architecture sim of tb___DUT__ is begin - clk <= not clk after 1 ns; + clk <= not clk after 500 ps; cycle <= cycle + 1 when rising_edge(clk); diff --git a/src/pkg.vhd b/src/pkg.vhd index f9127af..62024c0 100644 --- a/src/pkg.vhd +++ b/src/pkg.vhd @@ -1,6 +1,8 @@ library ieee; use ieee.std_logic_1164.all; +use std.env.all; + package pkg is @@ -28,6 +30,10 @@ package pkg is function to_bit (a : in character) return std_logic; function to_hex (a : in character) return std_logic_vector; + -- synthesis translate_off + procedure stop_sim (signal clk : in std_logic; cycles : in natural; add_cycles : in natural := 2); + -- synthesis translate_on + end package pkg; @@ -71,5 +77,20 @@ package body pkg is return ret; end function to_hex; + -- synthesis translate_off + procedure stop_sim (signal clk : in std_logic; cycles : in natural; add_cycles : in natural := 2) is + variable index : natural := cycles + 5; + begin + loop + wait until rising_edge(clk); + index := index - 1; + if index = 0 then + exit; + end if; + end loop; + stop(0); + end procedure stop_sim; + -- synthesis translate_on + end package body pkg; diff --git a/src/psl_always.vhd b/src/psl_always.vhd index a4e68b1..111950d 100644 --- a/src/psl_always.vhd +++ b/src/psl_always.vhd @@ -40,5 +40,11 @@ begin -- This assertion doesn't hold at cycle 2 WITH_ALWAYS_a : assert always a; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 6); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_before.vhd b/src/psl_before.vhd index 94c9016..ac4576b 100644 --- a/src/psl_before.vhd +++ b/src/psl_before.vhd @@ -72,5 +72,10 @@ begin -- This assertion holds BEFORE_9_a : assert always (e -> (f or next (f before e))); + -- 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; diff --git a/src/psl_cover.vhd b/src/psl_cover.vhd index ee0b05b..f2e906b 100644 --- a/src/psl_cover.vhd +++ b/src/psl_cover.vhd @@ -62,13 +62,25 @@ begin COVER_LENGTH_7_c : cover {req; {{busy[=7]} && {not done[+]}}; done}; COVER_LENGTH_8_c : cover {req; {{busy[=8]} && {not done[+]}}; done}; - -- BTW: GHDL creates a cover directive for each assert directive + -- BTW: GHDL synthesis creates a cover directive for each assert directive -- which is really nice. So you can run SymbiYosys in cover mode -- to see if your assertions can actually be active. -- This assertion checks for the final done at the end of transfer. -- In cover mode, the LHS side of the property has to hold. -- This cover directive holds at cycle 7 - ASSERT_a : assert always {req; (busy and not done)[=3]; not done} |=> {done}; + ASSERT_a : assert always {req; {{busy[=3]} && {not done[+]}}; not done} |=> {done}; + + -- For simulation, you have to write a separate cover directive when + -- you want to check if your assertion can be active + -- Simply use the LHS of the asserts property + COVER_A : cover {req; {{busy[=3]} && {not done[+]}}; not done} + report "Transfer of length 3"; + + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on end architecture psl; diff --git a/src/psl_eventually.vhd b/src/psl_eventually.vhd index b0002ab..d33dfa4 100644 --- a/src/psl_eventually.vhd +++ b/src/psl_eventually.vhd @@ -30,5 +30,11 @@ begin -- This assertion leads to a GHDL synthesis crash with bug report --EVENTUALLY_a : assert always (a -> eventually! b); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 16); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_logical_implication.vhd b/src/psl_logical_implication.vhd index 74ae838..866d5c0 100644 --- a/src/psl_logical_implication.vhd +++ b/src/psl_logical_implication.vhd @@ -18,7 +18,7 @@ architecture psl of psl_logical_implication is begin - -- 012345 + -- 01234567890 SEQ_A : sequencer generic map ("_-__-___-__") port map (clk, a); SEQ_B : sequencer generic map ("_-______-__") port map (clk, b); SEQ_C : sequencer generic map ("_-__-______") port map (clk, c); @@ -44,5 +44,10 @@ begin -- This assertion holds because LHS of implication never holds IMPLICATION_4_a : assert always (d -> (a and b and c)); + -- 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; diff --git a/src/psl_never.vhd b/src/psl_never.vhd index 9b938fc..c73ba33 100644 --- a/src/psl_never.vhd +++ b/src/psl_never.vhd @@ -36,5 +36,11 @@ begin -- This assertion doesn't hold at cycle 2 NEVER_1_a : assert never b; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 4); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next.vhd b/src/psl_next.vhd index ba51693..4049436 100644 --- a/src/psl_next.vhd +++ b/src/psl_next.vhd @@ -37,5 +37,11 @@ begin -- This assertion doesn't hold at cycle 6 NEXT_1_a : assert always (c -> next d); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 12); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_3.vhd b/src/psl_next_3.vhd index ae94265..51d155a 100644 --- a/src/psl_next_3.vhd +++ b/src/psl_next_3.vhd @@ -45,5 +45,11 @@ begin -- This assertion holds NEXT_2_a : assert always (e -> next[3] (f)); + -- 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; diff --git a/src/psl_next_a.vhd b/src/psl_next_a.vhd index e390da1..c724298 100644 --- a/src/psl_next_a.vhd +++ b/src/psl_next_a.vhd @@ -69,5 +69,11 @@ begin -- This assertion doesn't hold at cycle 5 NEXT_5_a : assert always (k -> next_a[3 to 5] (l)); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 12); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_e.vhd b/src/psl_next_e.vhd index 8ee0808..9f94f70 100644 --- a/src/psl_next_e.vhd +++ b/src/psl_next_e.vhd @@ -69,5 +69,11 @@ begin -- This assertion holds NEXT_5_a : assert always (k -> next_e[3 to 5] (l)); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 12); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_event.vhd b/src/psl_next_event.vhd index e18ecfc..33417d4 100644 --- a/src/psl_next_event.vhd +++ b/src/psl_next_event.vhd @@ -44,5 +44,11 @@ begin -- This assertion doesn't hold at cycle 9 NEXT_EVENT_3_a : assert always (d -> next next_event(e)(f)); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 15); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_event_4.vhd b/src/psl_next_event_4.vhd index 8ff75a8..59450c9 100644 --- a/src/psl_next_event_4.vhd +++ b/src/psl_next_event_4.vhd @@ -30,5 +30,11 @@ begin -- This assertion holds NEXT_EVENT_0_a : assert always (a -> next_event(b)[4](c)); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 16); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_event_a.vhd b/src/psl_next_event_a.vhd index 2c72bcd..168c1f5 100644 --- a/src/psl_next_event_a.vhd +++ b/src/psl_next_event_a.vhd @@ -49,5 +49,11 @@ begin NEXT_EVENT_a : assert always ((a and b = i_slv) -> next_event_a(c)[1 to 4](b = i_slv)); end generate check_b; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 24); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_next_event_e.vhd b/src/psl_next_event_e.vhd index 34ff694..660669f 100644 --- a/src/psl_next_event_e.vhd +++ b/src/psl_next_event_e.vhd @@ -34,5 +34,11 @@ begin -- This assert is similar to using next_event(b)[2](c) NEXT_EVENT_1_a : assert always (a -> next_event_e(b)[2 to 2](c)); + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 15); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere.vhd b/src/psl_sere.vhd index 4088775..9274a9b 100644 --- a/src/psl_sere.vhd +++ b/src/psl_sere.vhd @@ -38,5 +38,11 @@ begin -- This assertion doesn't hold at cycle 2 SERE_3_a : assert always {a; a}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 6); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_consecutive_repetition.vhd b/src/psl_sere_consecutive_repetition.vhd index a78cd2f..b0863a0 100644 --- a/src/psl_sere_consecutive_repetition.vhd +++ b/src/psl_sere_consecutive_repetition.vhd @@ -30,7 +30,7 @@ begin SEQ_E : sequencer generic map ("______") port map (clk, e); SEQ_F : sequencer generic map ("__-___") port map (clk, f); - -- 012345678 + -- 0123456789 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); @@ -105,5 +105,11 @@ begin -- This assertion holds SERE_13_a : assert always {g} |=> {{h; not h}[*3]; i}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_len_matching_and.vhd b/src/psl_sere_len_matching_and.vhd index 7a6a9bc..3a60542 100644 --- a/src/psl_sere_len_matching_and.vhd +++ b/src/psl_sere_len_matching_and.vhd @@ -34,5 +34,11 @@ begin -- This assertion holds SERE_0_a : assert always {req} |=> {{valid[->3]} && {(busy and not done)[+]}; not busy and done}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_non_consecutive_goto_repetition.vhd b/src/psl_sere_non_consecutive_goto_repetition.vhd index 3f3841b..8a45cc0 100644 --- a/src/psl_sere_non_consecutive_goto_repetition.vhd +++ b/src/psl_sere_non_consecutive_goto_repetition.vhd @@ -18,7 +18,7 @@ architecture psl of psl_sere_non_consecutive_goto_repetition is begin - -- 0123456789 + -- 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); @@ -61,5 +61,11 @@ begin -- 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; diff --git a/src/psl_sere_non_consecutive_repeat_repetition.vhd b/src/psl_sere_non_consecutive_repeat_repetition.vhd index 010b60b..19c4c5b 100644 --- a/src/psl_sere_non_consecutive_repeat_repetition.vhd +++ b/src/psl_sere_non_consecutive_repeat_repetition.vhd @@ -57,5 +57,11 @@ begin -- This assertion doesn't hold at cycle 8 SERE_4_a : assert always {req} |=> {{{busy[=4]} && {not done[+]}}; done}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_non_overlapping_suffix_impl.vhd b/src/psl_sere_non_overlapping_suffix_impl.vhd index 544c6c7..e8f1997 100644 --- a/src/psl_sere_non_overlapping_suffix_impl.vhd +++ b/src/psl_sere_non_overlapping_suffix_impl.vhd @@ -35,5 +35,11 @@ begin -- This assertion holds SERE_2_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, 9); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_or.vhd b/src/psl_sere_or.vhd index a73cef7..24ad5ec 100644 --- a/src/psl_sere_or.vhd +++ b/src/psl_sere_or.vhd @@ -26,7 +26,7 @@ begin SEQ_VALID : sequencer generic map ("___-_-____-_-_-_-__") port map (clk, valid); SEQ_DONE : sequencer generic map ("______-__________-_") port map (clk, done); - -- 0123456789012345678 + -- 01234567890123456789 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); @@ -57,5 +57,11 @@ begin {{{wen[=2]} && {not ends[+]}} | {{wen[=4]} && {not ends[+]}}; ends}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 20); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_sere_overlapping_suffix_impl.vhd b/src/psl_sere_overlapping_suffix_impl.vhd index 651bc76..f7746ca 100644 --- a/src/psl_sere_overlapping_suffix_impl.vhd +++ b/src/psl_sere_overlapping_suffix_impl.vhd @@ -35,5 +35,11 @@ begin -- This assertion holds SERE_2_a : assert always {not a; a} |-> next {b}; + -- 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; diff --git a/src/psl_sere_within.vhd b/src/psl_sere_within.vhd index 935ffa0..18b3689 100644 --- a/src/psl_sere_within.vhd +++ b/src/psl_sere_within.vhd @@ -33,5 +33,11 @@ begin -- This assertion holds SERE_0_a : assert always {req} |=> {{valid[=3]} within {(busy and not done)[+]}; not busy and done}; + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on + end architecture psl; diff --git a/src/psl_until.vhd b/src/psl_until.vhd index 689c489..8ceba4b 100644 --- a/src/psl_until.vhd +++ b/src/psl_until.vhd @@ -57,5 +57,11 @@ begin -- This assertion doesn't hold at cycle 2 UNTIL_5_a : assert always (g -> next (h until_ i)); + -- 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;