diff options
| -rw-r--r-- | src/psl/psl-nodes.adb | 6 | ||||
| -rw-r--r-- | src/psl/psl-nodes.adb.in | 4 | ||||
| -rw-r--r-- | src/psl/psl-nodes.ads | 18 | ||||
| -rw-r--r-- | src/psl/psl-nodes_meta.adb | 72 | ||||
| -rw-r--r-- | src/psl/psl-subsets.adb | 6 | ||||
| -rw-r--r-- | src/vhdl/vhdl-parse_psl.adb | 43 | ||||
| -rw-r--r-- | src/vhdl/vhdl-sem_psl.adb | 93 |
7 files changed, 179 insertions, 63 deletions
diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb index d7de320a8..99b449d22 100644 --- a/src/psl/psl-nodes.adb +++ b/src/psl/psl-nodes.adb @@ -325,6 +325,7 @@ package body PSL.Nodes is case Get_Kind (N) is when N_And_Prop | N_Or_Prop + | N_Paren_Prop | N_Log_Imp_Prop | N_Always | N_Never @@ -372,7 +373,8 @@ package body PSL.Nodes is | N_Imp_Bool | N_False | N_True - | N_Boolean_Parameter => + | N_Boolean_Parameter + | N_Paren_Bool => return Type_Boolean; when N_Number | N_Const_Parameter => @@ -439,6 +441,7 @@ package body PSL.Nodes is | N_Before | N_Or_Prop | N_And_Prop + | N_Paren_Prop | N_Braced_SERE | N_Concat_SERE | N_Fusion_SERE @@ -451,6 +454,7 @@ package body PSL.Nodes is | N_Goto_Repeat_Seq | N_Plus_Repeat_Seq | N_Equal_Repeat_Seq + | N_Paren_Bool | N_Not_Bool | N_And_Bool | N_Or_Bool diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in index 220ffee71..3c7888800 100644 --- a/src/psl/psl-nodes.adb.in +++ b/src/psl/psl-nodes.adb.in @@ -325,6 +325,7 @@ package body PSL.Nodes is case Get_Kind (N) is when N_And_Prop | N_Or_Prop + | N_Paren_Prop | N_Log_Imp_Prop | N_Always | N_Never @@ -372,7 +373,8 @@ package body PSL.Nodes is | N_Imp_Bool | N_False | N_True - | N_Boolean_Parameter => + | N_Boolean_Parameter + | N_Paren_Bool => return Type_Boolean; when N_Number | N_Const_Parameter => diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads index ec3022c35..0b11d0641 100644 --- a/src/psl/psl-nodes.ads +++ b/src/psl/psl-nodes.ads @@ -67,6 +67,7 @@ package PSL.Nodes is N_Before, N_Or_Prop, N_And_Prop, + N_Paren_Prop, -- Sequences/SERE. N_Braced_SERE, @@ -85,6 +86,7 @@ package PSL.Nodes is N_Equal_Repeat_Seq, -- Boolean layer. + N_Paren_Bool, N_Not_Bool, N_And_Bool, N_Or_Bool, @@ -100,7 +102,7 @@ package PSL.Nodes is ); for Nkind'Size use 8; - subtype N_Booleans is Nkind range N_Not_Bool .. N_True; + subtype N_Booleans is Nkind range N_Paren_Bool .. N_True; subtype N_Sequences is Nkind range N_Braced_SERE .. N_Equal_Repeat_Seq; type PSL_Types is @@ -335,6 +337,10 @@ package PSL.Nodes is -- -- Get/Set_Right (Field2) + -- N_Paren_Prop (Short) + -- + -- Get/Set_Property (Field4) + -- N_Until (Short) -- N_Before (Short) -- @@ -378,6 +384,16 @@ package PSL.Nodes is -- -- Get/Set_Hash_Link (Field6) + -- N_Paren_Bool (Short) + -- + -- Get/Set_Presence (State1) + -- + -- Get/Set_Boolean (Field3) + -- + -- Get/Set_Hash (Field5) + -- + -- Get/Set_Hash_Link (Field6) + -- N_Not_Bool (Short) -- -- Get/Set_Presence (State1) diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb index 04b42aceb..f33ac5122 100644 --- a/src/psl/psl-nodes_meta.adb +++ b/src/psl/psl-nodes_meta.adb @@ -203,6 +203,8 @@ package body PSL.Nodes_Meta is return "or_prop"; when N_And_Prop => return "and_prop"; + when N_Paren_Prop => + return "paren_prop"; when N_Braced_SERE => return "braced_sere"; when N_Concat_SERE => @@ -227,6 +229,8 @@ package body PSL.Nodes_Meta is return "plus_repeat_seq"; when N_Equal_Repeat_Seq => return "equal_repeat_seq"; + when N_Paren_Bool => + return "paren_bool"; when N_Not_Bool => return "not_bool"; when N_And_Bool => @@ -464,6 +468,8 @@ package body PSL.Nodes_Meta is -- N_And_Prop Field_Left, Field_Right, + -- N_Paren_Prop + Field_Property, -- N_Braced_SERE Field_SERE, -- N_Concat_SERE @@ -501,6 +507,11 @@ package body PSL.Nodes_Meta is Field_Sequence, Field_Low_Bound, Field_High_Bound, + -- N_Paren_Bool + Field_Hash, + Field_Presence, + Field_Boolean, + Field_Hash_Link, -- N_Not_Bool Field_Hash, Field_Presence, @@ -584,29 +595,31 @@ package body PSL.Nodes_Meta is N_Before => 99, N_Or_Prop => 101, N_And_Prop => 103, - N_Braced_SERE => 104, - N_Concat_SERE => 106, - N_Fusion_SERE => 108, - N_Within_SERE => 110, - N_Clocked_SERE => 112, - N_Match_And_Seq => 114, - N_And_Seq => 116, - N_Or_Seq => 118, - N_Star_Repeat_Seq => 121, - N_Goto_Repeat_Seq => 124, - N_Plus_Repeat_Seq => 125, - N_Equal_Repeat_Seq => 128, - N_Not_Bool => 132, - N_And_Bool => 137, - N_Or_Bool => 142, - N_Imp_Bool => 147, - N_HDL_Expr => 152, - N_False => 152, - N_True => 152, - N_EOS => 155, - N_Name => 157, - N_Name_Decl => 159, - N_Number => 160 + 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 => 157, + N_False => 157, + N_True => 157, + N_EOS => 160, + N_Name => 162, + N_Name_Decl => 164, + N_Number => 165 ); function Get_Fields (K : Nkind) return Fields_Array @@ -1007,7 +1020,8 @@ package body PSL.Nodes_Meta is | N_Next_Event | N_Next_Event_A | N_Next_Event_E - | N_Abort => + | N_Abort + | N_Paren_Prop => return True; when others => return False; @@ -1178,6 +1192,7 @@ package body PSL.Nodes_Meta is | N_Next_Event_E | N_Abort | N_Clocked_SERE + | N_Paren_Bool | N_Not_Bool => return True; when others => @@ -1198,7 +1213,8 @@ package body PSL.Nodes_Meta is function Has_Hash (K : Nkind) return Boolean is begin case K is - when N_Not_Bool + when N_Paren_Bool + | N_Not_Bool | N_And_Bool | N_Or_Bool | N_Imp_Bool @@ -1213,7 +1229,8 @@ package body PSL.Nodes_Meta is function Has_Hash_Link (K : Nkind) return Boolean is begin case K is - when N_Not_Bool + when N_Paren_Bool + | N_Not_Bool | N_And_Bool | N_Or_Bool | N_Imp_Bool @@ -1239,7 +1256,8 @@ package body PSL.Nodes_Meta is function Has_Presence (K : Nkind) return Boolean is begin case K is - when N_Not_Bool + when N_Paren_Bool + | N_Not_Bool | N_And_Bool | N_Or_Bool | N_Imp_Bool diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb index 8aaf2b063..95f8d781c 100644 --- a/src/psl/psl-subsets.adb +++ b/src/psl/psl-subsets.adb @@ -163,7 +163,8 @@ package body PSL.Subsets is Check_Simple (Get_Right (N)); when N_Next | N_Next_A - | N_Next_E => + | N_Next_E + | N_Paren_Prop => Check_Simple (Get_Property (N)); when N_Next_Event | N_Next_Event_A @@ -171,7 +172,8 @@ package body PSL.Subsets is | N_Abort => Check_Simple (Get_Boolean (N)); Check_Simple (Get_Property (N)); - when N_Not_Bool => + when N_Not_Bool + | N_Paren_Bool => Check_Simple (Get_Boolean (N)); when N_Const_Parameter | N_Sequence_Parameter diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb index 13b3a2d02..630339c79 100644 --- a/src/vhdl/vhdl-parse_psl.adb +++ b/src/vhdl/vhdl-parse_psl.adb @@ -378,7 +378,19 @@ package body Vhdl.Parse_Psl is when Tok_Brack_Star => return Parse_Maybe_Count (N_Star_Repeat_Seq, Null_Node); when Tok_Left_Paren => - Res := Parse_Parenthesis_Boolean; + if Parse.Flag_Parse_Parenthesis then + Res := Create_Node_Loc (N_Paren_Bool); + -- Skip '('. + Scan; + Set_Boolean (Res, Parse_Psl_Boolean); + if Current_Token = Tok_Right_Paren then + Scan; + else + Error_Msg_Parse ("missing matching ')'"); + end if; + else + Res := Parse_Parenthesis_Boolean; + end if; if Current_Token = Tok_Or or else Current_Token = Tok_And then @@ -426,7 +438,9 @@ package body Vhdl.Parse_Psl is -- precond: '(' -- postcond: next token - function Parse_Parenthesis_FL_Property return Node is + function Parse_Parenthesis_FL_Property return Node + is + Prop : Node; Res : Node; Loc : Location_Type; begin @@ -435,10 +449,15 @@ package body Vhdl.Parse_Psl is Error_Msg_Parse ("'(' expected around property"); return Parse_FL_Property (Prio_Lowest); else + if Parse.Flag_Parse_Parenthesis then + Res := Create_Node_Loc (N_Paren_Prop); + end if; + -- Skip '('. Scan; - Res := Parse_FL_Property (Prio_Lowest); + Prop := Parse_FL_Property (Prio_Lowest); + if Current_Token = Tok_Right_Paren then -- Skip ')'. Scan; @@ -447,16 +466,22 @@ package body Vhdl.Parse_Psl is & Image (Loc, False)); end if; - if Get_Kind (Res) = N_HDL_Expr then + if Get_Kind (Prop) = N_HDL_Expr then declare N : Vhdl_Node; begin - N := Psl_To_Vhdl (Res); + N := Psl_To_Vhdl (Prop); N := Parse.Parse_Binary_Expression (N, Parse.Prio_Expression); - Res := Vhdl_To_Psl (N); + Prop := Vhdl_To_Psl (N); end; end if; - return Res; + + if Parse.Flag_Parse_Parenthesis then + Set_Property (Res, Prop); + return Res; + else + return Prop; + end if; end if; end Parse_Parenthesis_FL_Property; @@ -618,7 +643,8 @@ package body Vhdl.Parse_Psl is | N_Next_E | N_Next_A | N_Next - | N_Log_Imp_Prop => + | N_Log_Imp_Prop + | N_Paren_Prop => Error_Msg_Parse (+N, "construct not allowed in sequences"); return N; when N_Const_Parameter @@ -639,6 +665,7 @@ package body Vhdl.Parse_Psl is | N_Or_Bool | N_And_Bool | N_Not_Bool + | N_Paren_Bool | N_Fusion_SERE | N_HDL_Expr | N_Hdl_Mod_Name diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb index 767cd0c01..28541e7cc 100644 --- a/src/vhdl/vhdl-sem_psl.adb +++ b/src/vhdl/vhdl-sem_psl.adb @@ -251,7 +251,8 @@ package body Vhdl.Sem_Psl is -- Used by Sem_Property to rewrite a property logical operator to a -- boolean logical operator. - function Reduce_Logic_Node (Prop : Node; Bool_Kind : Nkind) return Node + function Reduce_Logic_Binary_Node (Prop : Node; Bool_Kind : Nkind) + return Node is Res : Node; begin @@ -261,7 +262,19 @@ package body Vhdl.Sem_Psl is Set_Right (Res, Get_Right (Prop)); Free_Node (Prop); return Res; - end Reduce_Logic_Node; + end Reduce_Logic_Binary_Node; + + function Reduce_Logic_Unary_Node (Prop : Node; Bool_Kind : Nkind) + return Node + is + Res : Node; + begin + Res := Create_Node (Bool_Kind); + Set_Location (Res, Get_Location (Prop)); + Set_Boolean (Res, Get_Property (Prop)); + Free_Node (Prop); + return Res; + end Reduce_Logic_Unary_Node; function Sem_Sequence (Seq : Node) return Node is @@ -352,7 +365,6 @@ package body Vhdl.Sem_Psl is function Sem_Property (Prop : Node; Top : Boolean := False) return Node is Res : Node; - L, R : Node; begin case Get_Kind (Prop) is when N_Braced_SERE => @@ -387,31 +399,49 @@ package body Vhdl.Sem_Psl is when N_Log_Imp_Prop | N_And_Prop | N_Or_Prop => - L := Sem_Property (Get_Left (Prop)); - Set_Left (Prop, L); - R := Sem_Property (Get_Right (Prop)); - Set_Right (Prop, R); - if Get_Psl_Type (L) = Type_Boolean - and then Get_Psl_Type (R) = Type_Boolean - then - case Get_Kind (Prop) is - when N_And_Prop => - return Reduce_Logic_Node (Prop, N_And_Bool); - when N_Or_Prop => - return Reduce_Logic_Node (Prop, N_Or_Bool); - when N_Log_Imp_Prop => - return Reduce_Logic_Node (Prop, N_Imp_Bool); - when others => - Error_Kind ("psl.sem_property(log)", Prop); - end case; - end if; - return Prop; + declare + L, R : Node; + begin + L := Sem_Property (Get_Left (Prop)); + Set_Left (Prop, L); + R := Sem_Property (Get_Right (Prop)); + Set_Right (Prop, R); + if Get_Psl_Type (L) = Type_Boolean + and then Get_Psl_Type (R) = Type_Boolean + then + case Get_Kind (Prop) is + when N_And_Prop => + return Reduce_Logic_Binary_Node (Prop, N_And_Bool); + when N_Or_Prop => + return Reduce_Logic_Binary_Node (Prop, N_Or_Bool); + when N_Log_Imp_Prop => + return Reduce_Logic_Binary_Node (Prop, N_Imp_Bool); + when others => + Error_Kind ("psl.sem_property(log)", Prop); + end case; + else + return Prop; + end if; + end; when N_Overlap_Imp_Seq | N_Imp_Seq => Res := Sem_Sequence (Get_Sequence (Prop)); Set_Sequence (Prop, Res); Sem_Property (Prop); return Prop; + when N_Paren_Prop => + declare + Op : Node; + begin + Op := Get_Property (Prop); + Op := Sem_Property (Op); + Set_Property (Prop, Op); + if Get_Psl_Type (Op) = Type_Boolean then + return Reduce_Logic_Unary_Node (Prop, N_Paren_Bool); + else + return Prop; + end if; + end; when N_Next => Sem_Number (Prop); Sem_Property (Prop); @@ -588,6 +618,23 @@ package body Vhdl.Sem_Psl is return Rewrite_Dyadic_Operator (Prop, Iir_Kind_Or_Operator); when N_Not_Bool => return Rewrite_Monadic_Operator (Prop, Iir_Kind_Not_Operator); + when N_Paren_Bool => + declare + Expr : constant PSL_Node := Get_Boolean (Prop); + Hexpr : Iir; + Res : Iir; + begin + Res := Create_Iir (Iir_Kind_Parenthesis_Expression); + Set_Location (Res, Get_Location (Prop)); + if Get_Kind (Expr) = N_HDL_Expr then + Hexpr := Get_HDL_Node (Expr); + Set_Expression (Res, Hexpr); + Set_Type (Res, Get_Type (Hexpr)); + else + Set_Expression (Res, Rewrite_As_Boolean_Expression (Expr)); + end if; + return Res; + end; when others => Error_Kind ("rewrite_as_boolean_expression", Prop); end case; @@ -623,7 +670,7 @@ package body Vhdl.Sem_Psl is case Get_Kind (Expr) is when N_HDL_Expr => return True; - when N_And_Bool | N_Or_Bool | N_Not_Bool => + when N_And_Bool | N_Or_Bool | N_Not_Bool | N_Paren_Bool => return True; when others => return False; |