diff options
36 files changed, 555 insertions, 251 deletions
diff --git a/python/libghdl/thin/vhdl/nodes.py b/python/libghdl/thin/vhdl/nodes.py index 26b1a6f86..05782b97f 100644 --- a/python/libghdl/thin/vhdl/nodes.py +++ b/python/libghdl/thin/vhdl/nodes.py @@ -198,91 +198,92 @@ class Iir_Kind: Concurrent_Selected_Signal_Assignment = 183 Concurrent_Assertion_Statement = 184 Concurrent_Procedure_Call_Statement = 185 - Psl_Assert_Statement = 186 - Psl_Cover_Directive = 187 - Psl_Restrict_Directive = 188 - Block_Statement = 189 - If_Generate_Statement = 190 - Case_Generate_Statement = 191 - For_Generate_Statement = 192 - Component_Instantiation_Statement = 193 - Psl_Default_Clock = 194 - Simple_Simultaneous_Statement = 195 - Generate_Statement_Body = 196 - If_Generate_Else_Clause = 197 - Simple_Signal_Assignment_Statement = 198 - Conditional_Signal_Assignment_Statement = 199 - Selected_Waveform_Assignment_Statement = 200 - Null_Statement = 201 - Assertion_Statement = 202 - Report_Statement = 203 - Wait_Statement = 204 - Variable_Assignment_Statement = 205 - Conditional_Variable_Assignment_Statement = 206 - Return_Statement = 207 - For_Loop_Statement = 208 - While_Loop_Statement = 209 - Next_Statement = 210 - Exit_Statement = 211 - Case_Statement = 212 - Procedure_Call_Statement = 213 - If_Statement = 214 - Elsif = 215 - Character_Literal = 216 - Simple_Name = 217 - Selected_Name = 218 - Operator_Symbol = 219 - Reference_Name = 220 - External_Constant_Name = 221 - External_Signal_Name = 222 - External_Variable_Name = 223 - Selected_By_All_Name = 224 - Parenthesis_Name = 225 - Package_Pathname = 226 - Absolute_Pathname = 227 - Relative_Pathname = 228 - Pathname_Element = 229 - Base_Attribute = 230 - Subtype_Attribute = 231 - Element_Attribute = 232 - Left_Type_Attribute = 233 - Right_Type_Attribute = 234 - High_Type_Attribute = 235 - Low_Type_Attribute = 236 - Ascending_Type_Attribute = 237 - Image_Attribute = 238 - Value_Attribute = 239 - Pos_Attribute = 240 - Val_Attribute = 241 - Succ_Attribute = 242 - Pred_Attribute = 243 - Leftof_Attribute = 244 - Rightof_Attribute = 245 - Delayed_Attribute = 246 - Stable_Attribute = 247 - Quiet_Attribute = 248 - Transaction_Attribute = 249 - Event_Attribute = 250 - Active_Attribute = 251 - Last_Event_Attribute = 252 - Last_Active_Attribute = 253 - Last_Value_Attribute = 254 - Driving_Attribute = 255 - Driving_Value_Attribute = 256 - Behavior_Attribute = 257 - Structure_Attribute = 258 - Simple_Name_Attribute = 259 - Instance_Name_Attribute = 260 - Path_Name_Attribute = 261 - Left_Array_Attribute = 262 - Right_Array_Attribute = 263 - High_Array_Attribute = 264 - Low_Array_Attribute = 265 - Length_Array_Attribute = 266 - Ascending_Array_Attribute = 267 - Range_Array_Attribute = 268 - Reverse_Range_Array_Attribute = 269 - Attribute_Name = 270 + Psl_Assert_Directive = 186 + Psl_Assume_Directive = 187 + Psl_Cover_Directive = 188 + Psl_Restrict_Directive = 189 + Block_Statement = 190 + If_Generate_Statement = 191 + Case_Generate_Statement = 192 + For_Generate_Statement = 193 + Component_Instantiation_Statement = 194 + Psl_Default_Clock = 195 + Simple_Simultaneous_Statement = 196 + Generate_Statement_Body = 197 + If_Generate_Else_Clause = 198 + Simple_Signal_Assignment_Statement = 199 + Conditional_Signal_Assignment_Statement = 200 + Selected_Waveform_Assignment_Statement = 201 + Null_Statement = 202 + Assertion_Statement = 203 + Report_Statement = 204 + Wait_Statement = 205 + Variable_Assignment_Statement = 206 + Conditional_Variable_Assignment_Statement = 207 + Return_Statement = 208 + For_Loop_Statement = 209 + While_Loop_Statement = 210 + Next_Statement = 211 + Exit_Statement = 212 + Case_Statement = 213 + Procedure_Call_Statement = 214 + If_Statement = 215 + Elsif = 216 + Character_Literal = 217 + Simple_Name = 218 + Selected_Name = 219 + Operator_Symbol = 220 + Reference_Name = 221 + External_Constant_Name = 222 + External_Signal_Name = 223 + External_Variable_Name = 224 + Selected_By_All_Name = 225 + Parenthesis_Name = 226 + Package_Pathname = 227 + Absolute_Pathname = 228 + Relative_Pathname = 229 + Pathname_Element = 230 + Base_Attribute = 231 + Subtype_Attribute = 232 + Element_Attribute = 233 + Left_Type_Attribute = 234 + Right_Type_Attribute = 235 + High_Type_Attribute = 236 + Low_Type_Attribute = 237 + Ascending_Type_Attribute = 238 + Image_Attribute = 239 + Value_Attribute = 240 + Pos_Attribute = 241 + Val_Attribute = 242 + Succ_Attribute = 243 + Pred_Attribute = 244 + Leftof_Attribute = 245 + Rightof_Attribute = 246 + Delayed_Attribute = 247 + Stable_Attribute = 248 + Quiet_Attribute = 249 + Transaction_Attribute = 250 + Event_Attribute = 251 + Active_Attribute = 252 + Last_Event_Attribute = 253 + Last_Active_Attribute = 254 + Last_Value_Attribute = 255 + Driving_Attribute = 256 + Driving_Value_Attribute = 257 + Behavior_Attribute = 258 + Structure_Attribute = 259 + Simple_Name_Attribute = 260 + Instance_Name_Attribute = 261 + Path_Name_Attribute = 262 + Left_Array_Attribute = 263 + Right_Array_Attribute = 264 + High_Array_Attribute = 265 + Low_Array_Attribute = 266 + Length_Array_Attribute = 267 + Ascending_Array_Attribute = 268 + Range_Array_Attribute = 269 + Reverse_Range_Array_Attribute = 270 + Attribute_Name = 271 class Iir_Kinds: @@ -457,7 +458,8 @@ class Iir_Kinds: Iir_Kind.Concurrent_Selected_Signal_Assignment, Iir_Kind.Concurrent_Assertion_Statement, Iir_Kind.Concurrent_Procedure_Call_Statement, - Iir_Kind.Psl_Assert_Statement, + Iir_Kind.Psl_Assert_Directive, + Iir_Kind.Psl_Assume_Directive, Iir_Kind.Psl_Cover_Directive, Iir_Kind.Psl_Restrict_Directive] @@ -649,7 +651,8 @@ class Iir_Kinds: Iir_Kind.Concurrent_Selected_Signal_Assignment, Iir_Kind.Concurrent_Assertion_Statement, Iir_Kind.Concurrent_Procedure_Call_Statement, - Iir_Kind.Psl_Assert_Statement, + Iir_Kind.Psl_Assert_Directive, + Iir_Kind.Psl_Assume_Directive, Iir_Kind.Psl_Cover_Directive, Iir_Kind.Psl_Restrict_Directive, Iir_Kind.Block_Statement, @@ -1129,6 +1132,9 @@ class Iir_Predefined: Ieee_Std_Logic_Unsigned_Eq_Slv_Slv = 265 Ieee_Std_Logic_Unsigned_Eq_Slv_Int = 266 Ieee_Std_Logic_Unsigned_Eq_Int_Slv = 267 + Ieee_Std_Logic_Unsigned_Ne_Slv_Slv = 268 + Ieee_Std_Logic_Unsigned_Ne_Slv_Int = 269 + Ieee_Std_Logic_Unsigned_Ne_Int_Slv = 270 Get_Kind = libghdl.vhdl__nodes__get_kind Get_Location = libghdl.vhdl__nodes__get_location diff --git a/python/libghdl/thin/vhdl/tokens.py b/python/libghdl/thin/vhdl/tokens.py index 20cf3b7dd..2d5655001 100644 --- a/python/libghdl/thin/vhdl/tokens.py +++ b/python/libghdl/thin/vhdl/tokens.py @@ -180,26 +180,27 @@ class Tok: Psl_Property = 176 Psl_Sequence = 177 Psl_Endpoint = 178 - Psl_Cover = 179 - Psl_Restrict = 180 - Psl_Restrict_Guarantee = 181 - Psl_Const = 182 - Psl_Boolean = 183 - Inf = 184 - Within = 185 - Abort = 186 - Before = 187 - Before_Em = 188 - Before_Un = 189 - Before_Em_Un = 190 - Until_Em = 191 - Until_Un = 192 - Until_Em_Un = 193 - Always = 194 - Never = 195 - Eventually = 196 - Next_A = 197 - Next_E = 198 - Next_Event = 199 - Next_Event_A = 200 - Next_Event_E = 201 + Psl_Assume = 179 + Psl_Cover = 180 + Psl_Restrict = 181 + Psl_Restrict_Guarantee = 182 + Psl_Const = 183 + Psl_Boolean = 184 + Inf = 185 + Within = 186 + Abort = 187 + Before = 188 + Before_Em = 189 + Before_Un = 190 + Before_Em_Un = 191 + Until_Em = 192 + Until_Un = 193 + Until_Em_Un = 194 + Always = 195 + Never = 196 + Eventually = 197 + Next_A = 198 + Next_E = 199 + Next_Event = 200 + Next_Event_A = 201 + Next_Event_E = 202 diff --git a/src/ghdldrv/ghdlprint.adb b/src/ghdldrv/ghdlprint.adb index 6c5cd5873..a611f07e7 100644 --- a/src/ghdldrv/ghdlprint.adb +++ b/src/ghdldrv/ghdlprint.adb @@ -395,6 +395,7 @@ package body Ghdlprint is | Tok_Psl_Property | Tok_Psl_Sequence | Tok_Psl_Endpoint + | Tok_Psl_Assume | Tok_Psl_Cover | Tok_Psl_Restrict | Tok_Psl_Restrict_Guarantee diff --git a/src/ghdldrv/ghdlrun.adb b/src/ghdldrv/ghdlrun.adb index f82de30e0..46445b135 100644 --- a/src/ghdldrv/ghdlrun.adb +++ b/src/ghdldrv/ghdlrun.adb @@ -341,6 +341,8 @@ package body Ghdlrun is Grt.Lib.Ghdl_Ieee_Assert_Failed'Address); Def (Trans_Decls.Ghdl_Psl_Assert_Failed, Grt.Lib.Ghdl_Psl_Assert_Failed'Address); + Def (Trans_Decls.Ghdl_Psl_Assume_Failed, + Grt.Lib.Ghdl_Psl_Assume_Failed'Address); Def (Trans_Decls.Ghdl_Psl_Cover, Grt.Lib.Ghdl_Psl_Cover'Address); Def (Trans_Decls.Ghdl_Psl_Cover_Failed, diff --git a/src/grt/grt-disp_rti.adb b/src/grt/grt-disp_rti.adb index b3b595668..b908a3c3b 100644 --- a/src/grt/grt-disp_rti.adb +++ b/src/grt/grt-disp_rti.adb @@ -470,6 +470,8 @@ package body Grt.Disp_Rti is when Ghdl_Rtik_Psl_Assert => Put ("ghdl_rtik_psl_assert"); + when Ghdl_Rtik_Psl_Assume => + Put ("ghdl_rtik_psl_assume"); when Ghdl_Rtik_Psl_Cover => Put ("ghdl_rtik_psl_cover"); when Ghdl_Rtik_Psl_Endpoint => @@ -1310,6 +1312,7 @@ package body Grt.Disp_Rti is Disp_Type_Protected (To_Ghdl_Rtin_Type_Scalar_Acc (Rti), Ctxt, Indent); when Ghdl_Rtik_Psl_Cover + | Ghdl_Rtik_Psl_Assume | Ghdl_Rtik_Psl_Assert => Disp_Psl_Directive (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent); when Ghdl_Rtik_Psl_Endpoint => diff --git a/src/grt/grt-lib.adb b/src/grt/grt-lib.adb index 26491a7ad..149f218eb 100644 --- a/src/grt/grt-lib.adb +++ b/src/grt/grt-lib.adb @@ -116,6 +116,12 @@ package body Grt.Lib is Do_Report ("psl assertion", Str, "Assertion violation", Severity, Loc); end Ghdl_Psl_Assert_Failed; + procedure Ghdl_Psl_Assume_Failed + (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is + begin + Do_Report ("psl assumption", Str, "Assumption violation", Severity, Loc); + end Ghdl_Psl_Assume_Failed; + procedure Ghdl_Psl_Cover (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is begin diff --git a/src/grt/grt-lib.ads b/src/grt/grt-lib.ads index 167ea98e5..1f5e020d4 100644 --- a/src/grt/grt-lib.ads +++ b/src/grt/grt-lib.ads @@ -40,6 +40,11 @@ package Grt.Lib is Severity : Integer; Loc : Ghdl_Location_Ptr); + procedure Ghdl_Psl_Assume_Failed + (Str : Std_String_Ptr; + Severity : Integer; + Loc : Ghdl_Location_Ptr); + -- Called when a sequence is covered (in a cover directive) procedure Ghdl_Psl_Cover (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr); @@ -116,6 +121,7 @@ private pragma Export (C, Ghdl_Assert_Failed, "__ghdl_assert_failed"); pragma Export (C, Ghdl_Ieee_Assert_Failed, "__ghdl_ieee_assert_failed"); + pragma Export (C, Ghdl_Psl_Assume_Failed, "__ghdl_psl_assume_failed"); pragma Export (C, Ghdl_Psl_Assert_Failed, "__ghdl_psl_assert_failed"); pragma Export (C, Ghdl_Psl_Cover, "__ghdl_psl_cover"); pragma Export (C, Ghdl_Psl_Cover_Failed, "__ghdl_psl_cover_failed"); diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb index cf603a097..1fd3ad94f 100644 --- a/src/grt/grt-psl.adb +++ b/src/grt/grt-psl.adb @@ -40,6 +40,8 @@ package body Grt.Psl is 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; @@ -96,6 +98,8 @@ package body Grt.Psl is 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; @@ -130,6 +134,14 @@ package body Grt.Psl is Put (F, "failed"); Inc (Nbr_Assert_Failed); end if; + when Ghdl_Rtik_Psl_Assume => + if Val = 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 Val = 0 then Put (F, "not covered"); @@ -186,6 +198,16 @@ package body Grt.Psl is 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, ","); diff --git a/src/grt/grt-rtis.ads b/src/grt/grt-rtis.ads index 030cd7e04..d4664492f 100644 --- a/src/grt/grt-rtis.ads +++ b/src/grt/grt-rtis.ads @@ -94,6 +94,7 @@ package Grt.Rtis is Ghdl_Rtik_Attribute_Stable, Ghdl_Rtik_Psl_Assert, + Ghdl_Rtik_Psl_Assume, Ghdl_Rtik_Psl_Cover, Ghdl_Rtik_Psl_Endpoint, diff --git a/src/vhdl/simulate/simul-elaboration.adb b/src/vhdl/simulate/simul-elaboration.adb index 61048392b..f165662c2 100644 --- a/src/vhdl/simulate/simul-elaboration.adb +++ b/src/vhdl/simulate/simul-elaboration.adb @@ -1897,7 +1897,8 @@ package body Simul.Elaboration is null; when Iir_Kind_Psl_Cover_Directive - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Endpoint_Declaration => Elaborate_Psl_Directive (Instance, Stmt); diff --git a/src/vhdl/simulate/simul-simulation-main.adb b/src/vhdl/simulate/simul-simulation-main.adb index 5af8acb55..d6c6ba0ff 100644 --- a/src/vhdl/simulate/simul-simulation-main.adb +++ b/src/vhdl/simulate/simul-simulation-main.adb @@ -477,12 +477,18 @@ package body Simul.Simulation.Main is S_Num := Get_State_Label (S); pragma Assert (S_Num = Get_PSL_Nbr_States (E.Stmt) - 1); case Get_Kind (E.Stmt) is - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assume_Directive => if Nvec (S_Num) then Execute_Failed_Assertion (E.Instance, "psl assertion", E.Stmt, "assertion violation", 2); end if; + when Iir_Kind_Psl_Assume_Directive => + if Nvec (S_Num) then + Execute_Failed_Assertion + (E.Instance, "psl assumption", E.Stmt, + "assumption violation", 2); + end if; when Iir_Kind_Psl_Cover_Directive => if Nvec (S_Num) then if Get_Report_Expression (E.Stmt) /= Null_Iir then @@ -563,7 +569,8 @@ package body Simul.Simulation.Main is (E.Instance, Get_PSL_Clock_Sensitivity (E.Stmt)); case Get_Kind (E.Stmt) is - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive => if Get_PSL_EOS_Flag (E.Stmt) then Grt.Processes.Ghdl_Finalize_Register (To_Instance_Acc (E'Address), diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb index b70a673a5..7a2033624 100644 --- a/src/vhdl/translate/trans-chap9.adb +++ b/src/vhdl/translate/trans-chap9.adb @@ -644,9 +644,12 @@ package body Trans.Chap9 is Start_If_Stmt (S_Blk, Cond); Open_Temp; case Get_Kind (Stmt) is - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive => Chap8.Translate_Report (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error); + when Iir_Kind_Psl_Assume_Directive => + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error); when Iir_Kind_Psl_Cover_Directive => if Get_Report_Expression (Stmt) /= Null_Iir then Start_Association (Assocs, Report_Proc); @@ -697,7 +700,8 @@ package body Trans.Chap9 is -- The finalizer. case Get_Kind (Stmt) is - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive => if Get_PSL_EOS_Flag (Stmt) then Create_Psl_Final_Proc (Stmt, Base, Instance); @@ -724,8 +728,13 @@ package body Trans.Chap9 is (ON_And, Cond, Translate_Psl_Expr (Get_Edge_Expr (E), True)); Start_If_Stmt (E_Blk, Cond); - Chap8.Translate_Report - (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error); + if Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive then + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error); + else + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error); + end if; New_Return_Stmt; Finish_If_Stmt (E_Blk); @@ -974,7 +983,8 @@ package body Trans.Chap9 is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => Translate_Psl_Directive_Declarations (El); @@ -1122,7 +1132,8 @@ package body Trans.Chap9 is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => Translate_Psl_Directive_Statement (Stmt, Base_Info); @@ -2721,7 +2732,8 @@ package body Trans.Chap9 is when Iir_Kind_Psl_Declaration | Iir_Kind_Psl_Endpoint_Declaration => null; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive => null; when Iir_Kind_Component_Instantiation_Statement => @@ -2783,7 +2795,8 @@ package body Trans.Chap9 is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => Elab_Psl_Directive (Stmt, Base_Info); diff --git a/src/vhdl/translate/trans-rtis.adb b/src/vhdl/translate/trans-rtis.adb index 96aacb8b0..e618aeb9b 100644 --- a/src/vhdl/translate/trans-rtis.adb +++ b/src/vhdl/translate/trans-rtis.adb @@ -322,6 +322,9 @@ package body Trans.Rtis is (Constr, Get_Identifier ("__ghdl_rtik_psl_assert"), Ghdl_Rtik_Psl_Assert); New_Enum_Literal + (Constr, Get_Identifier ("__ghdl_rtik_psl_assume"), + Ghdl_Rtik_Psl_Assume); + New_Enum_Literal (Constr, Get_Identifier ("__ghdl_rtik_psl_cover"), Ghdl_Rtik_Psl_Cover); New_Enum_Literal @@ -2042,8 +2045,10 @@ package body Trans.Rtis is case Get_Kind (Decl) is when Iir_Kind_Psl_Cover_Directive => Kind := Ghdl_Rtik_Psl_Cover; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive => Kind := Ghdl_Rtik_Psl_Assert; + when Iir_Kind_Psl_Assume_Directive => + Kind := Ghdl_Rtik_Psl_Assume; when Iir_Kind_Psl_Endpoint_Declaration => Kind := Ghdl_Rtik_Psl_Endpoint; when others => @@ -2422,7 +2427,8 @@ package body Trans.Rtis is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => Generate_Psl_Directive (Stmt); @@ -2994,7 +3000,8 @@ package body Trans.Rtis is when Iir_Kind_Process_Statement | Iir_Kind_Sensitized_Process_Statement => return Node_Info.Process_Rti_Const; - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => return Node_Info.Psl_Rti_Const; @@ -3035,7 +3042,8 @@ package body Trans.Rtis is when Iir_Kind_Process_Statement | Iir_Kind_Sensitized_Process_Statement => Ref := Get_Instance_Ref (Node_Info.Process_Scope); - when Iir_Kind_Psl_Assert_Statement + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Endpoint_Declaration => Ref := Get_Instance_Ref (Node_Info.Psl_Scope); diff --git a/src/vhdl/translate/trans-rtis.ads b/src/vhdl/translate/trans-rtis.ads index e3c8c188e..1e4dd36ef 100644 --- a/src/vhdl/translate/trans-rtis.ads +++ b/src/vhdl/translate/trans-rtis.ads @@ -70,6 +70,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_Assume : O_Cnode; Ghdl_Rtik_Psl_Cover : O_Cnode; Ghdl_Rtik_Psl_Endpoint : O_Cnode; Ghdl_Rtik_Error : O_Cnode; diff --git a/src/vhdl/translate/trans_decls.ads b/src/vhdl/translate/trans_decls.ads index 38d3be7e7..d76b1b896 100644 --- a/src/vhdl/translate/trans_decls.ads +++ b/src/vhdl/translate/trans_decls.ads @@ -25,6 +25,7 @@ package Trans_Decls is Ghdl_Check_Stack_Allocation : O_Dnode; + Ghdl_Psl_Assume_Failed : O_Dnode; Ghdl_Psl_Cover : O_Dnode; Ghdl_Psl_Cover_Failed : O_Dnode; -- Procedure for report statement. diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb index de83ba132..863acd37d 100644 --- a/src/vhdl/translate/translation.adb +++ b/src/vhdl/translate/translation.adb @@ -1077,6 +1077,8 @@ package body Translation is ("__ghdl_ieee_assert_failed", Ghdl_Ieee_Assert_Failed); Create_Report_Subprg ("__ghdl_psl_assert_failed", Ghdl_Psl_Assert_Failed); + Create_Report_Subprg ("__ghdl_psl_assume_failed", + Ghdl_Psl_Assume_Failed); Create_Report_Subprg ("__ghdl_psl_cover", Ghdl_Psl_Cover); Create_Report_Subprg ("__ghdl_psl_cover_failed", Ghdl_Psl_Cover_Failed); diff --git a/src/vhdl/vhdl-annotations.adb b/src/vhdl/vhdl-annotations.adb index cb44f98f0..7e2d19a58 100644 --- a/src/vhdl/vhdl-annotations.adb +++ b/src/vhdl/vhdl-annotations.adb @@ -1083,7 +1083,8 @@ package body Vhdl.Annotations is null; when Iir_Kind_Psl_Cover_Directive - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Restrict_Directive => null; when Iir_Kind_Psl_Endpoint_Declaration => diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb index 4dbb03c4c..6dd40560b 100644 --- a/src/vhdl/vhdl-canon.adb +++ b/src/vhdl/vhdl-canon.adb @@ -2125,7 +2125,8 @@ package body Vhdl.Canon is (Top, Get_Generate_Statement_Body (El)); end; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive=> declare Prop : PSL_Node; Fa : PSL_NFA; diff --git a/src/vhdl/vhdl-elocations.adb b/src/vhdl/vhdl-elocations.adb index c4dd2f1b6..6965457d6 100644 --- a/src/vhdl/vhdl-elocations.adb +++ b/src/vhdl/vhdl-elocations.adb @@ -342,7 +342,8 @@ package body Vhdl.Elocations is | Iir_Kind_Psl_Expression | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Case_Generate_Statement diff --git a/src/vhdl/vhdl-elocations.ads b/src/vhdl/vhdl-elocations.ads index 286ba751c..84be78e93 100644 --- a/src/vhdl/vhdl-elocations.ads +++ b/src/vhdl/vhdl-elocations.ads @@ -404,7 +404,8 @@ package Vhdl.Elocations is -- Iir_Kind_Psl_Default_Clock (None) - -- Iir_Kind_Psl_Assert_Statement (None) + -- Iir_Kind_Psl_Assert_Directive (None) + -- Iir_Kind_Psl_Assume_Directive (None) -- Iir_Kind_Psl_Cover_Directive (None) -- Iir_Kind_Psl_Restrict_Directive (None) diff --git a/src/vhdl/vhdl-errors.adb b/src/vhdl/vhdl-errors.adb index 57be65311..ada8258af 100644 --- a/src/vhdl/vhdl-errors.adb +++ b/src/vhdl/vhdl-errors.adb @@ -687,8 +687,10 @@ package body Vhdl.Errors is (Node, "concurrent selected signal assignment"); when Iir_Kind_Concurrent_Assertion_Statement => return Disp_Label (Node, "concurrent assertion"); - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive => return Disp_Label (Node, "PSL assertion"); + when Iir_Kind_Psl_Assume_Directive => + return Disp_Label (Node, "PSL assumption"); when Iir_Kind_Psl_Cover_Directive => return Disp_Label (Node, "PSL cover"); when Iir_Kind_Psl_Restrict_Directive => diff --git a/src/vhdl/vhdl-nodes.adb b/src/vhdl/vhdl-nodes.adb index dfb9629af..780f13b5b 100644 --- a/src/vhdl/vhdl-nodes.adb +++ b/src/vhdl/vhdl-nodes.adb @@ -1235,7 +1235,8 @@ package body Vhdl.Nodes is | Iir_Kind_Concurrent_Simple_Signal_Assignment | Iir_Kind_Concurrent_Conditional_Signal_Assignment | Iir_Kind_Concurrent_Selected_Signal_Assignment - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement diff --git a/src/vhdl/vhdl-nodes.ads b/src/vhdl/vhdl-nodes.ads index a884f7b9d..58dce712a 100644 --- a/src/vhdl/vhdl-nodes.ads +++ b/src/vhdl/vhdl-nodes.ads @@ -2902,12 +2902,16 @@ package Vhdl.Nodes is -- Get/Set_Label (Field3) -- Get/Set_Identifier (Alias Field3) - -- Iir_Kind_Psl_Assert_Statement (Medium) + -- Iir_Kind_Psl_Assert_Directive (Medium) + -- Iir_Kind_Psl_Assume_Directive (Medium) -- Iir_Kind_Psl_Cover_Directive (Medium) -- -- Get/Set_Parent (Field0) -- - -- Only for Iir_Kind_Psl_Assert_Statement: + -- Only for Iir_Kind_Psl_Assert_Directive: + -- Get/Set_Psl_Property (Field1) + -- + -- Only for Iir_Kind_Psl_Assume_Directive: -- Get/Set_Psl_Property (Field1) -- -- Only for Iir_Kind_Psl_Cover_Directive: @@ -4377,7 +4381,8 @@ package Vhdl.Nodes is Iir_Kind_Concurrent_Selected_Signal_Assignment, Iir_Kind_Concurrent_Assertion_Statement, Iir_Kind_Concurrent_Procedure_Call_Statement, - Iir_Kind_Psl_Assert_Statement, + Iir_Kind_Psl_Assert_Directive, + Iir_Kind_Psl_Assume_Directive, Iir_Kind_Psl_Cover_Directive, Iir_Kind_Psl_Restrict_Directive, Iir_Kind_Block_Statement, @@ -5569,7 +5574,8 @@ package Vhdl.Nodes is --Iir_Kind_Concurrent_Selected_Signal_Assignment --Iir_Kind_Concurrent_Assertion_Statement --Iir_Kind_Concurrent_Procedure_Call_Statement - --Iir_Kind_Psl_Assert_Statement + --Iir_Kind_Psl_Assert_Directive + --Iir_Kind_Psl_Assume_Directive --Iir_Kind_Psl_Cover_Directive --Iir_Kind_Psl_Restrict_Directive --Iir_Kind_Block_Statement @@ -5587,7 +5593,8 @@ package Vhdl.Nodes is --Iir_Kind_Concurrent_Selected_Signal_Assignment --Iir_Kind_Concurrent_Assertion_Statement --Iir_Kind_Concurrent_Procedure_Call_Statement - --Iir_Kind_Psl_Assert_Statement + --Iir_Kind_Psl_Assert_Directive + --Iir_Kind_Psl_Assume_Directive --Iir_Kind_Psl_Cover_Directive Iir_Kind_Psl_Restrict_Directive; diff --git a/src/vhdl/vhdl-nodes_meta.adb b/src/vhdl/vhdl-nodes_meta.adb index 2e3512028..4b4c6b632 100644 --- a/src/vhdl/vhdl-nodes_meta.adb +++ b/src/vhdl/vhdl-nodes_meta.adb @@ -1388,8 +1388,10 @@ package body Vhdl.Nodes_Meta is return "concurrent_assertion_statement"; when Iir_Kind_Concurrent_Procedure_Call_Statement => return "concurrent_procedure_call_statement"; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Directive => return "psl_assert_statement"; + when Iir_Kind_Psl_Assume_Directive => + return "psl_assume_statement"; when Iir_Kind_Psl_Cover_Directive => return "psl_cover_directive"; when Iir_Kind_Psl_Restrict_Directive => @@ -3795,7 +3797,21 @@ package body Vhdl.Nodes_Meta is Field_Parent, Field_Procedure_Call, Field_Chain, - -- Iir_Kind_Psl_Assert_Statement + -- Iir_Kind_Psl_Assert_Directive + Field_Psl_Property, + Field_Label, + Field_PSL_Clock, + Field_PSL_NFA, + Field_PSL_Nbr_States, + Field_PSL_EOS_Flag, + Field_Postponed_Flag, + Field_Visible_Flag, + Field_Parent, + Field_Chain, + Field_Severity_Expression, + Field_Report_Expression, + Field_PSL_Clock_Sensitivity, + -- Iir_Kind_Psl_Assume_Directive Field_Psl_Property, Field_Label, Field_PSL_Clock, @@ -4640,91 +4656,92 @@ package body Vhdl.Nodes_Meta is Iir_Kind_Concurrent_Selected_Signal_Assignment => 1370, Iir_Kind_Concurrent_Assertion_Statement => 1378, Iir_Kind_Concurrent_Procedure_Call_Statement => 1385, - Iir_Kind_Psl_Assert_Statement => 1398, - Iir_Kind_Psl_Cover_Directive => 1411, - Iir_Kind_Psl_Restrict_Directive => 1422, - Iir_Kind_Block_Statement => 1436, - Iir_Kind_If_Generate_Statement => 1447, - Iir_Kind_Case_Generate_Statement => 1456, - Iir_Kind_For_Generate_Statement => 1465, - Iir_Kind_Component_Instantiation_Statement => 1476, - Iir_Kind_Psl_Default_Clock => 1480, - Iir_Kind_Simple_Simultaneous_Statement => 1487, - Iir_Kind_Generate_Statement_Body => 1498, - Iir_Kind_If_Generate_Else_Clause => 1504, - Iir_Kind_Simple_Signal_Assignment_Statement => 1514, - Iir_Kind_Conditional_Signal_Assignment_Statement => 1524, - Iir_Kind_Selected_Waveform_Assignment_Statement => 1535, - Iir_Kind_Null_Statement => 1539, - Iir_Kind_Assertion_Statement => 1546, - Iir_Kind_Report_Statement => 1552, - Iir_Kind_Wait_Statement => 1560, - Iir_Kind_Variable_Assignment_Statement => 1567, - Iir_Kind_Conditional_Variable_Assignment_Statement => 1574, - Iir_Kind_Return_Statement => 1580, - Iir_Kind_For_Loop_Statement => 1589, - Iir_Kind_While_Loop_Statement => 1598, - Iir_Kind_Next_Statement => 1605, - Iir_Kind_Exit_Statement => 1612, - Iir_Kind_Case_Statement => 1620, - Iir_Kind_Procedure_Call_Statement => 1626, - Iir_Kind_If_Statement => 1636, - Iir_Kind_Elsif => 1642, - Iir_Kind_Character_Literal => 1650, - Iir_Kind_Simple_Name => 1658, - Iir_Kind_Selected_Name => 1667, - Iir_Kind_Operator_Symbol => 1673, - Iir_Kind_Reference_Name => 1677, - Iir_Kind_External_Constant_Name => 1685, - Iir_Kind_External_Signal_Name => 1693, - Iir_Kind_External_Variable_Name => 1702, - Iir_Kind_Selected_By_All_Name => 1708, - Iir_Kind_Parenthesis_Name => 1713, - Iir_Kind_Package_Pathname => 1717, - Iir_Kind_Absolute_Pathname => 1718, - Iir_Kind_Relative_Pathname => 1719, - Iir_Kind_Pathname_Element => 1724, - Iir_Kind_Base_Attribute => 1726, - Iir_Kind_Subtype_Attribute => 1731, - Iir_Kind_Element_Attribute => 1736, - Iir_Kind_Left_Type_Attribute => 1741, - Iir_Kind_Right_Type_Attribute => 1746, - Iir_Kind_High_Type_Attribute => 1751, - Iir_Kind_Low_Type_Attribute => 1756, - Iir_Kind_Ascending_Type_Attribute => 1761, - Iir_Kind_Image_Attribute => 1767, - Iir_Kind_Value_Attribute => 1773, - Iir_Kind_Pos_Attribute => 1779, - Iir_Kind_Val_Attribute => 1785, - Iir_Kind_Succ_Attribute => 1791, - Iir_Kind_Pred_Attribute => 1797, - Iir_Kind_Leftof_Attribute => 1803, - Iir_Kind_Rightof_Attribute => 1809, - Iir_Kind_Delayed_Attribute => 1818, - Iir_Kind_Stable_Attribute => 1827, - Iir_Kind_Quiet_Attribute => 1836, - Iir_Kind_Transaction_Attribute => 1845, - Iir_Kind_Event_Attribute => 1849, - Iir_Kind_Active_Attribute => 1853, - Iir_Kind_Last_Event_Attribute => 1857, - Iir_Kind_Last_Active_Attribute => 1861, - Iir_Kind_Last_Value_Attribute => 1865, - Iir_Kind_Driving_Attribute => 1869, - Iir_Kind_Driving_Value_Attribute => 1873, - Iir_Kind_Behavior_Attribute => 1873, - Iir_Kind_Structure_Attribute => 1873, - Iir_Kind_Simple_Name_Attribute => 1880, - Iir_Kind_Instance_Name_Attribute => 1885, - Iir_Kind_Path_Name_Attribute => 1890, - Iir_Kind_Left_Array_Attribute => 1897, - Iir_Kind_Right_Array_Attribute => 1904, - Iir_Kind_High_Array_Attribute => 1911, - Iir_Kind_Low_Array_Attribute => 1918, - Iir_Kind_Length_Array_Attribute => 1925, - Iir_Kind_Ascending_Array_Attribute => 1932, - Iir_Kind_Range_Array_Attribute => 1939, - Iir_Kind_Reverse_Range_Array_Attribute => 1946, - Iir_Kind_Attribute_Name => 1955 + Iir_Kind_Psl_Assert_Directive => 1398, + Iir_Kind_Psl_Assume_Directive => 1411, + Iir_Kind_Psl_Cover_Directive => 1424, + Iir_Kind_Psl_Restrict_Directive => 1435, + Iir_Kind_Block_Statement => 1449, + Iir_Kind_If_Generate_Statement => 1460, + Iir_Kind_Case_Generate_Statement => 1469, + Iir_Kind_For_Generate_Statement => 1478, + Iir_Kind_Component_Instantiation_Statement => 1489, + Iir_Kind_Psl_Default_Clock => 1493, + Iir_Kind_Simple_Simultaneous_Statement => 1500, + Iir_Kind_Generate_Statement_Body => 1511, + Iir_Kind_If_Generate_Else_Clause => 1517, + Iir_Kind_Simple_Signal_Assignment_Statement => 1527, + Iir_Kind_Conditional_Signal_Assignment_Statement => 1537, + Iir_Kind_Selected_Waveform_Assignment_Statement => 1548, + Iir_Kind_Null_Statement => 1552, + Iir_Kind_Assertion_Statement => 1559, + Iir_Kind_Report_Statement => 1565, + Iir_Kind_Wait_Statement => 1573, + Iir_Kind_Variable_Assignment_Statement => 1580, + Iir_Kind_Conditional_Variable_Assignment_Statement => 1587, + Iir_Kind_Return_Statement => 1593, + Iir_Kind_For_Loop_Statement => 1602, + Iir_Kind_While_Loop_Statement => 1611, + Iir_Kind_Next_Statement => 1618, + Iir_Kind_Exit_Statement => 1625, + Iir_Kind_Case_Statement => 1633, + Iir_Kind_Procedure_Call_Statement => 1639, + Iir_Kind_If_Statement => 1649, + Iir_Kind_Elsif => 1655, + Iir_Kind_Character_Literal => 1663, + Iir_Kind_Simple_Name => 1671, + Iir_Kind_Selected_Name => 1680, + Iir_Kind_Operator_Symbol => 1686, + Iir_Kind_Reference_Name => 1690, + Iir_Kind_External_Constant_Name => 1698, + Iir_Kind_External_Signal_Name => 1706, + Iir_Kind_External_Variable_Name => 1715, + Iir_Kind_Selected_By_All_Name => 1721, + Iir_Kind_Parenthesis_Name => 1726, + Iir_Kind_Package_Pathname => 1730, + Iir_Kind_Absolute_Pathname => 1731, + Iir_Kind_Relative_Pathname => 1732, + Iir_Kind_Pathname_Element => 1737, + Iir_Kind_Base_Attribute => 1739, + Iir_Kind_Subtype_Attribute => 1744, + Iir_Kind_Element_Attribute => 1749, + Iir_Kind_Left_Type_Attribute => 1754, + Iir_Kind_Right_Type_Attribute => 1759, + Iir_Kind_High_Type_Attribute => 1764, + Iir_Kind_Low_Type_Attribute => 1769, + Iir_Kind_Ascending_Type_Attribute => 1774, + Iir_Kind_Image_Attribute => 1780, + Iir_Kind_Value_Attribute => 1786, + Iir_Kind_Pos_Attribute => 1792, + Iir_Kind_Val_Attribute => 1798, + Iir_Kind_Succ_Attribute => 1804, + Iir_Kind_Pred_Attribute => 1810, + Iir_Kind_Leftof_Attribute => 1816, + Iir_Kind_Rightof_Attribute => 1822, + Iir_Kind_Delayed_Attribute => 1831, + Iir_Kind_Stable_Attribute => 1840, + Iir_Kind_Quiet_Attribute => 1849, + Iir_Kind_Transaction_Attribute => 1858, + Iir_Kind_Event_Attribute => 1862, + Iir_Kind_Active_Attribute => 1866, + Iir_Kind_Last_Event_Attribute => 1870, + Iir_Kind_Last_Active_Attribute => 1874, + Iir_Kind_Last_Value_Attribute => 1878, + Iir_Kind_Driving_Attribute => 1882, + Iir_Kind_Driving_Value_Attribute => 1886, + Iir_Kind_Behavior_Attribute => 1886, + Iir_Kind_Structure_Attribute => 1886, + Iir_Kind_Simple_Name_Attribute => 1893, + Iir_Kind_Instance_Name_Attribute => 1898, + Iir_Kind_Path_Name_Attribute => 1903, + Iir_Kind_Left_Array_Attribute => 1910, + Iir_Kind_Right_Array_Attribute => 1917, + Iir_Kind_High_Array_Attribute => 1924, + Iir_Kind_Low_Array_Attribute => 1931, + Iir_Kind_Length_Array_Attribute => 1938, + Iir_Kind_Ascending_Array_Attribute => 1945, + Iir_Kind_Range_Array_Attribute => 1952, + Iir_Kind_Reverse_Range_Array_Attribute => 1959, + Iir_Kind_Attribute_Name => 1968 ); function Get_Fields_First (K : Iir_Kind) return Fields_Index is @@ -7393,7 +7410,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement @@ -8172,7 +8190,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement @@ -8223,7 +8242,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement @@ -8309,7 +8329,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement @@ -8777,7 +8798,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; @@ -9035,7 +9057,8 @@ package body Vhdl.Nodes_Meta is begin case K is when Iir_Kind_Concurrent_Assertion_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Assertion_Statement | Iir_Kind_Report_Statement => @@ -9049,7 +9072,8 @@ package body Vhdl.Nodes_Meta is begin case K is when Iir_Kind_Concurrent_Assertion_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Assertion_Statement | Iir_Kind_Report_Statement => @@ -9393,7 +9417,8 @@ package body Vhdl.Nodes_Meta is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive | Iir_Kind_Block_Statement @@ -10759,7 +10784,13 @@ package body Vhdl.Nodes_Meta is function Has_Psl_Property (K : Iir_Kind) return Boolean is begin - return K = Iir_Kind_Psl_Assert_Statement; + case K is + when Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive => + return True; + when others => + return False; + end case; end Has_Psl_Property; function Has_Psl_Sequence (K : Iir_Kind) return Boolean is @@ -10799,7 +10830,8 @@ package body Vhdl.Nodes_Meta is case K is when Iir_Kind_Psl_Declaration | Iir_Kind_Psl_Endpoint_Declaration - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; @@ -10813,7 +10845,8 @@ package body Vhdl.Nodes_Meta is case K is when Iir_Kind_Psl_Declaration | Iir_Kind_Psl_Endpoint_Declaration - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; @@ -10826,7 +10859,8 @@ package body Vhdl.Nodes_Meta is begin case K is when Iir_Kind_Psl_Endpoint_Declaration - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; @@ -10839,7 +10873,8 @@ package body Vhdl.Nodes_Meta is begin case K is when Iir_Kind_Psl_Endpoint_Declaration - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; @@ -10852,7 +10887,8 @@ package body Vhdl.Nodes_Meta is begin case K is when Iir_Kind_Psl_Endpoint_Declaration - | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Assert_Directive + | Iir_Kind_Psl_Assume_Directive | Iir_Kind_Psl_Cover_Directive | Iir_Kind_Psl_Restrict_Directive => return True; diff --git a/src/vhdl/vhdl-parse.adb b/src/vhdl/vhdl-parse.adb index e182821ae..491d14b85 100644 --- a/src/vhdl/vhdl-parse.adb +++ b/src/vhdl/vhdl-parse.adb @@ -8586,11 +8586,11 @@ package body Vhdl.Parse is Expect_Scan (Tok_Semi_Colon); end Parse_Psl_Assert_Report_Severity; - function Parse_Psl_Assert_Statement return Iir + function Parse_Psl_Assert_Directive return Iir is Res : Iir; begin - Res := Create_Iir (Iir_Kind_Psl_Assert_Statement); + Res := Create_Iir (Iir_Kind_Psl_Assert_Directive); -- Accept PSL tokens if Flags.Vhdl_Std >= Vhdl_08 then @@ -8605,7 +8605,26 @@ package body Vhdl.Parse is Parse_Psl_Assert_Report_Severity (Res); return Res; - end Parse_Psl_Assert_Statement; + end Parse_Psl_Assert_Directive; + + function Parse_Psl_Assume_Directive return Iir + is + Res : Iir; + begin + Res := Create_Iir (Iir_Kind_Psl_Assume_Directive); + + -- Skip 'assume' + Scan; + + Set_Psl_Property (Res, Parse_Psl.Parse_Psl_Property); + + Vhdl.Scanner.Flag_Psl := False; + Vhdl.Scanner.Flag_Scan_In_Comment := False; + + Expect_Scan (Tok_Semi_Colon); + + return Res; + end Parse_Psl_Assume_Directive; function Parse_Psl_Cover_Directive return Iir is @@ -8758,7 +8777,7 @@ package body Vhdl.Parse is if Vhdl_Std >= Vhdl_08 or else (Flag_Psl_Comment and then Flag_Scan_In_Comment) then - Stmt := Parse_Psl_Assert_Statement; + Stmt := Parse_Psl_Assert_Directive; else Stmt := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement); Parse_Assertion (Stmt); @@ -8804,6 +8823,9 @@ package body Vhdl.Parse is Postponed_Not_Allowed; Label_Not_Allowed; Stmt := Parse_Psl_Declaration; + when Tok_Psl_Assume => + Postponed_Not_Allowed; + Stmt := Parse_Psl_Assume_Directive; when Tok_Psl_Cover => Postponed_Not_Allowed; Stmt := Parse_Psl_Cover_Directive; diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb index 16f9e0e37..7c87b3df5 100644 --- a/src/vhdl/vhdl-prints.adb +++ b/src/vhdl/vhdl-prints.adb @@ -3893,7 +3893,7 @@ package body Vhdl.Prints is end if; end Disp_PSL_NFA; - procedure Disp_Psl_Assert_Statement + procedure Disp_Psl_Assert_Directive (Ctxt : in out Ctxt_Class; Stmt : Iir) is begin Start_Hbox (Ctxt); @@ -3909,7 +3909,25 @@ package body Vhdl.Prints is Disp_Token (Ctxt, Tok_Semi_Colon); Close_Hbox (Ctxt); Disp_PSL_NFA (Get_PSL_NFA (Stmt)); - end Disp_Psl_Assert_Statement; + end Disp_Psl_Assert_Directive; + + procedure Disp_Psl_Assume_Directive + (Ctxt : in out Ctxt_Class; Stmt : Iir) is + begin + Start_Hbox (Ctxt); + if Vhdl_Std < Vhdl_08 then + OOB.Put ("--psl "); + end if; + Disp_Label (Ctxt, Stmt); + Disp_Postponed (Ctxt, Stmt); + Disp_Token (Ctxt, Tok_Psl_Assume); + Disp_Psl_Expression (Ctxt, Get_Psl_Property (Stmt)); + Disp_Report_Expression (Ctxt, Stmt); + Disp_Severity_Expression (Ctxt, Stmt); + Disp_Token (Ctxt, Tok_Semi_Colon); + Close_Hbox (Ctxt); + Disp_PSL_NFA (Get_PSL_NFA (Stmt)); + end Disp_Psl_Assume_Directive; procedure Disp_Psl_Cover_Directive (Ctxt : in out Ctxt_Class; Stmt : Iir) is @@ -3984,8 +4002,10 @@ package body Vhdl.Prints is when Iir_Kind_Psl_Declaration | Iir_Kind_Psl_Endpoint_Declaration => Disp_Psl_Declaration (Ctxt, Stmt); - when Iir_Kind_Psl_Assert_Statement => - Disp_Psl_Assert_Statement (Ctxt, Stmt); + when Iir_Kind_Psl_Assert_Directive => + Disp_Psl_Assert_Directive (Ctxt, Stmt); + when Iir_Kind_Psl_Assume_Directive => + Disp_Psl_Assume_Directive (Ctxt, Stmt); when Iir_Kind_Psl_Cover_Directive => Disp_Psl_Cover_Directive (Ctxt, Stmt); when Iir_Kind_Psl_Restrict_Directive => diff --git a/src/vhdl/vhdl-scanner.adb b/src/vhdl/vhdl-scanner.adb index 740617ba4..2f08ffbab 100644 --- a/src/vhdl/vhdl-scanner.adb +++ b/src/vhdl/vhdl-scanner.adb @@ -1307,6 +1307,8 @@ package body Vhdl.Scanner is Current_Token := Tok_Psl_Property; when Std_Names.Name_Endpoint => Current_Token := Tok_Psl_Endpoint; + when Std_Names.Name_Assume => + Current_Token := Tok_Psl_Assume; when Std_Names.Name_Cover => Current_Token := Tok_Psl_Cover; when Std_Names.Name_Default => diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb index b4e949aac..671c59c27 100644 --- a/src/vhdl/vhdl-sem_psl.adb +++ b/src/vhdl/vhdl-sem_psl.adb @@ -695,12 +695,12 @@ package body Vhdl.Sem_Psl is Set_PSL_Clock (Stmt, Clk); end Sem_Psl_Directive_Clock; - function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir + function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir is Prop : PSL_Node; Res : Iir; begin - pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Statement); + pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive); -- Sem report and severity expressions. Sem_Report_Statement (Stmt); @@ -730,7 +730,26 @@ package body Vhdl.Sem_Psl is PSL.Subsets.Check_Simple (Prop); return Stmt; - end Sem_Psl_Assert_Statement; + end Sem_Psl_Assert_Directive; + + procedure Sem_Psl_Assume_Directive (Stmt : Iir) + is + Prop : PSL_Node; + begin + -- Sem report and severity expressions. + Sem_Report_Statement (Stmt); + + Prop := Get_Psl_Property (Stmt); + Prop := Sem_Property (Prop, True); + Set_Psl_Property (Stmt, Prop); + + -- Properties must be clocked. + Sem_Psl_Directive_Clock (Stmt, Prop); + Set_Psl_Property (Stmt, Prop); + + -- Check simple subset restrictions. + PSL.Subsets.Check_Simple (Prop); + end Sem_Psl_Assume_Directive; procedure Sem_Psl_Cover_Directive (Stmt : Iir) is diff --git a/src/vhdl/vhdl-sem_psl.ads b/src/vhdl/vhdl-sem_psl.ads index 433555b20..1cd02796e 100644 --- a/src/vhdl/vhdl-sem_psl.ads +++ b/src/vhdl/vhdl-sem_psl.ads @@ -23,8 +23,9 @@ package Vhdl.Sem_Psl is procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir); -- May return a non-psl concurrent assertion statement. - function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir; + function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir; + procedure Sem_Psl_Assume_Directive (Stmt : Iir); procedure Sem_Psl_Cover_Directive (Stmt : Iir); procedure Sem_Psl_Restrict_Directive (Stmt : Iir); procedure Sem_Psl_Default_Clock (Stmt : Iir); diff --git a/src/vhdl/vhdl-sem_stmts.adb b/src/vhdl/vhdl-sem_stmts.adb index 4b8c5880c..545a543c7 100644 --- a/src/vhdl/vhdl-sem_stmts.adb +++ b/src/vhdl/vhdl-sem_stmts.adb @@ -2020,8 +2020,10 @@ package body Vhdl.Sem_Stmts is Sem_Psl.Sem_Psl_Declaration (El); when Iir_Kind_Psl_Endpoint_Declaration => Sem_Psl.Sem_Psl_Endpoint_Declaration (El); - when Iir_Kind_Psl_Assert_Statement => - New_El := Sem_Psl.Sem_Psl_Assert_Statement (El); + when Iir_Kind_Psl_Assert_Directive => + New_El := Sem_Psl.Sem_Psl_Assert_Directive (El); + when Iir_Kind_Psl_Assume_Directive => + Sem_Psl.Sem_Psl_Assume_Directive (El); when Iir_Kind_Psl_Cover_Directive => Sem_Psl.Sem_Psl_Cover_Directive (El); when Iir_Kind_Psl_Restrict_Directive => diff --git a/src/vhdl/vhdl-tokens.adb b/src/vhdl/vhdl-tokens.adb index 8ad0e4081..1f17c5092 100644 --- a/src/vhdl/vhdl-tokens.adb +++ b/src/vhdl/vhdl-tokens.adb @@ -422,6 +422,8 @@ package body Vhdl.Tokens is return "sequence"; when Tok_Psl_Endpoint => return "endpoint"; + when Tok_Psl_Assume => + return "assume"; when Tok_Psl_Cover => return "cover"; when Tok_Psl_Restrict => diff --git a/src/vhdl/vhdl-tokens.ads b/src/vhdl/vhdl-tokens.ads index e8daf0bce..f8e2dd14e 100644 --- a/src/vhdl/vhdl-tokens.ads +++ b/src/vhdl/vhdl-tokens.ads @@ -261,6 +261,7 @@ package Vhdl.Tokens is Tok_Psl_Property, Tok_Psl_Sequence, Tok_Psl_Endpoint, + Tok_Psl_Assume, Tok_Psl_Cover, Tok_Psl_Restrict, Tok_Psl_Restrict_Guarantee, diff --git a/testsuite/gna/issue880/psl.ref b/testsuite/gna/issue880/psl.ref new file mode 100644 index 000000000..5fd471f5d --- /dev/null +++ b/testsuite/gna/issue880/psl.ref @@ -0,0 +1,30 @@ +{ "details" : [ + { "directive": "assumption", + "name": ".psl(behav).a1", + "file": "psl.vhdl", + "line": 27, + "count": 0, + "status": "passed"}, + { "directive": "assumption", + "name": ".psl(behav).a2", + "file": "psl.vhdl", + "line": 28, + "count": 0, + "status": "passed"}, + { "directive": "cover", + "name": ".psl(behav).c1", + "file": "psl.vhdl", + "line": 29, + "count": 3, + "status": "covered"}], + "summary" : { + "assert": 0, + "assert-failure": 0, + "assert-pass": 0, + "assume": 2, + "assume-failure": 0, + "assume-pass": 2, + "cover": 1, + "cover-failure": 0, + "cover-pass": 1} +} diff --git a/testsuite/gna/issue880/psl.vhdl b/testsuite/gna/issue880/psl.vhdl new file mode 100644 index 000000000..a1e203f5f --- /dev/null +++ b/testsuite/gna/issue880/psl.vhdl @@ -0,0 +1,30 @@ +entity psl is +end; + +architecture behav of psl is + signal a, b, c : bit; + signal clk : bit; + subtype wf_type is bit_vector (0 to 7); + constant wave_a : wf_type := "10010100"; + constant wave_b : wf_type := "01001010"; + constant wave_c : wf_type := "00100101"; +begin + process + begin + for i in wf_type'range loop + clk <= '0'; + wait for 1 ns; + a <= wave_a (i); + b <= wave_b (i); + c <= wave_c (i); + clk <= '1'; + wait for 1 ns; + end loop; + wait; + end process; + + -- psl default clock is (clk'event and clk = '1'); + -- psl a1: assume always a |=> b; + -- psl a2: assume always a -> eventually! c; + -- psl c1: cover {a;b;c}; +end behav; diff --git a/testsuite/gna/issue880/testsuite.sh b/testsuite/gna/issue880/testsuite.sh new file mode 100755 index 000000000..136317e17 --- /dev/null +++ b/testsuite/gna/issue880/testsuite.sh @@ -0,0 +1,41 @@ +#! /bin/sh + +. ../../testenv.sh + +GHDL_STD_FLAGS="-fpsl" +analyze psl.vhdl +elab psl +if ghdl_has_feature psl psl; then + simulate psl --psl-report=psl.out + + if ! diff --strip-trailing-cr psl.out psl.ref > /dev/null; then + echo "report mismatch" + exit 1 + fi + + rm -f psl.out +fi +clean + +# Using vhdl 08 +GHDL_STD_FLAGS="-fpsl --std=08" +analyze psl.vhdl +elab -fpsl psl +if ghdl_has_feature psl psl; then + simulate psl --psl-report=psl.out + + diff --strip-trailing-cr -q psl.out psl.ref + + rm -f psl.out +fi +clean + +# Usage example (python 2.7): +# +# import json +# d=json.load(open("psl.out")) +# print d['summary'] +# {u'assert-pass': 2, u'cover': 1, ... } +# print d['summary']['assert'] + +echo "Test successful" diff --git a/testsuite/gna/ticket24/psl.ref b/testsuite/gna/ticket24/psl.ref index 6a5588a3a..9cd8cdb35 100644 --- a/testsuite/gna/ticket24/psl.ref +++ b/testsuite/gna/ticket24/psl.ref @@ -21,6 +21,9 @@ "assert": 2, "assert-failure": 0, "assert-pass": 2, + "assume": 0, + "assume-failure": 0, + "assume-pass": 0, "cover": 1, "cover-failure": 0, "cover-pass": 1} |