From 2fdf7d99e34ab3f45fc6909992a41902c27d0b3f Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 9 May 2020 13:56:37 +0200 Subject: [PATCH] PSL next_event_e operator now supported by GHDL :) --- README.md | 5 +++-- formal/tests.mk | 1 + src/psl_next_event_e.vhd | 25 +++++-------------------- 3 files changed, 9 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 84e65df..a19f2af 100644 --- a/README.md +++ b/README.md @@ -32,6 +32,7 @@ The next two lists will grow during further development * next_e[i to j] operator * next_event operator * next_event[n] operator +* next_event_e[i to j] operator * until operator * until_ operator * before operator (GHDL crash with a specific property, see psl_before.vhd) @@ -39,9 +40,9 @@ The next two lists will grow during further development ## PSL features not yet supported by GHDL: -* next_event_a[i to j] operator -* next_event_e[i to j] operator +* forall statement ## PSL features supported by GHDL but with wrong behaviour * 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 (Behaviour currently under verification) diff --git a/formal/tests.mk b/formal/tests.mk index 7e30155..d646d58 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -7,6 +7,7 @@ psl_next_a \ psl_next_e \ psl_next_event \ psl_next_event_4 \ +psl_next_event_e \ psl_until \ psl_before \ psl_eventually diff --git a/src/psl_next_event_e.vhd b/src/psl_next_event_e.vhd index d04b53a..34ff694 100644 --- a/src/psl_next_event_e.vhd +++ b/src/psl_next_event_e.vhd @@ -24,30 +24,15 @@ begin SEQ_C : sequencer generic map ("______-___-____") port map (clk, c); - -- All is sensitive to rising edge of clk default clock is rising_edge(clk); -- This assertion holds - NEXT_EVENT_a : assert always (a -> next_event_e(b)[1 to 2](c)); - - - -- psl.sem_property: cannot handle N_NEXT_EVENT_E - -- - -- ******************** GHDL Bug occurred *************************** - -- Please report this bug on https://github.com/ghdl/ghdl/issues - -- GHDL release: 1.0-dev (tarball) [Dunoon edition] - -- Compiled with GNAT Version: 8.3.0 - -- Target: x86_64-linux-gnu - -- /build/src/ - -- Command line: - -- ghdl --synth --std=08 pkg.vhd sequencer.vhd psl_next_event_e.vhd -e psl_next_event_e - -- Exception TYPES.INTERNAL_ERROR raised - -- Exception information: - -- raised TYPES.INTERNAL_ERROR : psl-errors.adb:39 - -- Call stack traceback locations: - -- 0x55607472bb3a 0x55607484fbb7 0x55607484f8f1 0x55607484f69f 0x55607484f765 0x556074850557 0x556074856fd7 0x5560748570de 0x556074857235 0x55607488f17d 0x556074895e72 0x55607484d9c2 0x55607484e814 0x55607484e9bc 0x5560748f61c6 0x556074934ab9 0x556074935361 0x55607484536f 0x55607493ecaf 0x5560746f7fa3 0x7f2cefe1f099 0x5560746f6df8 0xfffffffffffffffe - -- ****************************************************************** + NEXT_EVENT_0_a : assert always (a -> next_event_e(b)[1 to 2](c)); + + -- This assertion doesn't hold at cycle 13 + -- 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)); end architecture psl;