Add example for next_a operator

* Add example for next_a operator
* Add formal test for next_a operator example
* Move next_a from unsupported to supported list

README.md

@@ -6,7 +6,7 @@ A collection of examples of using PSL for functional and formal verification of
 
 This is a project with the purpose to get a current state of PSL implementation in GHDL. It probably will find unsupported PSL features, incorrect implemented features or simple bugs like GHDL crashs.
 
-It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a sucessful proof os simulation if you want. You can change them to see what happens. Have fun!
+It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a successful proof or simulation if you want. You can change them to see what happens. Have fun!
 
 
 The next two lists will grow during further development
@@ -22,6 +22,7 @@ The next two lists will grow during further development
 * implication operator
 * next operator
 * next[n] operator
+* next_a[i to j] operator
 * next_event operator
 * next_event[n] operator
 * until operator
@@ -31,10 +32,9 @@ The next two lists will grow during further development
 
 ## PSL features not yet supported by GHDL:
 
-* next_a[i:j] operator
-* next_e[i:j] operator
-* next_event_a[i:j] operator
-* next_event_e[i:j] operator
+* next_e[i to j] operator
+* next_event_a[i to j] operator
+* next_event_e[i to j] operator
 
 ## PSL features supported by GHDL but with wrong behaviour
 

formal/psl_next_a.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_a.vhd -e psl_next_a
+prep -top psl_next_a
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_a.vhd

formal/tests.mk

@@ -3,6 +3,7 @@ psl_always \
 psl_never \
 psl_next \
 psl_next_3 \
+psl_next_a \
 psl_next_event \
 psl_next_event_4 \
 psl_until \

src/psl_next_a.vhd

@@ -0,0 +1,49 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_next_a is
+  port (
+    clk : in std_logic
+  );
+end entity psl_next_a;
+
+
+architecture psl of psl_next_a is
+
+  signal a, b : std_logic;
+  signal c, d : std_logic;
+  signal e, f : std_logic;
+
+begin
+
+
+  --                              01234567890
+  SEQ_A : sequencer generic map ("__-_-______") port map (clk, a);
+  SEQ_B : sequencer generic map ("_____-_-___") port map (clk, b);
+
+  --                              01234567890
+  SEQ_C : sequencer generic map ("__-_-______") port map (clk, c);
+  SEQ_D : sequencer generic map ("_____-_____") port map (clk, d);
+
+  --                              01234567890
+  SEQ_E : sequencer generic map ("__-_-______") port map (clk, e);
+  SEQ_F : sequencer generic map ("_____-----_") port map (clk, f);
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion doesn't hold at cycle 6
+  NEXT_0_a : assert always (a -> next_a[3 to 5] (b));
+
+  -- This assertion doesn't hold at cycle 6
+  NEXT_1_a : assert always (c -> next_a[3 to 5] (d));
+
+  -- This assertion holds
+  NEXT_2_a : assert always (e -> next_a[3 to 5] (f));
+
+
+end architecture psl;