-- GHDL Run Time (GRT) - PSL report. -- Copyright (C) 2016 Tristan Gingold -- -- This program 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 of the License, or -- (at your option) any later version. -- -- This program 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 this program. If not, see . -- -- 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.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_Assume_Failed : Ghdl_U32 := 0; Nbr_Assume_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; Psl_Dir : Ghdl_Rtin_Psl_Directive_Acc; Addr : System.Address; Finished_Count : Ghdl_Index_Type; Started_Count : 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_Assume => Put (F, """assumption"""); when Ghdl_Rtik_Psl_Cover => Put (F, """cover"""); end case; Put_Line (F, ","); Put (F, " ""name"": """); Psl_Dir := To_Ghdl_Rtin_Psl_Directive_Acc (Rti); Put (F, Ctxt); Put (F, '.'); Put (F, Psl_Dir.Name); Put_Line (F, ""","); Put (F, " ""file"": """); Put (F, Get_Filename (Ctxt)); Put_Line (F, ""","); Put (F, " ""line"": "); Put_U32 (F, Get_Linecol_Line (Psl_Dir.Linecol)); Put_Line (F, ","); Put (F, " ""finished-count"": "); Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc, Ctxt); 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 Finished_Count = 0 then Put (F, "passed"); Inc (Nbr_Assert_Passed); else Put (F, "failed"); Inc (Nbr_Assert_Failed); end if; when Ghdl_Rtik_Psl_Assume => if Finished_Count = 0 then Put (F, "passed"); Inc (Nbr_Assume_Passed); else Put (F, "failed"); Inc (Nbr_Assume_Failed); end if; when Ghdl_Rtik_Psl_Cover => if Finished_Count = 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_S ("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 or Status = Traverse_Skip); 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, " ""assume"": "); Put_U32 (F, Nbr_Assume_Failed + Nbr_Assume_Passed); Put_Line (F, ","); Put (F, " ""assume-failure"": "); Put_U32 (F, Nbr_Assume_Failed); Put_Line (F, ","); Put (F, " ""assume-pass"": "); Put_U32 (F, Nbr_Assume_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;