From 0331772c3ef05bad40b748542939ccafab2a9c68 Mon Sep 17 00:00:00 2001 From: Pepijn de Vos Date: Wed, 7 Aug 2019 04:20:14 +0200 Subject: Add support for PSL assumptions, used in formal verification (#880) * vhdl: make the parser understand PSL assume * assume does not actually have report according to the spec. Just a property. * add SPL assume to semantic analysis * canonicalise PSL assume * add assume to annotations * add PSL assume to simulation code * statement -> directive * add assume to translation files * update ticked24 testcase * correctly parse assume * add assume testcase * refactor chunk of duplicated code --- python/libghdl/thin/vhdl/nodes.py | 180 +++++++++++++++++++------------------ python/libghdl/thin/vhdl/tokens.py | 47 +++++----- 2 files changed, 117 insertions(+), 110 deletions(-) (limited to 'python') 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 -- cgit v1.2.3