PSL: add counters, generate rti and add --psl-report

4 files changed, 66 insertions, 57 deletions

diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index fe3545463..395f3610a 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -315,14 +315,12 @@ package body Trans.Chap9 is
       New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type);
 
       --  Create the variables.
+      Info.Psl_Count_Var := Create_Var
+        (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type);
+
       Info.Psl_Vect_Var := Create_Var
         (Create_Var_Identifier ("VECT"), Info.Psl_Vect_Type);
 
-      if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Statement then
-         Info.Psl_Bool_Var := Create_Var
-           (Create_Var_Identifier ("BOOL"), Ghdl_Bool_Type);
-      end if;
-
       Pop_Instance_Factory (Info.Psl_Scope'Access);
       New_Type_Decl (Create_Identifier ("INSTTYPE"),
                      Get_Scope_Type (Info.Psl_Scope));
@@ -438,18 +436,6 @@ package body Trans.Chap9 is
       --  New state vector.
       New_Var_Decl (Var_Nvec, Wki_Res, O_Storage_Local, Info.Psl_Vect_Type);
 
-      --  For cover directive, return now if already covered.
-      case Get_Kind (Stmt) is
-         when Iir_Kind_Psl_Assert_Statement =>
-            null;
-         when Iir_Kind_Psl_Cover_Statement =>
-            Start_If_Stmt (S_Blk, New_Value (Get_Var (Info.Psl_Bool_Var)));
-            New_Return_Stmt;
-            Finish_If_Stmt (S_Blk);
-         when others =>
-            Error_Kind ("Translate_Psl_Directive_Statement(1)", Stmt);
-      end case;
-
       --  Initialize the new state vector.
       Start_Declare_Stmt;
       New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
@@ -539,11 +525,13 @@ package body Trans.Chap9 is
          when Iir_Kind_Psl_Cover_Statement =>
             Chap8.Translate_Report
               (Stmt, Ghdl_Psl_Cover, Severity_Level_Note);
-            New_Assign_Stmt (Get_Var (Info.Psl_Bool_Var),
-                             New_Lit (Ghdl_Bool_True_Node));
          when others =>
             Error_Kind ("Translate_Psl_Directive_Statement", Stmt);
       end case;
+      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var),
+                       New_Dyadic_Op (ON_Add_Ov,
+                                      New_Value (Get_Var (Info.Psl_Count_Var)),
+                                      New_Lit (Ghdl_Index_1)));
       Close_Temp;
       Finish_If_Stmt (S_Blk);
 
@@ -633,8 +621,10 @@ package body Trans.Chap9 is
 
             Start_If_Stmt
               (S_Blk,
-               New_Monadic_Op (ON_Not,
-                               New_Value (Get_Var (Info.Psl_Bool_Var))));
+               New_Compare_Op (ON_Eq,
+                               New_Value (Get_Var (Info.Psl_Count_Var)),
+                               New_Lit (Ghdl_Index_0),
+                               Ghdl_Bool_Type));
             Chap8.Translate_Report
               (Stmt, Ghdl_Psl_Cover_Failed, Severity_Level_Error);
             Finish_If_Stmt (S_Blk);
@@ -1401,10 +1391,7 @@ package body Trans.Chap9 is
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
 
-      if Info.Psl_Bool_Var /= Null_Var then
-         New_Assign_Stmt (Get_Var (Info.Psl_Bool_Var),
-                          New_Lit (Ghdl_Bool_False_Node));
-      end if;
+      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Ghdl_Index_0));
    end Elab_Psl_Directive;
 
    procedure Elab_Implicit_Guard_Signal
diff --git a/src/vhdl/translate/trans-rtis.adb b/src/vhdl/translate/trans-rtis.adb
index 8ac312fd2..ef26d17f3 100644
--- a/src/vhdl/translate/trans-rtis.adb
+++ b/src/vhdl/translate/trans-rtis.adb
@@ -309,6 +309,9 @@ package body Trans.Rtis is
          New_Enum_Literal
            (Constr, Get_Identifier ("__ghdl_rtik_psl_assert"),
             Ghdl_Rtik_Psl_Assert);
+         New_Enum_Literal
+           (Constr, Get_Identifier ("__ghdl_rtik_psl_cover"),
+            Ghdl_Rtik_Psl_Cover);
 
          New_Enum_Literal (Constr, Get_Identifier ("__ghdl_rtik_error"),
                            Ghdl_Rtik_Error);
@@ -1970,7 +1973,8 @@ package body Trans.Rtis is
             Val := Var_Acc_To_Loc (Var);
          end if;
          New_Record_Aggr_El (List, Val);
-         New_Record_Aggr_El (List, New_Rti_Address (Type_Info.Type_Rti));
+         Val := New_Rti_Address (Type_Info.Type_Rti);
+         New_Record_Aggr_El (List, Val);
          New_Record_Aggr_El (List, Generate_Linecol (Decl));
          Finish_Record_Aggr (List, Val);
          Finish_Init_Value (Rti, Val);
@@ -1978,6 +1982,50 @@ package body Trans.Rtis is
       Pop_Identifier_Prefix (Mark);
    end Generate_Object;
 
+   procedure Generate_Psl_Directive (Decl : Iir)
+   is
+      Info : constant Psl_Info_Acc := Get_Info (Decl);
+      Name : O_Dnode;
+      Kind : O_Cnode;
+      Val  : O_Cnode;
+      List : O_Record_Aggr_List;
+      Mark : Id_Mark_Type;
+      Field_Off : O_Cnode;
+   begin
+      pragma Assert (Global_Storage /= O_Storage_External);
+
+      Push_Identifier_Prefix (Mark, Get_Identifier (Decl));
+
+      New_Const_Decl (Info.Psl_Rti_Const, Create_Identifier ("RTI"),
+                      Global_Storage, Ghdl_Rtin_Object);
+
+      Name := Generate_Name (Decl);
+
+      Start_Init_Value (Info.Psl_Rti_Const);
+      Start_Record_Aggr (List, Ghdl_Rtin_Object);
+      case Get_Kind (Decl) is
+         when Iir_Kind_Psl_Cover_Statement =>
+            Kind := Ghdl_Rtik_Psl_Cover;
+         when Iir_Kind_Psl_Assert_Statement =>
+            Kind := Ghdl_Rtik_Psl_Assert;
+         when others =>
+            Error_Kind ("rti.generate_psl_directive", Decl);
+      end case;
+      New_Record_Aggr_El (List, Generate_Common (Kind));
+      New_Record_Aggr_El (List, New_Name_Address (Name));
+
+      Field_Off := Get_Scope_Offset (Info.Psl_Scope, Ghdl_Ptr_Type);
+      New_Record_Aggr_El (List, Field_Off);
+      New_Record_Aggr_El (List, New_Null_Access (Ghdl_Rti_Access));
+      New_Record_Aggr_El (List, Generate_Linecol (Decl));
+      Finish_Record_Aggr (List, Val);
+      Finish_Init_Value (Info.Psl_Rti_Const, Val);
+
+      Pop_Identifier_Prefix (Mark);
+
+      Add_Rti_Node (Info.Psl_Rti_Const);
+   end Generate_Psl_Directive;
+
    procedure Generate_Block (Blk : Iir; Parent_Rti : O_Dnode);
    procedure Generate_If_Generate_Statement (Blk : Iir; Parent_Rti : O_Dnode);
    procedure Generate_For_Generate_Statement (Blk : Iir; Parent_Rti : O_Dnode);
@@ -2149,32 +2197,6 @@ package body Trans.Rtis is
       Add_Rti_Node (Info.Block_Rti_Const);
    end Generate_Instance;
 
-   procedure Generate_Psl_Directive (Stmt : Iir)
-   is
-      Name : O_Dnode;
-      List : O_Record_Aggr_List;
-
-      Rti  : O_Dnode;
-      Res  : O_Cnode;
-      Info : constant Psl_Info_Acc := Get_Info (Stmt);
-      Mark : Id_Mark_Type;
-   begin
-      Push_Identifier_Prefix (Mark, Get_Identifier (Stmt));
-      Name := Generate_Name (Stmt);
-
-      New_Const_Decl (Rti, Create_Identifier ("RTI"),
-                      O_Storage_Public, Ghdl_Rtin_Type_Scalar);
-
-      Start_Init_Value (Rti);
-      Start_Record_Aggr (List, Ghdl_Rtin_Type_Scalar);
-      New_Record_Aggr_El (List, Generate_Common (Ghdl_Rtik_Psl_Assert));
-      New_Record_Aggr_El (List, New_Global_Address (Name, Char_Ptr_Type));
-      Finish_Record_Aggr (List, Res);
-      Finish_Init_Value (Rti, Res);
-      Info.Psl_Rti_Const := Rti;
-      Pop_Identifier_Prefix (Mark);
-   end Generate_Psl_Directive;
-
    procedure Generate_Declaration_Chain (Chain : Iir)
    is
       Decl : Iir;
@@ -2312,9 +2334,8 @@ package body Trans.Rtis is
                null;
             when Iir_Kind_Psl_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement =>
-               Generate_Psl_Directive (Stmt);
-            when Iir_Kind_Psl_Cover_Statement =>
+            when Iir_Kind_Psl_Assert_Statement
+              | Iir_Kind_Psl_Cover_Statement =>
                Generate_Psl_Directive (Stmt);
             when others =>
                Error_Kind ("rti.generate_concurrent_statement_chain", Stmt);
diff --git a/src/vhdl/translate/trans-rtis.ads b/src/vhdl/translate/trans-rtis.ads
index 06662fc6f..c272bf7e9 100644
--- a/src/vhdl/translate/trans-rtis.ads
+++ b/src/vhdl/translate/trans-rtis.ads
@@ -67,6 +67,7 @@ package Trans.Rtis is
    Ghdl_Rtik_Attribute_Quiet             : O_Cnode;
    Ghdl_Rtik_Attribute_Stable            : O_Cnode;
    Ghdl_Rtik_Psl_Assert                  : O_Cnode;
+   Ghdl_Rtik_Psl_Cover                   : O_Cnode;
    Ghdl_Rtik_Error                       : O_Cnode;
 
    --  RTI types.
diff --git a/src/vhdl/translate/trans.ads b/src/vhdl/translate/trans.ads
index e97d6a0c3..fc53a0cea 100644
--- a/src/vhdl/translate/trans.ads
+++ b/src/vhdl/translate/trans.ads
@@ -1317,8 +1317,8 @@ package Trans is
             --  State vector variable.
             Psl_Vect_Var : Var_Type;
 
-            --  Boolean variable (for cover)
-            Psl_Bool_Var : Var_Type;
+            --  Counter variable (nbr of failures or coverage)
+            Psl_Count_Var : Var_Type;
 
             --  RTI for the process.
             Psl_Rti_Const : O_Dnode := O_Dnode_Null;