Minor fixes, beauty care

* Minor fixes to README
* Add psl_before & psl_eventually to formal test list

README.md

@@ -38,4 +38,4 @@ The next two lists will grow during further development
 
 ## PSL features supported by GHDL but with wrong behaviour
 
-* before_ operator (Overlapping between left & right side not working, see psl_before.vhd)
+* before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd)

formal/tests.mk

@@ -5,4 +5,6 @@ psl_next \
 psl_next_3 \
 psl_next_event \
 psl_next_event_4 \
-psl_until
+psl_until \
+psl_before \
+psl_eventually

src/psl_before.vhd

@@ -47,9 +47,9 @@ begin
 
   -- This is flawed variant of the former assertion
   -- because even in cycle 1 the b before a property has
-  -- to hold, which is clearly what we want
+  -- to hold, which is clearly not what we want
   -- This assertion doesn't hold at cycle 1
-  -- Furthermore this assertion leads to a GHDL crash with bug report
+  -- Furthermore this assertion leads to a GHDL synthesis crash with bug report
   -- BEFORE_3_a : assert always (a -> (b before a));
 
   -- This assertion should hold but does not at cycle 3
@@ -58,7 +58,7 @@ begin
 
   -- This assertion should hold but does not at cycle 9
   -- Potential GHDL bug?
-   BEFORE_5_a : assert always (c -> next (d before_ c));
+  BEFORE_5_a : assert always (c -> next (d before_ c));
 
   -- This assertion doesn't at cycle 6
   BEFORE_6_a : assert always (e -> next (f before_ e));

src/psl_eventually.vhd

@@ -27,7 +27,8 @@ begin
   default clock is rising_edge(clk);
 
   -- This assertion holds
-  EVENTUALLY_a : assert always (a -> eventually! b);
+  -- This assertion leads to a GHDL synthesis crash with bug report
+  --EVENTUALLY_a : assert always (a -> eventually! b);
 
 
 end architecture psl;