From 0aa92b4d4fce27d9db50b4427a9efc66aaafa774 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Fri, 29 May 2020 19:46:56 +0200 Subject: [PATCH] Include eventually example in formal tests after ghdl/ghdl#1345 was fixed --- README.md | 5 +++-- formal/tests.mk | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index a37d213..8d67c07 100644 --- a/README.md +++ b/README.md @@ -40,8 +40,8 @@ The next lists will grow during further development * next_event_e[i to j] operator * until operator * until_ operator -* before operator (GHDL crash with a specific property, see psl_before.vhd) -* eventually! operator (simulation, synthesis produces a GHDL crash, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345)) +* before operator (GHDL crash with a specific invalid property, see [PSL before example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_before.vhd#L53)) +* eventually! operator ### Sequential Extended Regular Expressions (SERE style) @@ -64,6 +64,7 @@ The next lists will grow during further development * before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd) * next_event_a[i to j] operator +* eventually! behaviour with (un)bounded proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345) ## Further Ressources diff --git a/formal/tests.mk b/formal/tests.mk index 3678c49..1d939df 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -12,6 +12,7 @@ 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 \