aboutsummaryrefslogtreecommitdiffstats
path: root/src/grt
diff options
context:
space:
mode:
authorTristan Gingold <tgingold@free.fr>2016-03-17 05:03:36 +0100
committerTristan Gingold <tgingold@free.fr>2016-03-18 05:22:04 +0100
commit73a6ed8e5e982034920d8c9fe95faddefdcffa43 (patch)
tree14da67e29b2452272a908e2145e9c87df84a53ef /src/grt
parentd0b0f30b71d77e2dbf9952e9accd8e50e69fc731 (diff)
downloadghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.tar.gz
ghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.tar.bz2
ghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.zip
PSL: add counters, generate rti and add --psl-report
Diffstat (limited to 'src/grt')
-rw-r--r--src/grt/grt-astdio.adb6
-rw-r--r--src/grt/grt-astdio.ads1
-rw-r--r--src/grt/grt-disp_rti.adb37
-rw-r--r--src/grt/grt-modules.adb2
-rw-r--r--src/grt/grt-psl.adb217
-rw-r--r--src/grt/grt-psl.ads28
-rw-r--r--src/grt/grt-rtis.ads11
-rw-r--r--src/grt/grt-rtis_utils.adb41
-rw-r--r--src/grt/grt-rtis_utils.ads7
-rw-r--r--src/grt/grt-types.ads6
10 files changed, 339 insertions, 17 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,