PSL next_event_e operator now supported by GHDL :)

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)

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

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;