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

1 files changed, 217 insertions, 0 deletions

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;