From c033bff91ebf329f3876d70b49588e1d785fc1f7 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Tue, 16 Jun 2020 07:29:53 +0200 Subject: vhdl psl: add support for equivalence operator. Fix #1371 --- src/psl/psl-nodes.adb | 114 ++++++++++++++++++++-------------------- src/psl/psl-nodes.adb.in | 123 ++++++++++++++++++++++++-------------------- src/psl/psl-nodes.ads | 4 ++ src/psl/psl-nodes_meta.adb | 100 +++++++++++++++++++++-------------- src/psl/psl-qm.adb | 16 ++++++ src/psl/psl-rewrites.adb | 5 +- src/psl/psl-subsets.adb | 52 ++++++++++--------- src/vhdl/vhdl-parse_psl.adb | 110 +++++++++++++++++++++------------------ src/vhdl/vhdl-scanner.adb | 8 +++ src/vhdl/vhdl-sem_psl.adb | 11 ++-- src/vhdl/vhdl-tokens.adb | 2 + src/vhdl/vhdl-tokens.ads | 1 + 12 files changed, 316 insertions(+), 230 deletions(-) (limited to 'src') diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb index d3a0d9320..5fc439efb 100644 --- a/src/psl/psl-nodes.adb +++ b/src/psl/psl-nodes.adb @@ -337,43 +337,44 @@ package body PSL.Nodes is begin case Get_Kind (N) is when N_And_Prop - | N_Or_Prop - | N_Paren_Prop - | N_Log_Imp_Prop - | N_Always - | N_Never - | N_Eventually - | N_Next - | N_Next_E - | N_Next_A - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Before - | N_Until - | N_Abort - | N_Strong - | N_Property_Parameter - | N_Property_Instance => + | N_Or_Prop + | N_Paren_Prop + | N_Log_Imp_Prop + | N_Log_Equiv_Prop + | N_Always + | N_Never + | N_Eventually + | N_Next + | N_Next_E + | N_Next_A + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Before + | N_Until + | N_Abort + | N_Strong + | N_Property_Parameter + | N_Property_Instance => return Type_Property; when N_Braced_SERE - | N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE - | N_Clocked_SERE - | N_Overlap_Imp_Seq - | N_Imp_Seq - | N_And_Seq - | N_Or_Seq - | N_Match_And_Seq - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Clock_Event - | N_Sequence_Instance - | N_Endpoint_Instance - | N_Sequence_Parameter => + | N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE + | N_Clocked_SERE + | N_Overlap_Imp_Seq + | N_Imp_Seq + | N_And_Seq + | N_Or_Seq + | N_Match_And_Seq + | N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq + | N_Plus_Repeat_Seq + | N_Clock_Event + | N_Sequence_Instance + | N_Endpoint_Instance + | N_Sequence_Parameter => return Type_Sequence; when N_Name => return Get_Psl_Type (Get_Decl (N)); @@ -381,30 +382,31 @@ package body PSL.Nodes is -- FIXME. return Type_Boolean; when N_Or_Bool - | N_And_Bool - | N_Not_Bool - | N_Imp_Bool - | N_False - | N_True - | N_Boolean_Parameter - | N_Paren_Bool - | N_HDL_Bool => + | N_And_Bool + | N_Not_Bool + | N_Imp_Bool + | N_Equiv_Bool + | N_False + | N_True + | N_Boolean_Parameter + | N_Paren_Bool + | N_HDL_Bool => return Type_Boolean; when N_Number - | N_Const_Parameter => + | N_Const_Parameter => return Type_Numeric; when N_Vmode - | N_Vunit - | N_Vprop - | N_Hdl_Mod_Name - | N_Assert_Directive - | N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Property_Declaration - | N_Actual - | N_Name_Decl - | N_Error - | N_EOS => + | N_Vunit + | N_Vprop + | N_Hdl_Mod_Name + | N_Assert_Directive + | N_Sequence_Declaration + | N_Endpoint_Declaration + | N_Property_Declaration + | N_Actual + | N_Name_Decl + | N_Error + | N_EOS => PSL.Errors.Error_Kind ("get_psl_type", N); end case; end Get_Psl_Type; @@ -444,6 +446,7 @@ package body PSL.Nodes is | N_Imp_Seq | N_Overlap_Imp_Seq | N_Log_Imp_Prop + | N_Log_Equiv_Prop | N_Next | N_Next_A | N_Next_E @@ -473,6 +476,7 @@ package body PSL.Nodes is | N_And_Bool | N_Or_Bool | N_Imp_Bool + | N_Equiv_Bool | N_HDL_Expr | N_HDL_Bool | N_False diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in index 4294140c1..c0236d9dc 100644 --- a/src/psl/psl-nodes.adb.in +++ b/src/psl/psl-nodes.adb.in @@ -304,23 +304,32 @@ package body PSL.Nodes is Errors.Error_Kind (Msg, N); end Failed; - procedure Init is + procedure Init (Loc : Location_Type) is begin + pragma Assert (Loc /= No_Location); Nodet.Init; + if Create_Node (N_False) /= False_Node then raise Internal_Error; end if; + Set_Location (False_Node, Loc); + if Create_Node (N_True) /= True_Node then raise Internal_Error; end if; + Set_Location (True_Node, Loc); + if Create_Node (N_Number) /= One_Node then raise Internal_Error; end if; Set_Value (One_Node, 1); + Set_Location (One_Node, Loc); + if Create_Node (N_EOS) /= EOS_Node then raise Internal_Error; end if; Set_Hash (EOS_Node, 0); + Set_Location (EOS_Node, Loc); PSL.Hash.Init; end Init; @@ -328,43 +337,44 @@ package body PSL.Nodes is begin case Get_Kind (N) is when N_And_Prop - | N_Or_Prop - | N_Paren_Prop - | N_Log_Imp_Prop - | N_Always - | N_Never - | N_Eventually - | N_Next - | N_Next_E - | N_Next_A - | N_Next_Event - | N_Next_Event_A - | N_Next_Event_E - | N_Before - | N_Until - | N_Abort - | N_Strong - | N_Property_Parameter - | N_Property_Instance => + | N_Or_Prop + | N_Paren_Prop + | N_Log_Imp_Prop + | N_Log_Equiv_Prop + | N_Always + | N_Never + | N_Eventually + | N_Next + | N_Next_E + | N_Next_A + | N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Before + | N_Until + | N_Abort + | N_Strong + | N_Property_Parameter + | N_Property_Instance => return Type_Property; when N_Braced_SERE - | N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE - | N_Clocked_SERE - | N_Overlap_Imp_Seq - | N_Imp_Seq - | N_And_Seq - | N_Or_Seq - | N_Match_And_Seq - | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Clock_Event - | N_Sequence_Instance - | N_Endpoint_Instance - | N_Sequence_Parameter => + | N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE + | N_Clocked_SERE + | N_Overlap_Imp_Seq + | N_Imp_Seq + | N_And_Seq + | N_Or_Seq + | N_Match_And_Seq + | N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq + | N_Plus_Repeat_Seq + | N_Clock_Event + | N_Sequence_Instance + | N_Endpoint_Instance + | N_Sequence_Parameter => return Type_Sequence; when N_Name => return Get_Psl_Type (Get_Decl (N)); @@ -372,30 +382,31 @@ package body PSL.Nodes is -- FIXME. return Type_Boolean; when N_Or_Bool - | N_And_Bool - | N_Not_Bool - | N_Imp_Bool - | N_False - | N_True - | N_Boolean_Parameter - | N_Paren_Bool - | N_HDL_Bool => + | N_And_Bool + | N_Not_Bool + | N_Imp_Bool + | N_Equiv_Bool + | N_False + | N_True + | N_Boolean_Parameter + | N_Paren_Bool + | N_HDL_Bool => return Type_Boolean; when N_Number - | N_Const_Parameter => + | N_Const_Parameter => return Type_Numeric; when N_Vmode - | N_Vunit - | N_Vprop - | N_Hdl_Mod_Name - | N_Assert_Directive - | N_Sequence_Declaration - | N_Endpoint_Declaration - | N_Property_Declaration - | N_Actual - | N_Name_Decl - | N_Error - | N_EOS => + | N_Vunit + | N_Vprop + | N_Hdl_Mod_Name + | N_Assert_Directive + | N_Sequence_Declaration + | N_Endpoint_Declaration + | N_Property_Declaration + | N_Actual + | N_Name_Decl + | N_Error + | N_EOS => PSL.Errors.Error_Kind ("get_psl_type", N); end case; end Get_Psl_Type; diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads index 9418ae78a..aedf621be 100644 --- a/src/psl/psl-nodes.ads +++ b/src/psl/psl-nodes.ads @@ -56,6 +56,7 @@ package PSL.Nodes is N_Imp_Seq, -- |=> N_Overlap_Imp_Seq, -- |-> N_Log_Imp_Prop, -- -> + N_Log_Equiv_Prop, -- <-> N_Next, N_Next_A, N_Next_E, @@ -91,6 +92,7 @@ package PSL.Nodes is N_And_Bool, N_Or_Bool, N_Imp_Bool, -- -> + N_Equiv_Bool, -- <-> N_HDL_Expr, N_HDL_Bool, N_False, @@ -307,6 +309,7 @@ package PSL.Nodes is -- Get/Set_Property (Field4) -- N_Log_Imp_Prop (Short) + -- N_Log_Equiv_Prop (Short) -- -- Get/Set_Left (Field1) -- @@ -420,6 +423,7 @@ package PSL.Nodes is -- N_And_Bool (Short) -- N_Or_Bool (Short) -- N_Imp_Bool (Short) + -- N_Equiv_Bool (Short) -- -- Get/Set_Presence (State1) -- diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb index ef5808fe4..52ad5e245 100644 --- a/src/psl/psl-nodes_meta.adb +++ b/src/psl/psl-nodes_meta.adb @@ -184,6 +184,8 @@ package body PSL.Nodes_Meta is return "overlap_imp_seq"; when N_Log_Imp_Prop => return "log_imp_prop"; + when N_Log_Equiv_Prop => + return "log_equiv_prop"; when N_Next => return "next"; when N_Next_A => @@ -242,6 +244,8 @@ package body PSL.Nodes_Meta is return "or_bool"; when N_Imp_Bool => return "imp_bool"; + when N_Equiv_Bool => + return "equiv_bool"; when N_HDL_Expr => return "hdl_expr"; when N_HDL_Bool => @@ -425,6 +429,9 @@ package body PSL.Nodes_Meta is -- N_Log_Imp_Prop Field_Left, Field_Right, + -- N_Log_Equiv_Prop + Field_Left, + Field_Right, -- N_Next Field_Strong_Flag, Field_Number, @@ -542,6 +549,12 @@ package body PSL.Nodes_Meta is Field_Left, Field_Right, Field_Hash_Link, + -- N_Equiv_Bool + Field_Hash, + Field_Presence, + Field_Left, + Field_Right, + Field_Hash_Link, -- N_HDL_Expr Field_HDL_Node, Field_HDL_Hash, @@ -594,43 +607,45 @@ package body PSL.Nodes_Meta is N_Imp_Seq => 60, N_Overlap_Imp_Seq => 62, N_Log_Imp_Prop => 64, - N_Next => 67, - N_Next_A => 71, - N_Next_E => 75, - N_Next_Event => 79, - N_Next_Event_A => 84, - N_Next_Event_E => 89, - N_Abort => 91, - N_Until => 95, - N_Before => 99, - N_Or_Prop => 101, - N_And_Prop => 103, - N_Paren_Prop => 104, - N_Braced_SERE => 105, - N_Concat_SERE => 107, - N_Fusion_SERE => 109, - N_Within_SERE => 111, - N_Clocked_SERE => 113, - N_Match_And_Seq => 115, - N_And_Seq => 117, - N_Or_Seq => 119, - N_Star_Repeat_Seq => 122, - N_Goto_Repeat_Seq => 125, - N_Plus_Repeat_Seq => 126, - N_Equal_Repeat_Seq => 129, - N_Paren_Bool => 133, - N_Not_Bool => 137, - N_And_Bool => 142, - N_Or_Bool => 147, - N_Imp_Bool => 152, - N_HDL_Expr => 154, - N_HDL_Bool => 159, - N_False => 159, - N_True => 159, - N_EOS => 162, - N_Name => 164, - N_Name_Decl => 166, - N_Number => 167 + N_Log_Equiv_Prop => 66, + N_Next => 69, + N_Next_A => 73, + N_Next_E => 77, + N_Next_Event => 81, + N_Next_Event_A => 86, + N_Next_Event_E => 91, + N_Abort => 93, + N_Until => 97, + N_Before => 101, + N_Or_Prop => 103, + N_And_Prop => 105, + N_Paren_Prop => 106, + N_Braced_SERE => 107, + N_Concat_SERE => 109, + N_Fusion_SERE => 111, + N_Within_SERE => 113, + N_Clocked_SERE => 115, + N_Match_And_Seq => 117, + N_And_Seq => 119, + N_Or_Seq => 121, + N_Star_Repeat_Seq => 124, + N_Goto_Repeat_Seq => 127, + N_Plus_Repeat_Seq => 128, + N_Equal_Repeat_Seq => 131, + N_Paren_Bool => 135, + N_Not_Bool => 139, + N_And_Bool => 144, + N_Or_Bool => 149, + N_Imp_Bool => 154, + N_Equiv_Bool => 159, + N_HDL_Expr => 161, + N_HDL_Bool => 166, + N_False => 166, + N_True => 166, + N_EOS => 169, + N_Name => 171, + N_Name_Decl => 173, + N_Number => 174 ); function Get_Fields (K : Nkind) return Fields_Array @@ -1063,6 +1078,7 @@ package body PSL.Nodes_Meta is begin case K is when N_Log_Imp_Prop + | N_Log_Equiv_Prop | N_Until | N_Before | N_Or_Prop @@ -1075,7 +1091,8 @@ package body PSL.Nodes_Meta is | N_Or_Seq | N_And_Bool | N_Or_Bool - | N_Imp_Bool => + | N_Imp_Bool + | N_Equiv_Bool => return True; when others => return False; @@ -1086,6 +1103,7 @@ package body PSL.Nodes_Meta is begin case K is when N_Log_Imp_Prop + | N_Log_Equiv_Prop | N_Until | N_Before | N_Or_Prop @@ -1098,7 +1116,8 @@ package body PSL.Nodes_Meta is | N_Or_Seq | N_And_Bool | N_Or_Bool - | N_Imp_Bool => + | N_Imp_Bool + | N_Equiv_Bool => return True; when others => return False; @@ -1239,6 +1258,7 @@ package body PSL.Nodes_Meta is | N_And_Bool | N_Or_Bool | N_Imp_Bool + | N_Equiv_Bool | N_HDL_Bool | N_EOS => return True; @@ -1255,6 +1275,7 @@ package body PSL.Nodes_Meta is | N_And_Bool | N_Or_Bool | N_Imp_Bool + | N_Equiv_Bool | N_HDL_Bool | N_EOS => return True; @@ -1287,6 +1308,7 @@ package body PSL.Nodes_Meta is | N_And_Bool | N_Or_Bool | N_Imp_Bool + | N_Equiv_Bool | N_HDL_Bool => return True; when others => diff --git a/src/psl/psl-qm.adb b/src/psl/psl-qm.adb index 722577018..100900212 100644 --- a/src/psl/psl-qm.adb +++ b/src/psl/psl-qm.adb @@ -275,6 +275,22 @@ package body PSL.QM is return Build_Primes_And (Build_Primes (Get_Left (N), False), Build_Primes (Get_Right (N), True)); end if; + when N_Equiv_Bool => + if not Negate then + -- a <-> b <-> (a && b) || (!a && !b) + return Build_Primes_Or + (Build_Primes_And (Build_Primes (Get_Left (N), False), + Build_Primes (Get_Right (N), False)), + Build_Primes_And (Build_Primes (Get_Left (N), True), + Build_Primes (Get_Right (N), True))); + else + -- !(a <-> b) <-> (!a && b) || (a && !b) + return Build_Primes_Or + (Build_Primes_And (Build_Primes (Get_Left (N), True), + Build_Primes (Get_Right (N), False)), + Build_Primes_And (Build_Primes (Get_Left (N), False), + Build_Primes (Get_Right (N), True))); + end if; when others => Error_Kind ("build_primes", N); end case; diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb index 33c41697f..ad71ccd74 100644 --- a/src/psl/psl-rewrites.adb +++ b/src/psl/psl-rewrites.adb @@ -103,8 +103,9 @@ package body PSL.Rewrites is Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); return N; when N_And_Bool - | N_Or_Bool - | N_Imp_Bool => + | N_Or_Bool + | N_Imp_Bool + | N_Equiv_Bool => Set_Left (N, Rewrite_Boolean (Get_Left (N))); Set_Right (N, Rewrite_Boolean (Get_Right (N))); return N; diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb index dc677cb21..f7b615519 100644 --- a/src/psl/psl-subsets.adb +++ b/src/psl/psl-subsets.adb @@ -93,8 +93,8 @@ package body PSL.Subsets is when N_Hdl_Mod_Name => null; when N_Vunit - | N_Vmode - | N_Vprop => + | N_Vmode + | N_Vprop => declare Item : Node; begin @@ -107,32 +107,32 @@ package body PSL.Subsets is when N_Name_Decl => null; when N_Assert_Directive - | N_Property_Declaration => + | N_Property_Declaration => Check_Simple (Get_Property (N)); when N_Endpoint_Declaration - | N_Sequence_Declaration => + | N_Sequence_Declaration => Check_Simple (Get_Sequence (N)); when N_Clock_Event => Check_Simple (Get_Property (N)); Check_Simple (Get_Boolean (N)); when N_Always - | N_Never - | N_Eventually - | N_Strong => + | N_Never + | N_Eventually + | N_Strong => Check_Simple (Get_Property (N)); when N_Braced_SERE - | N_Clocked_SERE => + | N_Clocked_SERE => Check_Simple (Get_SERE (N)); when N_Concat_SERE - | N_Fusion_SERE - | N_Within_SERE => + | N_Fusion_SERE + | N_Within_SERE => Check_Simple (Get_Left (N)); Check_Simple (Get_Right (N)); when N_Name => null; when N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Equal_Repeat_Seq => + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq => declare N2 : constant Node := Get_Sequence (N); begin @@ -143,28 +143,30 @@ package body PSL.Subsets is when N_Plus_Repeat_Seq => Check_Simple (Get_Sequence (N)); when N_Match_And_Seq - | N_And_Seq - | N_Or_Seq => + | N_And_Seq + | N_Or_Seq => Check_Simple (Get_Left (N)); Check_Simple (Get_Right (N)); when N_Imp_Seq - | N_Overlap_Imp_Seq => + | N_Overlap_Imp_Seq => Check_Simple (Get_Sequence (N)); Check_Simple (Get_Property (N)); when N_Log_Imp_Prop - | N_Until - | N_Before - | N_Or_Prop - | N_And_Prop - | N_And_Bool - | N_Or_Bool - | N_Imp_Bool => + | N_Log_Equiv_Prop + | N_Until + | N_Before + | N_Or_Prop + | N_And_Prop + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool + | N_Equiv_Bool => Check_Simple (Get_Left (N)); Check_Simple (Get_Right (N)); when N_Next - | N_Next_A - | N_Next_E - | N_Paren_Prop => + | N_Next_A + | N_Next_E + | N_Paren_Prop => Check_Simple (Get_Property (N)); when N_Next_Event | N_Next_Event_A diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb index b664ec5c2..e50367648 100644 --- a/src/vhdl/vhdl-parse_psl.adb +++ b/src/vhdl/vhdl-parse_psl.adb @@ -679,12 +679,12 @@ package body Vhdl.Parse_Psl is begin case Get_Kind (N) is when N_Sequence_Instance - | N_Star_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Braced_SERE - | N_Clocked_SERE => + | N_Star_Repeat_Seq + | N_Plus_Repeat_Seq + | N_Equal_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Braced_SERE + | N_Clocked_SERE => return N; when N_And_Prop => Res := Create_Node (N_And_Seq); @@ -699,52 +699,54 @@ package body Vhdl.Parse_Psl is Set_Right (N, Property_To_Sequence (Get_Right (N))); return N; when N_Clock_Event - | N_Always - | N_Never - | N_Eventually - | N_Until - | N_Property_Parameter - | N_Property_Instance - | N_Endpoint_Instance - | N_Strong - | N_Abort - | N_Next_Event_E - | N_Next_Event_A - | N_Next_Event - | N_Next_E - | N_Next_A - | N_Next - | N_Log_Imp_Prop - | N_Paren_Prop => + | N_Always + | N_Never + | N_Eventually + | N_Until + | N_Property_Parameter + | N_Property_Instance + | N_Endpoint_Instance + | N_Strong + | N_Abort + | N_Next_Event_E + | N_Next_Event_A + | N_Next_Event + | N_Next_E + | N_Next_A + | N_Next + | N_Log_Imp_Prop + | N_Log_Equiv_Prop + | N_Paren_Prop => Error_Msg_Parse (+N, "construct not allowed in sequences"); return N; when N_Const_Parameter - | N_Boolean_Parameter - | N_Sequence_Parameter - | N_Actual - | N_And_Seq - | N_Or_Seq - | N_Imp_Seq - | N_Overlap_Imp_Seq - | N_Match_And_Seq - | N_Imp_Bool - | N_Or_Bool - | N_And_Bool - | N_Not_Bool - | N_Paren_Bool - | N_Fusion_SERE - | N_HDL_Expr - | N_HDL_Bool - | N_Hdl_Mod_Name - | N_Concat_SERE - | N_Within_SERE - | N_False - | N_True - | N_Number - | N_Name_Decl - | N_Name - | N_EOS - | N_Error => + | N_Boolean_Parameter + | N_Sequence_Parameter + | N_Actual + | N_And_Seq + | N_Or_Seq + | N_Imp_Seq + | N_Equiv_Bool + | N_Overlap_Imp_Seq + | N_Match_And_Seq + | N_Imp_Bool + | N_Or_Bool + | N_And_Bool + | N_Not_Bool + | N_Paren_Bool + | N_Fusion_SERE + | N_HDL_Expr + | N_HDL_Bool + | N_Hdl_Mod_Name + | N_Concat_SERE + | N_Within_SERE + | N_False + | N_True + | N_Number + | N_Name_Decl + | N_Name + | N_EOS + | N_Error => return N; when N_Vmode | N_Vunit @@ -812,6 +814,7 @@ package body Vhdl.Parse_Psl is loop case Current_Token is when Tok_Minus_Greater => + -- -> if Prio > Prio_Bool_Imp then return Res; end if; @@ -820,6 +823,15 @@ package body Vhdl.Parse_Psl is Scan; Set_Right (N, Parse_FL_Property (Prio_Bool_Imp)); Res := N; + when Tok_Equiv_Arrow => + if Prio > Prio_Bool_Imp then + return Res; + end if; + N := Create_Node_Loc (N_Log_Equiv_Prop); + Set_Left (N, Res); + Scan; + Set_Right (N, Parse_FL_Property (Prio_Bool_Imp)); + Res := N; when Tok_Bar_Arrow => if Prio > Prio_Seq_Imp then return Res; diff --git a/src/vhdl/vhdl-scanner.adb b/src/vhdl/vhdl-scanner.adb index bdda2340f..fba0dab54 100644 --- a/src/vhdl/vhdl-scanner.adb +++ b/src/vhdl/vhdl-scanner.adb @@ -2257,6 +2257,14 @@ package body Vhdl.Scanner is when '<' => Current_Token := Tok_Double_Less; Pos := Pos + 2; + when '-' => + if Flag_Psl and then Source (Pos + 2) = '>' then + Current_Token := Tok_Equiv_Arrow; + Pos := Pos + 3; + else + Current_Token := Tok_Less; + Pos := Pos + 1; + end if; when others => Current_Token := Tok_Less; Pos := Pos + 1; diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb index e4b3554fd..0e077b8c9 100644 --- a/src/vhdl/vhdl-sem_psl.adb +++ b/src/vhdl/vhdl-sem_psl.adb @@ -552,7 +552,7 @@ package body Vhdl.Sem_Psl is when N_Braced_SERE => return Sem_Sequence (Prop); when N_Always - | N_Never => + | N_Never => -- By extension, clock_event is allowed within outermost -- always/never. Sem_Property (Prop, Top); @@ -572,15 +572,16 @@ package body Vhdl.Sem_Psl is Sem_Boolean (Prop); return Prop; when N_Until - | N_Before => + | N_Before => Res := Sem_Property (Get_Left (Prop)); Set_Left (Prop, Res); Res := Sem_Property (Get_Right (Prop)); Set_Right (Prop, Res); return Prop; when N_Log_Imp_Prop - | N_And_Prop - | N_Or_Prop => + | N_Log_Equiv_Prop + | N_And_Prop + | N_Or_Prop => declare L, R : PSL_Node; begin @@ -598,6 +599,8 @@ package body Vhdl.Sem_Psl is return Reduce_Logic_Binary_Node (Prop, N_Or_Bool); when N_Log_Imp_Prop => return Reduce_Logic_Binary_Node (Prop, N_Imp_Bool); + when N_Log_Equiv_Prop => + return Reduce_Logic_Binary_Node (Prop, N_Equiv_Bool); when others => Error_Kind ("psl.sem_property(log)", Prop); end case; diff --git a/src/vhdl/vhdl-tokens.adb b/src/vhdl/vhdl-tokens.adb index 0242808bf..c4550af82 100644 --- a/src/vhdl/vhdl-tokens.adb +++ b/src/vhdl/vhdl-tokens.adb @@ -430,6 +430,8 @@ package body Vhdl.Tokens is return "|=>"; when Tok_Minus_Greater => return "->"; + when Tok_Equiv_Arrow => + return "<->"; when Tok_Arobase => return "@"; diff --git a/src/vhdl/vhdl-tokens.ads b/src/vhdl/vhdl-tokens.ads index e35a3a4e4..373b92acc 100644 --- a/src/vhdl/vhdl-tokens.ads +++ b/src/vhdl/vhdl-tokens.ads @@ -100,6 +100,7 @@ package Vhdl.Tokens is Tok_Bar_Arrow, -- |-> Tok_Bar_Double_Arrow, -- |=> Tok_Minus_Greater, -- -> + Tok_Equiv_Arrow, -- <-> Tok_Arobase, -- @ -- multiplying operator -- cgit v1.2.3