diff options
| -rw-r--r-- | src/grt/grt-psl.adb | 21 | ||||
| -rw-r--r-- | src/vhdl/translate/trans-chap7.adb | 2 | ||||
| -rw-r--r-- | src/vhdl/translate/trans-chap9.adb | 42 | ||||
| -rw-r--r-- | src/vhdl/translate/trans.ads | 10 | ||||
| -rw-r--r-- | src/vhdl/translate/translation.adb | 1 |
5 files changed, 57 insertions, 19 deletions
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb index ff736c951..b6362509c 100644 --- a/src/grt/grt-psl.adb +++ b/src/grt/grt-psl.adb @@ -75,7 +75,8 @@ package body Grt.Psl is F : constant FILEs := Report_Stream; Psl_Dir : Ghdl_Rtin_Psl_Directive_Acc; Addr : System.Address; - Val : Ghdl_Index_Type; + Finished_Count : Ghdl_Index_Type; + Started_Count : Ghdl_Index_Type; begin case Rti.Kind is when Ghdl_Rtiks_Psl => @@ -116,16 +117,22 @@ package body Grt.Psl is Put_U32 (F, Get_Linecol_Line (Psl_Dir.Linecol)); Put_Line (F, ","); - Put (F, " ""count"": "); + Put (F, " ""finished-count"": "); Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc, Ctxt); - Val := To_Ghdl_Index_Ptr (Addr).all; - Put_U32 (F, Ghdl_U32 (Val)); + 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 Val = 0 then + if Finished_Count = 0 then Put (F, "passed"); Inc (Nbr_Assert_Passed); else @@ -133,7 +140,7 @@ package body Grt.Psl is Inc (Nbr_Assert_Failed); end if; when Ghdl_Rtik_Psl_Assume => - if Val = 0 then + if Finished_Count = 0 then Put (F, "passed"); Inc (Nbr_Assume_Passed); else @@ -141,7 +148,7 @@ package body Grt.Psl is Inc (Nbr_Assume_Failed); end if; when Ghdl_Rtik_Psl_Cover => - if Val = 0 then + if Finished_Count = 0 then Put (F, "not covered"); Inc (Nbr_Cover_Failed); else diff --git a/src/vhdl/translate/trans-chap7.adb b/src/vhdl/translate/trans-chap7.adb index 369e7564d..618ca996d 100644 --- a/src/vhdl/translate/trans-chap7.adb +++ b/src/vhdl/translate/trans-chap7.adb @@ -4527,7 +4527,7 @@ package body Trans.Chap7 is declare Info : constant Psl_Info_Acc := Get_Info (Expr); begin - return New_Value (Get_Var (Info.Psl_Count_Var)); + return New_Value (Get_Var (Info.Psl_Finish_Count_Var)); end; when others => diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb index 4acb0c01f..f9d8f5054 100644 --- a/src/vhdl/translate/trans-chap9.adb +++ b/src/vhdl/translate/trans-chap9.adb @@ -342,17 +342,19 @@ package body Trans.Chap9 is New_Index_Lit (Unsigned_64 (Get_PSL_Nbr_States (Stmt)))); New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type); - -- Create the variables. + -- Create count variables if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then -- FIXME: endpoint is a variable (and not a signal). This is required -- to have the right value for the current cycle, but as a -- consequence, this process must be evaluated before using the -- endpoint. - Info.Psl_Count_Var := Create_Var + Info.Psl_Finish_Count_Var := Create_Var (Create_Var_Identifier ("ENDPOINT"), Std_Boolean_Type_Node); else - Info.Psl_Count_Var := Create_Var - (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type); + Info.Psl_Finish_Count_Var := Create_Var + (Create_Var_Identifier ("FINISH_COUNT"), Ghdl_Index_Type); + Info.Psl_Start_Count_Var := Create_Var + (Create_Var_Identifier ("START_COUNT"), Ghdl_Index_Type); end if; Info.Psl_State_Var := Create_Var @@ -530,6 +532,7 @@ package body Trans.Chap9 is Instance : O_Dnode; Var_I : O_Dnode; Var_Nvec : O_Dnode; + Var_SFlag : O_Dnode; Report_Proc : O_Dnode; Label : O_Snode; Clk_Blk : O_If_Block; @@ -595,6 +598,8 @@ package body Trans.Chap9 is New_Lit (Std_Boolean_False_Node)); Inc_Var (Var_I); Finish_Loop_Stmt (Label); + -- Flag for active edge from start state (assertion "started" flag) + New_Var_Decl (Var_SFlag, Wki_Flag, O_Storage_Local, Ghdl_Bool_Type); Finish_Declare_Stmt; -- Global 'if' statement for the clock. @@ -602,6 +607,9 @@ package body Trans.Chap9 is Start_If_Stmt (Clk_Blk, Translate_Psl_Expr (Get_PSL_Clock (Stmt), False)); + -- Default "started" flag is not set + New_Assign_Stmt (New_Obj (Var_SFlag), New_Lit (Ghdl_Bool_False_Node)); + -- Default simplified state -> Inactive New_Assign_Stmt (Get_Var (Info.Psl_State_Var), New_Lit (Trans.Rtis.Ghdl_Rti_Psl_State_Inactive)); @@ -641,10 +649,17 @@ package body Trans.Chap9 is New_Lit (D_Lit)))); Cond := New_Dyadic_Op (ON_And, Cond, Translate_Psl_Expr (Get_Edge_Expr (E), False)); + + -- If NFA edge expression is valid -> Fire-up destination state. Start_If_Stmt (E_Blk, Cond); New_Assign_Stmt (New_Indexed_Element (New_Obj (Var_Nvec), New_Lit (D_Lit)), New_Lit (Std_Boolean_True_Node)); + -- If we fire from start state -> set "started" flag. + if S = Get_First_State (NFA) then + New_Assign_Stmt (New_Obj (Var_SFlag), + New_Lit (Ghdl_Bool_True_Node)); + end if; Finish_If_Stmt (E_Blk); Close_Temp; @@ -667,7 +682,7 @@ package body Trans.Chap9 is (Unsigned_64 (S_Num))))); if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then - New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), Cond); + New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), Cond); else Start_If_Stmt (S_Blk, Cond); Open_Temp; @@ -697,14 +712,23 @@ package body Trans.Chap9 is Error_Kind ("Translate_Psl_Directive_Statement", Stmt); end case; New_Assign_Stmt - (Get_Var (Info.Psl_Count_Var), + (Get_Var (Info.Psl_Finish_Count_Var), New_Dyadic_Op (ON_Add_Ov, - New_Value (Get_Var (Info.Psl_Count_Var)), + New_Value (Get_Var (Info.Psl_Finish_Count_Var)), New_Lit (Ghdl_Index_1))); Close_Temp; Finish_If_Stmt (S_Blk); end if; + -- Check "started" flag, increment started count if set + Start_If_Stmt (S_Blk, New_Value (New_Obj (Var_SFlag))); + New_Assign_Stmt + (Get_Var (Info.Psl_Start_Count_Var), + New_Dyadic_Op (ON_Add_Ov, + New_Value (Get_Var (Info.Psl_Start_Count_Var)), + New_Lit (Ghdl_Index_1))); + Finish_If_Stmt (S_Blk); + -- Assign state vector. Start_Declare_Stmt; New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type); @@ -797,7 +821,7 @@ package body Trans.Chap9 is Start_If_Stmt (S_Blk, New_Compare_Op (ON_Eq, - New_Value (Get_Var (Info.Psl_Count_Var)), + New_Value (Get_Var (Info.Psl_Finish_Count_Var)), New_Lit (Ghdl_Index_0), Ghdl_Bool_Type)); Start_Association (Assocs, Report_Proc); @@ -1900,7 +1924,7 @@ package body Trans.Chap9 is else Init := Ghdl_Index_0; end if; - New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Init)); + New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), New_Lit (Init)); end Elab_Psl_Directive; procedure Elab_Implicit_Guard_Signal diff --git a/src/vhdl/translate/trans.ads b/src/vhdl/translate/trans.ads index 4e0b9b959..ecfc79203 100644 --- a/src/vhdl/translate/trans.ads +++ b/src/vhdl/translate/trans.ads @@ -172,6 +172,7 @@ package Trans is Wki_Base : O_Ident; Wki_Bounds : O_Ident; Wki_Locvars : O_Ident; + Wki_Flag : O_Ident; -- ALLOCATION_KIND defines the type of memory storage. -- ALLOC_STACK means the object is allocated on the local stack and @@ -1946,8 +1947,13 @@ package Trans is -- Simplified Assertion state (for dumping) Psl_State_Var : Var_Type; - -- Counter variable (nbr of failures or coverage) - Psl_Count_Var : Var_Type; + -- Number of times assertion finished + -- For cover points: Number of coveres + -- For assertions: Number of failures + Psl_Finish_Count_Var : Var_Type; + + -- Number of times assertion was started + Psl_Start_Count_Var : Var_Type; -- RTI for the process. Psl_Rti_Const : O_Dnode := O_Dnode_Null; diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb index b8d19e6ce..c02326ea8 100644 --- a/src/vhdl/translate/translation.adb +++ b/src/vhdl/translate/translation.adb @@ -416,6 +416,7 @@ package body Translation is Wki_Base := Get_Identifier ("BASE"); Wki_Bounds := Get_Identifier ("BOUNDS"); Wki_Locvars := Get_Identifier ("LOCVARS"); + Wki_Flag := Get_Identifier ("FLAG"); Sizetype := New_Unsigned_Type (32); New_Type_Decl (Get_Identifier ("__ghdl_size_type"), Sizetype); |