Browse Source

Exclude crashing eventually example from formal tests

master
T. Meissner 4 years ago
parent
commit
a5afca8752
6 changed files with 5 additions and 4 deletions
  1. +0
    -0
      .github/workflows/formal.yml
  2. +1
    -2
      formal/tests.mk
  3. +1
    -1
      sim/tests.mk
  4. +1
    -0
      src/psl_before.vhd
  5. +1
    -1
      src/psl_eventually.vhd
  6. +1
    -0
      src/psl_logical_implication.vhd

.github/workflows/test.yml → .github/workflows/formal.yml View File


+ 1
- 2
formal/tests.mk View File

@ -12,7 +12,6 @@ psl_next_event_e \
psl_next_event_a \
psl_until \
psl_before \
psl_eventually \
psl_sere \
psl_sere_overlapping_suffix_impl \
psl_sere_non_overlapping_suffix_impl \
@ -22,4 +21,4 @@ psl_sere_non_consecutive_goto_repetition \
psl_cover \
psl_sere_within \
psl_sere_or \
psl_sere_len_matching_and
psl_sere_len_matching_and

+ 1
- 1
sim/tests.mk View File

@ -22,4 +22,4 @@ psl_sere_non_consecutive_goto_repetition \
psl_cover \
psl_sere_within \
psl_sere_or \
psl_sere_len_matching_and
psl_sere_len_matching_and

+ 1
- 0
src/psl_before.vhd View File

@ -78,4 +78,5 @@ begin
stop_sim(clk, 11);
-- synthesis translate_on
end architecture psl;

+ 1
- 1
src/psl_eventually.vhd View File

@ -28,7 +28,7 @@ begin
-- This assertion holds
-- This assertion leads to a GHDL synthesis crash with bug report
--EVENTUALLY_a : assert always (a -> eventually! b);
EVENTUALLY_a : assert always (a -> eventually! b);
-- Stop simulation after longest running sequencer is finished
-- Simulation only code by using pragmas


+ 1
- 0
src/psl_logical_implication.vhd View File

@ -50,4 +50,5 @@ begin
stop_sim(clk, 11);
-- synthesis translate_on
end architecture psl;

Loading…
Cancel
Save