From cef17d03f8d9eb870b322dab2b6ac5f782c9af77 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 4 Aug 2022 15:39:22 +0200 Subject: [PATCH] Update PSL next_event_a example as ghdl issue ghdl/ghdl#2157 was fixed --- README.md | 1 - src/psl_next_event_a.vhd | 9 +++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 6edb75d..a92ba54 100644 --- a/README.md +++ b/README.md @@ -100,7 +100,6 @@ The next lists will grow during further development ## Supported, but under investigation -* `next_event_a[i to j]` operator * `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345) ## Further Ressources diff --git a/src/psl_next_event_a.vhd b/src/psl_next_event_a.vhd index 168c1f5..09b5185 100644 --- a/src/psl_next_event_a.vhd +++ b/src/psl_next_event_a.vhd @@ -32,10 +32,11 @@ begin default clock is rising_edge(clk); -- Check for one possible value of b - -- Both assertions should hold - -- Assertions don't hold, assuming GHDL bug - NEXT_EVENT_0_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4")); - NEXT_EVENT_1_a : assert always ((a and b = x"5") -> next_event_a(c)[1 to 4](b = x"5")); + -- Both assertions hold (see ghdl/ghdl#2157) + NEXT_EVENT_0_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4")) + report "NEXT_EVENT_0_a failed"; + NEXT_EVENT_1_a : assert always ((a and b = x"5") -> next_event_a(c)[1 to 4](b = x"5")) + report "NEXT_EVENT_1_a failed"; -- Check for all possible values of b