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

14 files changed, 405 insertions, 74 deletions

diff --git a/src/grt/grt-astdio.adb b/src/grt/grt-astdio.adb
index 456d024ac..a572dd3cc 100644
--- a/src/grt/grt-astdio.adb
+++ b/src/grt/grt-astdio.adb
@@ -56,6 +56,12 @@ package body Grt.Astdio is
       Put (Stream, Nl);
    end New_Line;
 
+   procedure Put_Line (Stream : FILEs; Str : String) is
+   begin
+      Put (Stream, Str);
+      New_Line (Stream);
+   end Put_Line;
+
    procedure Put (Str : String)
    is
       S : size_t;
diff --git a/src/grt/grt-astdio.ads b/src/grt/grt-astdio.ads
index 8e8b739cc..c496afe07 100644
--- a/src/grt/grt-astdio.ads
+++ b/src/grt/grt-astdio.ads
@@ -31,6 +31,7 @@ package Grt.Astdio is
 
    --  Procedures to disp on STREAM.
    procedure Put (Stream : FILEs; Str : String);
+   procedure Put_Line (Stream : FILEs; Str : String);
    procedure Put_I32 (Stream : FILEs; I32 : Ghdl_I32);
    procedure Put_U32 (Stream : FILEs; U32 : Ghdl_U32);
    procedure Put_I64 (Stream : FILEs; I64 : Ghdl_I64);
diff --git a/src/grt/grt-disp_rti.adb b/src/grt/grt-disp_rti.adb
index 1e6389f0c..57f6ae146 100644
--- a/src/grt/grt-disp_rti.adb
+++ b/src/grt/grt-disp_rti.adb
@@ -22,6 +22,7 @@
 --  covered by the GNU General Public License. This exception does not
 --  however invalidate any other reasons why the executable file might be
 --  covered by the GNU Public License.
+
 with Grt.Astdio; use Grt.Astdio;
 with Grt.Errors; use Grt.Errors;
 with Grt.Hooks; use Grt.Hooks;
@@ -422,6 +423,11 @@ package body Grt.Disp_Rti is
          when Ghdl_Rtik_Unitptr =>
             Put ("ghdl_rtik_unitptr");
 
+         when Ghdl_Rtik_Psl_Assert =>
+            Put ("ghdl_rtik_psl_assert");
+         when Ghdl_Rtik_Psl_Cover =>
+            Put ("ghdl_rtik_psl_cover");
+
          when others =>
             Put ("ghdl_rtik_#");
             Put_I32 (stdout, Ghdl_Rtik'Pos (Kind));
@@ -656,15 +662,12 @@ package body Grt.Disp_Rti is
       end case;
    end Disp_Subtype_Indication;
 
-   procedure Disp_Linecol (Linecol : Ghdl_Index_Type)
-   is
-      Line : constant Ghdl_U32 := Ghdl_U32 (Linecol / 256);
-      Col : constant Ghdl_U32 := Ghdl_U32 (Linecol mod 256);
+   procedure Disp_Linecol (Linecol : Ghdl_Index_Type) is
    begin
       Put ("sloc=");
-      Put_U32 (stdout, Line);
+      Put_U32 (stdout, Get_Linecol_Line (Linecol));
       Put (":");
-      Put_U32 (stdout, Col);
+      Put_U32 (stdout, Get_Linecol_Col (Linecol));
    end Disp_Linecol;
 
    procedure Disp_Rti (Rti : Ghdl_Rti_Access;
@@ -802,6 +805,25 @@ package body Grt.Disp_Rti is
       New_Line;
    end Disp_Object;
 
+   procedure Disp_Psl_Directive (Obj : Ghdl_Rtin_Object_Acc;
+                                 Ctxt : Rti_Context;
+                                 Indent : Natural)
+   is
+      Addr : Address;
+   begin
+      Disp_Indent (Indent);
+      Disp_Kind (Obj.Common.Kind);
+      Disp_Depth (Obj.Common.Depth);
+      Put (", ");
+      Disp_Linecol (Obj.Linecol);
+      Put ("; ");
+      Disp_Name (Obj.Name);
+      Put (": count = ");
+      Addr := Loc_To_Addr (Obj.Common.Depth, Obj.Loc, Ctxt);
+      Put_U32 (stdout, Ghdl_U32 (To_Ghdl_Index_Ptr (Addr).all));
+      New_Line;
+   end Disp_Psl_Directive;
+
    procedure Disp_Attribute (Obj : Ghdl_Rtin_Object_Acc;
                              Ctxt : Rti_Context;
                              Indent : Natural)
@@ -1155,6 +1177,9 @@ package body Grt.Disp_Rti is
          when Ghdl_Rtik_Type_Protected =>
             Disp_Type_Protected
               (To_Ghdl_Rtin_Type_Scalar_Acc (Rti), Ctxt, Indent);
+         when Ghdl_Rtik_Psl_Cover
+           | Ghdl_Rtik_Psl_Assert =>
+            Disp_Psl_Directive (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent);
          when others =>
             Disp_Indent (Indent);
             Disp_Kind (Rti.Kind);
diff --git a/src/grt/grt-modules.adb b/src/grt/grt-modules.adb
index 0feb46cb1..befe77188 100644
--- a/src/grt/grt-modules.adb
+++ b/src/grt/grt-modules.adb
@@ -32,6 +32,7 @@ with Grt.Waves;
 with Grt.Vital_Annotate;
 with Grt.Disp_Tree;
 with Grt.Disp_Rti;
+with Grt.Psl;
 with Grt.Backtraces;
 
 package body Grt.Modules is
@@ -46,6 +47,7 @@ package body Grt.Modules is
       Grt.Vpi.Register;
       Grt.Vital_Annotate.Register;
       Grt.Disp_Rti.Register;
+      Grt.Psl.Register;
       Grt.Backtraces.Register;
    end Register_Modules;
 end Grt.Modules;
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
new file mode 100644
index 000000000..b7b863f11
--- /dev/null
+++ b/src/grt/grt-psl.adb
@@ -0,0 +1,217 @@
+--  GHDL Run Time (GRT) - PSL report.
+--  Copyright (C) 2016 Tristan Gingold
+--
+--  GHDL is free software; you can redistribute it and/or modify it under
+--  the terms of the GNU General Public License as published by the Free
+--  Software Foundation; either version 2, or (at your option) any later
+--  version.
+--
+--  GHDL is distributed in the hope that it will be useful, but WITHOUT ANY
+--  WARRANTY; without even the implied warranty of MERCHANTABILITY or
+--  FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+--  for more details.
+--
+--  You should have received a copy of the GNU General Public License
+--  along with GCC; see the file COPYING.  If not, write to the Free
+--  Software Foundation, 59 Temple Place - Suite 330, Boston, MA
+--  02111-1307, USA.
+--
+--  As a special exception, if other files instantiate generics from this
+--  unit, or you link this unit with other files to produce an executable,
+--  this unit does not by itself cause the resulting executable to be
+--  covered by the GNU General Public License. This exception does not
+--  however invalidate any other reasons why the executable file might be
+--  covered by the GNU Public License.
+
+with System;
+with Grt.Types; use Grt.Types;
+with Grt.Stdio; use Grt.Stdio;
+with Grt.Errors; use Grt.Errors;
+with Grt.Signals; use Grt.Signals;
+with Grt.Astdio; use Grt.Astdio;
+with Grt.Hooks; use Grt.Hooks;
+with Grt.Rtis; use Grt.Rtis;
+with Grt.Rtis_Addr; use Grt.Rtis_Addr;
+with Grt.Rtis_Utils; use Grt.Rtis_Utils;
+
+package body Grt.Psl is
+   --  Filename of the report. Last character is NUL.
+   Report_Filename : String_Access;
+   Report_Stream : FILEs;
+   Is_First : Boolean := True;
+   Nbr_Assert_Failed : Ghdl_U32 := 0;
+   Nbr_Assert_Passed : Ghdl_U32 := 0;
+   Nbr_Cover_Failed : Ghdl_U32 := 0;
+   Nbr_Cover_Passed : Ghdl_U32 := 0;
+
+   --  Return TRUE if OPT is an option for PSL.
+   function Psl_Option (Opt : String) return Boolean
+   is
+      F : constant Natural := Opt'First;
+   begin
+      if Opt'Length > 13 and then Opt (F .. F + 12) = "--psl-report=" then
+         Report_Filename := new String (1 .. Opt'Last - F - 13 + 1 + 1);
+         Report_Filename (1 .. Opt'Last - F - 13 + 1) :=
+           Opt (F + 13 .. Opt'Last);
+         Report_Filename (Report_Filename'Last) := NUL;
+         return True;
+      else
+         return False;
+      end if;
+   end Psl_Option;
+
+   procedure Psl_Help is
+   begin
+      Put_Line (" --psl-report=FILE  report psl result at end of simulation");
+   end Psl_Help;
+
+   procedure Inc (V : in out Ghdl_U32) is
+   begin
+      V := V + 1;
+   end Inc;
+
+   function Process (Ctxt : Rti_Context; Rti : Ghdl_Rti_Access)
+                    return Traverse_Result
+   is
+      F : constant FILEs := Report_Stream;
+      Obj : Ghdl_Rtin_Object_Acc;
+      Addr : System.Address;
+      Val : Ghdl_Index_Type;
+   begin
+      case Rti.Kind is
+         when Ghdl_Rtiks_Psl =>
+            null;
+         when Ghdl_Rtik_Process =>
+            return Traverse_Skip;
+         when others =>
+            return Traverse_Ok;
+      end case;
+
+      if Is_First then
+         Is_First := False;
+      else
+         Put_Line (F, ",");
+      end if;
+
+      Put (F, " { ""directive"": ");
+      case Ghdl_Rtiks_Psl (Rti.Kind) is
+         when Ghdl_Rtik_Psl_Assert =>
+            Put (F, """assertion""");
+         when Ghdl_Rtik_Psl_Cover =>
+            Put (F, """cover""");
+      end case;
+      Put_Line (F, ",");
+      Put (F, "   ""name"": """);
+      Obj := To_Ghdl_Rtin_Object_Acc (Rti);
+      Put (F, Ctxt);
+      Put (F, '.');
+      Put (F, Obj.Name);
+      Put_Line (F, """,");
+
+      Put (F, "   ""file"": """);
+      Put (F, Get_Filename (Ctxt));
+      Put_Line (F, """,");
+      Put (F, "   ""line"": ");
+      Put_U32 (F, Get_Linecol_Line (Obj.Linecol));
+      Put_Line (F, ",");
+
+      Put (F, "   ""count"": ");
+      Addr := Loc_To_Addr (Obj.Common.Depth, Obj.Loc, Ctxt);
+      Val := To_Ghdl_Index_Ptr (Addr).all;
+      Put_U32 (F, Ghdl_U32 (Val));
+      Put_Line (F, ",");
+
+      Put (F, "   ""status"": """);
+      case Rti.Kind is
+         when Ghdl_Rtik_Psl_Assert =>
+            if Val = 0 then
+               Put (F, "passed");
+               Inc (Nbr_Assert_Passed);
+            else
+               Put (F, "failed");
+               Inc (Nbr_Assert_Failed);
+            end if;
+         when Ghdl_Rtik_Psl_Cover =>
+            if Val = 0 then
+               Put (F, "not covered");
+               Inc (Nbr_Cover_Failed);
+            else
+               Put (F, "covered");
+               Inc (Nbr_Cover_Passed);
+            end if;
+         when others =>
+            raise Program_Error;
+      end case;
+      Put (F, """}");
+
+      return Traverse_Ok;
+   end Process;
+
+   function Psl_Traverse_Blocks is new Traverse_Blocks (Process);
+
+   --  Called at the end of the simulation.
+   procedure Psl_End
+   is
+      Mode : constant String := "wt" & NUL;
+      Status : Traverse_Result;
+      F : FILEs;
+   begin
+      if Report_Filename = null then
+         return;
+      end if;
+
+      F := fopen (Report_Filename.all'Address, Mode'Address);
+      if F = NULL_Stream then
+         Error_C ("cannot open ");
+         Error_E (Report_Filename (Report_Filename'First
+                                     .. Report_Filename'Last - 1));
+         return;
+      end if;
+
+      Put_Line (F, "{ ""details"" : [");
+
+      Report_Stream := F;
+      Status := Psl_Traverse_Blocks (Get_Top_Context);
+      pragma Assert (Status = Traverse_Ok);
+
+      Put_Line (F, "],");
+      Put_Line (F, " ""summary"" : {");
+
+      Put (F, "  ""assert"": ");
+      Put_U32 (F, Nbr_Assert_Failed + Nbr_Assert_Passed);
+      Put_Line (F, ",");
+      Put (F, "  ""assert-failure"": ");
+      Put_U32 (F, Nbr_Assert_Failed);
+      Put_Line (F, ",");
+      Put (F, "  ""assert-pass"": ");
+      Put_U32 (F, Nbr_Assert_Passed);
+      Put_Line (F, ",");
+
+      Put (F, "  ""cover"": ");
+      Put_U32 (F, Nbr_Cover_Failed + Nbr_Cover_Passed);
+      Put_Line (F, ",");
+      Put (F, "  ""cover-failure"": ");
+      Put_U32 (F, Nbr_Cover_Failed);
+      Put_Line (F, ",");
+      Put (F, "  ""cover-pass"": ");
+      Put_U32 (F, Nbr_Cover_Passed);
+
+      Put_Line (F, "}");
+
+      Put_Line (F, "}");
+      fclose (F);
+   end Psl_End;
+
+   Psl_Hooks : aliased constant Hooks_Type :=
+     (Desc => new String'("psl: display status of psl assertion and cover"),
+      Option => Psl_Option'Access,
+      Help => Psl_Help'Access,
+      Init => null,
+      Start => null,
+      Finish => Psl_End'Access);
+
+   procedure Register is
+   begin
+      Register_Hooks (Psl_Hooks'Access);
+   end Register;
+end Grt.Psl;
diff --git a/src/grt/grt-psl.ads b/src/grt/grt-psl.ads
new file mode 100644
index 000000000..899ce7398
--- /dev/null
+++ b/src/grt/grt-psl.ads
@@ -0,0 +1,28 @@
+--  GHDL Run Time (GRT) - PSL report.
+--  Copyright (C) 2016 Tristan Gingold
+--
+--  GHDL is free software; you can redistribute it and/or modify it under
+--  the terms of the GNU General Public License as published by the Free
+--  Software Foundation; either version 2, or (at your option) any later
+--  version.
+--
+--  GHDL is distributed in the hope that it will be useful, but WITHOUT ANY
+--  WARRANTY; without even the implied warranty of MERCHANTABILITY or
+--  FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+--  for more details.
+--
+--  You should have received a copy of the GNU General Public License
+--  along with GCC; see the file COPYING.  If not, write to the Free
+--  Software Foundation, 59 Temple Place - Suite 330, Boston, MA
+--  02111-1307, USA.
+--
+--  As a special exception, if other files instantiate generics from this
+--  unit, or you link this unit with other files to produce an executable,
+--  this unit does not by itself cause the resulting executable to be
+--  covered by the GNU General Public License. This exception does not
+--  however invalidate any other reasons why the executable file might be
+--  covered by the GNU Public License.
+
+package Grt.Psl is
+   procedure Register;
+end Grt.Psl;
diff --git a/src/grt/grt-rtis.ads b/src/grt/grt-rtis.ads
index 7a08ae0ff..06e09647c 100644
--- a/src/grt/grt-rtis.ads
+++ b/src/grt/grt-rtis.ads
@@ -55,7 +55,7 @@ package Grt.Rtis is
       Ghdl_Rtik_Generic,
       Ghdl_Rtik_Alias,
 
-      Ghdl_Rtik_Guard,
+      Ghdl_Rtik_Guard,          -- 20
       Ghdl_Rtik_Component,
       Ghdl_Rtik_Attribute,
       Ghdl_Rtik_Type_B1,        --  Enum
@@ -67,7 +67,7 @@ package Grt.Rtis is
       Ghdl_Rtik_Type_F64,
       Ghdl_Rtik_Type_P32,
 
-      Ghdl_Rtik_Type_P64,
+      Ghdl_Rtik_Type_P64,       -- 30
       Ghdl_Rtik_Type_Access,
       Ghdl_Rtik_Type_Array,
       Ghdl_Rtik_Type_Record,
@@ -79,7 +79,7 @@ package Grt.Rtis is
       Ghdl_Rtik_Subtype_Record,
       Ghdl_Rtik_Subtype_Access,
 
-      Ghdl_Rtik_Type_Protected,
+      Ghdl_Rtik_Type_Protected, -- 40
       Ghdl_Rtik_Element,
       Ghdl_Rtik_Unit64,
       Ghdl_Rtik_Unitptr,
@@ -87,9 +87,14 @@ package Grt.Rtis is
 
       Ghdl_Rtik_Attribute_Quiet,
       Ghdl_Rtik_Attribute_Stable,
+      Ghdl_Rtik_Psl_Assert,
+      Ghdl_Rtik_Psl_Cover,
       Ghdl_Rtik_Error);
    for Ghdl_Rtik'Size use 8;
 
+   subtype Ghdl_Rtiks_Psl is
+     Ghdl_Rtik range Ghdl_Rtik_Psl_Assert .. Ghdl_Rtik_Psl_Cover;
+
    type Ghdl_Rti_Depth is range 0 .. 255;
    for Ghdl_Rti_Depth'Size use 8;
 
diff --git a/src/grt/grt-rtis_utils.adb b/src/grt/grt-rtis_utils.adb
index ca158997c..1206d3f1f 100644
--- a/src/grt/grt-rtis_utils.adb
+++ b/src/grt/grt-rtis_utils.adb
@@ -99,15 +99,8 @@ package body Grt.Rtis_Utils is
                  | Ghdl_Rtik_Entity
                  | Ghdl_Rtik_Architecture =>
                   Internal_Error ("traverse_blocks");
-               when Ghdl_Rtik_Port
-                 | Ghdl_Rtik_Signal
-                 | Ghdl_Rtik_Guard
-                 | Ghdl_Rtik_Attribute_Quiet
-                 | Ghdl_Rtik_Attribute_Stable
-                 | Ghdl_Rtik_Attribute_Transaction =>
-                  Res := Process (Ctxt, Child);
                when others =>
-                  null;
+                  Res := Process (Ctxt, Child);
             end case;
             exit when Res = Traverse_Stop;
          end loop;
@@ -652,4 +645,36 @@ package body Grt.Rtis_Utils is
       Free (Rstr);
    end Put;
 
+   function Get_Linecol_Line (Linecol : Ghdl_Index_Type) return Ghdl_U32 is
+   begin
+      return Ghdl_U32 (Linecol / 256);
+   end Get_Linecol_Line;
+
+   function Get_Linecol_Col (Linecol : Ghdl_Index_Type) return Ghdl_U32 is
+   begin
+      return Ghdl_U32 (Linecol mod 256);
+   end Get_Linecol_Col;
+
+   function Get_Filename (Ctxt : Rti_Context) return Ghdl_C_String
+   is
+      C : Rti_Context;
+   begin
+      C := Ctxt;
+      loop
+         case C.Block.Kind is
+            when Ghdl_Rtik_Package
+              | Ghdl_Rtik_Package_Body
+              | Ghdl_Rtik_Architecture
+              | Ghdl_Rtik_Entity =>
+               declare
+                  Blk : constant Ghdl_Rtin_Block_Filename_Acc :=
+                    To_Ghdl_Rtin_Block_Filename_Acc (C.Block);
+               begin
+                  return Blk.Filename;
+               end;
+            when others =>
+               C := Get_Parent_Context (C);
+         end case;
+      end loop;
+   end Get_Filename;
 end Grt.Rtis_Utils;
diff --git a/src/grt/grt-rtis_utils.ads b/src/grt/grt-rtis_utils.ads
index 10c1a0f28..eecf390a2 100644
--- a/src/grt/grt-rtis_utils.ads
+++ b/src/grt/grt-rtis_utils.ads
@@ -89,4 +89,11 @@ package Grt.Rtis_Utils is
 
    --  Disp a context as a path.
    procedure Put (Stream : FILEs; Ctxt : Rti_Context);
+
+   --  Extract line and column from a linecol.
+   function Get_Linecol_Line (Linecol : Ghdl_Index_Type) return Ghdl_U32;
+   function Get_Linecol_Col (Linecol : Ghdl_Index_Type) return Ghdl_U32;
+
+   --  Return the filename in which CTXT is defined.  Used to report locations.
+   function Get_Filename (Ctxt : Rti_Context) return Ghdl_C_String;
 end Grt.Rtis_Utils;
diff --git a/src/grt/grt-types.ads b/src/grt/grt-types.ads
index acd7f0cb7..ff85c6779 100644
--- a/src/grt/grt-types.ads
+++ b/src/grt/grt-types.ads
@@ -279,6 +279,12 @@ package Grt.Types is
 
    type Ghdl_Range_Array is array (Ghdl_Index_Type range <>) of Ghdl_Range_Ptr;
 
+   --  For PSL counters.
+   type Ghdl_Index_Ptr is access all Ghdl_Index_Type;
+
+   function To_Ghdl_Index_Ptr is new Ada.Unchecked_Conversion
+     (Source => Address, Target => Ghdl_Index_Ptr);
+
    --  Mode of a signal.
    type Mode_Signal_Type is
      (Mode_Signal,
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;