diff options
author | Tristan Gingold <tgingold@free.fr> | 2016-03-17 05:03:36 +0100 |
---|---|---|
committer | Tristan Gingold <tgingold@free.fr> | 2016-03-18 05:22:04 +0100 |
commit | 73a6ed8e5e982034920d8c9fe95faddefdcffa43 (patch) | |
tree | 14da67e29b2452272a908e2145e9c87df84a53ef /src | |
parent | d0b0f30b71d77e2dbf9952e9accd8e50e69fc731 (diff) | |
download | ghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.tar.gz ghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.tar.bz2 ghdl-73a6ed8e5e982034920d8c9fe95faddefdcffa43.zip |
PSL: add counters, generate rti and add --psl-report
Diffstat (limited to 'src')
-rw-r--r-- | src/grt/grt-astdio.adb | 6 | ||||
-rw-r--r-- | src/grt/grt-astdio.ads | 1 | ||||
-rw-r--r-- | src/grt/grt-disp_rti.adb | 37 | ||||
-rw-r--r-- | src/grt/grt-modules.adb | 2 | ||||
-rw-r--r-- | src/grt/grt-psl.adb | 217 | ||||
-rw-r--r-- | src/grt/grt-psl.ads | 28 | ||||
-rw-r--r-- | src/grt/grt-rtis.ads | 11 | ||||
-rw-r--r-- | src/grt/grt-rtis_utils.adb | 41 | ||||
-rw-r--r-- | src/grt/grt-rtis_utils.ads | 7 | ||||
-rw-r--r-- | src/grt/grt-types.ads | 6 | ||||
-rw-r--r-- | src/vhdl/translate/trans-chap9.adb | 37 | ||||
-rw-r--r-- | src/vhdl/translate/trans-rtis.adb | 81 | ||||
-rw-r--r-- | src/vhdl/translate/trans-rtis.ads | 1 | ||||
-rw-r--r-- | src/vhdl/translate/trans.ads | 4 |
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; |