Add more failing assertions (should hold, assuming GHDL bug) to next_event_a example

formal/tests.mk

@@ -8,6 +8,7 @@ psl_next_e \
 psl_next_event \
 psl_next_event_4 \
 psl_next_event_e \
+psl_next_event_a \
 psl_until \
 psl_before \
 psl_eventually

src/psl_next_event_a.vhd

@@ -1,6 +1,7 @@
 library ieee;
   use ieee.std_logic_1164.all;
   use ieee.numeric_std.all;
+  use ieee.math_real.all;
 
 use work.pkg.all;
 
@@ -20,10 +21,10 @@ architecture psl of psl_next_event_a is
 begin
 
 
-  --                                  012345678901234567890
-  SEQ_A : sequencer generic map     ("_-______________-____") port map (clk, a);
-  SEQ_B : hex_sequencer generic map ("443334477444433355555") port map (clk, b);
-  SEQ_C : sequencer generic map     ("_____-___---_____----") port map (clk, c);
+  --                                  012345678901234567890123
+  SEQ_A : sequencer generic map     ("_-______________-_______") port map (clk, a);
+  SEQ_B : hex_sequencer generic map ("443334477444433355554555") port map (clk, b);
+  SEQ_C : sequencer generic map     ("_____-___---______--_--_") port map (clk, c);
 
 
 
@@ -31,40 +32,26 @@ begin
   default clock is rising_edge(clk);
 
   -- Check for one possible value of b
-  -- This assertion holds
-  NEXT_EVENT_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4"));
+  -- 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"));
+
 
   -- Check for all possible values of b
   -- Workaround for missing PSL forall in {i to j} statement
-  -- This assertion holds
-  check_b : for i in 0 to 0 generate
+  -- This assertions should hold
+  -- Assertions for i = 4 & i = 5 don't hold, assuming GHDL bug
+  check_b : for i in 0 to 2**b'length-1 generate
     signal i_slv : std_logic_vector(b'range);
   begin
     i_slv <= std_logic_vector(to_unsigned(i, 4));
-    --Without name it works
+    -- Without name it works
     assert always ((a and b = i_slv) -> next_event_a(c)[1 to 4](b = i_slv));
     -- This errors because of similar names for all asserts
     -- ERROR: Assert `count_id(cell->name) == 0' failed in kernel/rtlil.cc:1613.
-    -- NEXT_EVENT_a : assert always ((a and b = i_slv) -> next_event_a(c)[1](b = i_slv));
+    -- NEXT_EVENT_a : assert always ((a and b = i_slv) -> next_event_a(c)[1 to 4](b = i_slv));
   end generate check_b;
 
 
-  -- psl.sem_property: cannot handle N_NEXT_EVENT_A
-  --
-  -- ******************** 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 hex_sequencer.vhd psl_next_event_a.vhd -e psl_next_event_a
-  -- Exception TYPES.INTERNAL_ERROR raised
-  -- Exception information:
-  -- raised TYPES.INTERNAL_ERROR : psl-errors.adb:39
-  -- Call stack traceback locations:
-  -- 0x556095397b3a 0x5560954bbbb7 0x5560954bb8f1 0x5560954bb69f 0x5560954bb765 0x5560954bc557 0x5560954c2fd7 0x5560954c30de 0x5560954c3235 0x5560954fb17d 0x556095501e72 0x5560954b99c2 0x5560954ba814 0x5560954ba9bc 0x5560955621c6 0x5560955a0ab9 0x5560955a1361 0x5560954b136f 0x5560955aacaf 0x556095363fa3 0x7f72faa58099 0x556095362df8 0xfffffffffffffffe
-  -- ******************************************************************
-
-
 end architecture psl;