src: Introduce two separate PSL counters (Finish and Start).

Finish counter corresponds to legacy count.
Start counter corresponds to number of times start
state is left (assertion is triggered).

5 files changed, 57 insertions, 19 deletions

diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
index ff736c951..b6362509c 100644
--- a/src/grt/grt-psl.adb
+++ b/src/grt/grt-psl.adb
@@ -75,7 +75,8 @@ package body Grt.Psl is
       F : constant FILEs := Report_Stream;
       Psl_Dir : Ghdl_Rtin_Psl_Directive_Acc;
       Addr : System.Address;
-      Val : Ghdl_Index_Type;
+      Finished_Count : Ghdl_Index_Type;
+      Started_Count : Ghdl_Index_Type;
    begin
       case Rti.Kind is
          when Ghdl_Rtiks_Psl =>
@@ -116,16 +117,22 @@ package body Grt.Psl is
       Put_U32 (F, Get_Linecol_Line (Psl_Dir.Linecol));
       Put_Line (F, ",");
 
-      Put (F, "   ""count"": ");
+      Put (F, "   ""finished-count"": ");
       Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc, Ctxt);
-      Val := To_Ghdl_Index_Ptr (Addr).all;
-      Put_U32 (F, Ghdl_U32 (Val));
+      Finished_Count := To_Ghdl_Index_Ptr (Addr).all;
+      Put_U32 (F, Ghdl_U32 (Finished_Count));
+      Put_Line (F, ",");
+
+      Put (F, "   ""started-count"": ");
+      Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc + 4, Ctxt);
+      Started_Count := To_Ghdl_Index_Ptr (Addr).all;
+      Put_U32 (F, Ghdl_U32 (Started_Count));
       Put_Line (F, ",");
 
       Put (F, "   ""status"": """);
       case Rti.Kind is
          when Ghdl_Rtik_Psl_Assert =>
-            if Val = 0 then
+            if Finished_Count = 0 then
                Put (F, "passed");
                Inc (Nbr_Assert_Passed);
             else
@@ -133,7 +140,7 @@ package body Grt.Psl is
                Inc (Nbr_Assert_Failed);
             end if;
          when Ghdl_Rtik_Psl_Assume =>
-            if Val = 0 then
+            if Finished_Count = 0 then
                Put (F, "passed");
                Inc (Nbr_Assume_Passed);
             else
@@ -141,7 +148,7 @@ package body Grt.Psl is
                Inc (Nbr_Assume_Failed);
             end if;
          when Ghdl_Rtik_Psl_Cover =>
-            if Val = 0 then
+            if Finished_Count = 0 then
                Put (F, "not covered");
                Inc (Nbr_Cover_Failed);
             else
diff --git a/src/vhdl/translate/trans-chap7.adb b/src/vhdl/translate/trans-chap7.adb
index 369e7564d..618ca996d 100644
--- a/src/vhdl/translate/trans-chap7.adb
+++ b/src/vhdl/translate/trans-chap7.adb
@@ -4527,7 +4527,7 @@ package body Trans.Chap7 is
             declare
                Info : constant Psl_Info_Acc := Get_Info (Expr);
             begin
-               return New_Value (Get_Var (Info.Psl_Count_Var));
+               return New_Value (Get_Var (Info.Psl_Finish_Count_Var));
             end;
 
          when others =>
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index 4acb0c01f..f9d8f5054 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -342,17 +342,19 @@ package body Trans.Chap9 is
          New_Index_Lit (Unsigned_64 (Get_PSL_Nbr_States (Stmt))));
       New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type);
 
-      --  Create the variables.
+      --  Create count variables
       if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
          --  FIXME: endpoint is a variable (and not a signal). This is required
          --  to have the right value for the current cycle, but as a
          --  consequence, this process must be evaluated before using the
          --  endpoint.
-         Info.Psl_Count_Var := Create_Var
+         Info.Psl_Finish_Count_Var := Create_Var
            (Create_Var_Identifier ("ENDPOINT"), Std_Boolean_Type_Node);
       else
-         Info.Psl_Count_Var := Create_Var
-           (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type);
+         Info.Psl_Finish_Count_Var := Create_Var
+           (Create_Var_Identifier ("FINISH_COUNT"), Ghdl_Index_Type);
+         Info.Psl_Start_Count_Var := Create_Var
+           (Create_Var_Identifier ("START_COUNT"), Ghdl_Index_Type);
       end if;
 
       Info.Psl_State_Var := Create_Var
@@ -530,6 +532,7 @@ package body Trans.Chap9 is
       Instance   : O_Dnode;
       Var_I      : O_Dnode;
       Var_Nvec   : O_Dnode;
+      Var_SFlag  : O_Dnode;
       Report_Proc : O_Dnode;
       Label      : O_Snode;
       Clk_Blk    : O_If_Block;
@@ -595,6 +598,8 @@ package body Trans.Chap9 is
                        New_Lit (Std_Boolean_False_Node));
       Inc_Var (Var_I);
       Finish_Loop_Stmt (Label);
+      -- Flag for active edge from start state (assertion "started" flag)
+      New_Var_Decl (Var_SFlag, Wki_Flag, O_Storage_Local, Ghdl_Bool_Type);
       Finish_Declare_Stmt;
 
       --  Global 'if' statement for the clock.
@@ -602,6 +607,9 @@ package body Trans.Chap9 is
       Start_If_Stmt (Clk_Blk,
                      Translate_Psl_Expr (Get_PSL_Clock (Stmt), False));
 
+      -- Default "started" flag is not set
+      New_Assign_Stmt (New_Obj (Var_SFlag), New_Lit (Ghdl_Bool_False_Node));
+
       -- Default simplified state -> Inactive
       New_Assign_Stmt (Get_Var (Info.Psl_State_Var),
                        New_Lit (Trans.Rtis.Ghdl_Rti_Psl_State_Inactive));
@@ -641,10 +649,17 @@ package body Trans.Chap9 is
                  New_Lit (D_Lit))));
             Cond := New_Dyadic_Op
               (ON_And, Cond, Translate_Psl_Expr (Get_Edge_Expr (E), False));
+
+            -- If NFA edge expression is valid -> Fire-up destination state.
             Start_If_Stmt (E_Blk, Cond);
             New_Assign_Stmt
               (New_Indexed_Element (New_Obj (Var_Nvec), New_Lit (D_Lit)),
                New_Lit (Std_Boolean_True_Node));
+            -- If we fire from start state -> set "started" flag.
+            if S = Get_First_State (NFA) then
+               New_Assign_Stmt (New_Obj (Var_SFlag),
+                                New_Lit (Ghdl_Bool_True_Node));
+            end if;
             Finish_If_Stmt (E_Blk);
 
             Close_Temp;
@@ -667,7 +682,7 @@ package body Trans.Chap9 is
                                          (Unsigned_64 (S_Num)))));
 
       if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
-         New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), Cond);
+         New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), Cond);
       else
          Start_If_Stmt (S_Blk, Cond);
          Open_Temp;
@@ -697,14 +712,23 @@ package body Trans.Chap9 is
                Error_Kind ("Translate_Psl_Directive_Statement", Stmt);
          end case;
          New_Assign_Stmt
-           (Get_Var (Info.Psl_Count_Var),
+           (Get_Var (Info.Psl_Finish_Count_Var),
             New_Dyadic_Op (ON_Add_Ov,
-                           New_Value (Get_Var (Info.Psl_Count_Var)),
+                           New_Value (Get_Var (Info.Psl_Finish_Count_Var)),
                            New_Lit (Ghdl_Index_1)));
          Close_Temp;
          Finish_If_Stmt (S_Blk);
       end if;
 
+      -- Check "started" flag, increment started count if set
+      Start_If_Stmt (S_Blk, New_Value (New_Obj (Var_SFlag)));
+      New_Assign_Stmt
+           (Get_Var (Info.Psl_Start_Count_Var),
+            New_Dyadic_Op (ON_Add_Ov,
+                           New_Value (Get_Var (Info.Psl_Start_Count_Var)),
+                           New_Lit (Ghdl_Index_1)));
+      Finish_If_Stmt (S_Blk);
+
       --  Assign state vector.
       Start_Declare_Stmt;
       New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
@@ -797,7 +821,7 @@ package body Trans.Chap9 is
             Start_If_Stmt
               (S_Blk,
                New_Compare_Op (ON_Eq,
-                               New_Value (Get_Var (Info.Psl_Count_Var)),
+                               New_Value (Get_Var (Info.Psl_Finish_Count_Var)),
                                New_Lit (Ghdl_Index_0),
                                Ghdl_Bool_Type));
             Start_Association (Assocs, Report_Proc);
@@ -1900,7 +1924,7 @@ package body Trans.Chap9 is
       else
          Init := Ghdl_Index_0;
       end if;
-      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Init));
+      New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), New_Lit (Init));
    end Elab_Psl_Directive;
 
    procedure Elab_Implicit_Guard_Signal
diff --git a/src/vhdl/translate/trans.ads b/src/vhdl/translate/trans.ads
index 4e0b9b959..ecfc79203 100644
--- a/src/vhdl/translate/trans.ads
+++ b/src/vhdl/translate/trans.ads
@@ -172,6 +172,7 @@ package Trans is
    Wki_Base          : O_Ident;
    Wki_Bounds        : O_Ident;
    Wki_Locvars       : O_Ident;
+   Wki_Flag          : O_Ident;
 
    --  ALLOCATION_KIND defines the type of memory storage.
    --  ALLOC_STACK means the object is allocated on the local stack and
@@ -1946,8 +1947,13 @@ package Trans is
             --  Simplified Assertion state (for dumping)
             Psl_State_Var : Var_Type;
 
-            --  Counter variable (nbr of failures or coverage)
-            Psl_Count_Var : Var_Type;
+            --  Number of times assertion finished
+            --  For cover points: Number of coveres
+            --  For assertions: Number of failures
+            Psl_Finish_Count_Var : Var_Type;
+
+            -- Number of times assertion was started
+            Psl_Start_Count_Var : Var_Type;
 
             --  RTI for the process.
             Psl_Rti_Const : O_Dnode := O_Dnode_Null;
diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb
index b8d19e6ce..c02326ea8 100644
--- a/src/vhdl/translate/translation.adb
+++ b/src/vhdl/translate/translation.adb
@@ -416,6 +416,7 @@ package body Translation is
       Wki_Base := Get_Identifier ("BASE");
       Wki_Bounds := Get_Identifier ("BOUNDS");
       Wki_Locvars := Get_Identifier ("LOCVARS");
+      Wki_Flag := Get_Identifier ("FLAG");
 
       Sizetype := New_Unsigned_Type (32);
       New_Type_Decl (Get_Identifier ("__ghdl_size_type"), Sizetype);