Add rose() example to formal tests after it was implemented by ghdl/ghdl#1356

README.md

@@ -61,12 +61,14 @@ The next lists will grow during further development
 ### Functions
 
 * `prev()` function (Synthesis only, see [prev() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_prev.vhd))
+* `stable()` function (Synthesis only, see [stable() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_stable.vhd))
+* `rose()` function (Synthesis only, see [rose() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_rose.vhd))
 
 ## Not yet supported by GHDL:
 
 * `forall` statement
 * Synthesis of strong operator versions
-* PSL functions (`prev()` implemented)
+* PSL functions (`prev()`, `stable()` & `rose()` are implemented for synthesis)
 
 ## Under investigation
 

formal/tests.mk

@@ -27,4 +27,5 @@ psl_sere_non_len_matching_and \
 psl_sere_concat \
 psl_sere_fusion \
 psl_prev \
-psl_stable
+psl_stable \
+psl_rose

src/psl_rose.vhd

@@ -29,6 +29,12 @@ begin
   -- This assertion holds
   ROSE_0_a : assert always (rose(a) -> b);
 
+  -- This assertion holds
+  ROSE_1_a : assert always {not a; a} |-> rose(a);
+
+  -- This assertion holds
+  ROSE_2_a : assert always (rose(a) -> (not prev(a) and a));
+
   -- Workaround needed before rose() is implemented
   -- With VHDL glue logic generating the
   -- previous value of a and simple comparing the two values
@@ -41,11 +47,11 @@ begin
         a_prev <= a;
       end if;
     end process;
-    ROSE_1_a : assert always (a and not a_prev -> b);
+    ROSE_3_a : assert always (a and not a_prev -> b);
   end block d_reg;
 
   -- Another workaround by using simple SERE concatenation on LHS
-  FELL_2_a : assert always {not a; a} |-> b;
+  ROSE_4_a : assert always {not a; a} |-> b;
 
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas