diff options
Diffstat (limited to 'src/grt/grt-psl.adb')
-rw-r--r-- | src/grt/grt-psl.adb | 217 |
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; |