diff options
| -rw-r--r-- | src/psl/psl-nodes.ads | 15 | ||||
| -rw-r--r-- | src/psl/psl-nodes_meta.adb | 10 | ||||
| -rw-r--r-- | src/psl/psl-rewrites.adb | 22 | ||||
| -rw-r--r-- | src/vhdl/vhdl-parse_psl.adb | 86 | ||||
| -rw-r--r-- | src/vhdl/vhdl-prints.adb | 23 | ||||
| -rw-r--r-- | src/vhdl/vhdl-sem_psl.adb | 20 |
6 files changed, 118 insertions, 58 deletions
diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads index 93ecd20f5..07d4f7df6 100644 --- a/src/psl/psl-nodes.ads +++ b/src/psl/psl-nodes.ads @@ -81,8 +81,8 @@ package PSL.Nodes is N_Star_Repeat_Seq, N_Goto_Repeat_Seq, - N_Plus_Repeat_Seq, -- [+] - N_Equal_Repeat_Seq, + N_Plus_Repeat_Seq, -- [+] + N_Equal_Repeat_Seq, -- [= ] -- Boolean layer. N_Paren_Bool, @@ -276,8 +276,6 @@ package PSL.Nodes is -- Get/Set_Right (Field2) -- N_Star_Repeat_Seq (Short) - -- N_Goto_Repeat_Seq (Short) - -- N_Equal_Repeat_Seq (Short) -- -- Note: can be null_node for star_repeat_seq. -- Get/Set_Sequence (Field3) @@ -286,6 +284,15 @@ package PSL.Nodes is -- -- Get/Set_High_Bound (Field2) + -- N_Equal_Repeat_Seq (Short) + -- N_Goto_Repeat_Seq (Short) + -- + -- Get/Set_Boolean (Field3) + -- + -- Get/Set_Low_Bound (Field1) + -- + -- Get/Set_High_Bound (Field2) + -- N_Plus_Repeat_Seq (Short) -- -- Note: can be null_node. diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb index 4d229b5cd..8486c177f 100644 --- a/src/psl/psl-nodes_meta.adb +++ b/src/psl/psl-nodes_meta.adb @@ -510,13 +510,13 @@ package body PSL.Nodes_Meta is Field_Low_Bound, Field_High_Bound, -- N_Goto_Repeat_Seq - Field_Sequence, + Field_Boolean, Field_Low_Bound, Field_High_Bound, -- N_Plus_Repeat_Seq Field_Sequence, -- N_Equal_Repeat_Seq - Field_Sequence, + Field_Boolean, Field_Low_Bound, Field_High_Bound, -- N_Paren_Bool @@ -1130,9 +1130,7 @@ package body PSL.Nodes_Meta is | N_Imp_Seq | N_Overlap_Imp_Seq | N_Star_Repeat_Seq - | N_Goto_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Equal_Repeat_Seq => + | N_Plus_Repeat_Seq => return True; when others => return False; @@ -1224,6 +1222,8 @@ package body PSL.Nodes_Meta is | N_Next_Event_E | N_Abort | N_Clocked_SERE + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq | N_Paren_Bool | N_Not_Bool => return True; diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb index be9477088..7568ab8fc 100644 --- a/src/psl/psl-rewrites.adb +++ b/src/psl/psl-rewrites.adb @@ -188,12 +188,12 @@ package body PSL.Rewrites is end if; end Rewrite_Star_Repeat_Seq; - function Rewrite_Goto_Repeat_Seq (Seq : Node; - Lo, Hi : Node) return Node is + function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Node) return Node + is Res : Node; begin -- b[->] --> {(~b)[*];b} - Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); + Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B); if Lo = Null_Node then return Res; @@ -203,12 +203,12 @@ package body PSL.Rewrites is return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); end Rewrite_Goto_Repeat_Seq; - function Rewrite_Goto_Repeat_Seq (Seq : Node; - Lo, Hi : Uns32) return Node is + function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Uns32) return Node + is Res : Node; begin -- b[->] --> {(~b)[*];b} - Res := Build_Concat (Build_Star (Build_Bool_Not (Seq)), Seq); + Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B); -- b[->l:h] --> {b[->]}[*l:h] return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); @@ -216,13 +216,13 @@ package body PSL.Rewrites is function Rewrite_Equal_Repeat_Seq (N : Node) return Node is - Seq : constant Node := Get_Sequence (N); + B : constant Node := Get_Boolean (N); Lo : constant Node := Get_Low_Bound (N); Hi : constant Node := Get_High_Bound (N); begin -- b[=l:h] --> {b[->l:h]};(~b)[*] - return Build_Concat (Rewrite_Goto_Repeat_Seq (Seq, Lo, Hi), - Build_Star (Build_Bool_Not (Seq))); + return Build_Concat (Rewrite_Goto_Repeat_Seq (B, Lo, Hi), + Build_Star (Build_Bool_Not (B))); end Rewrite_Equal_Repeat_Seq; function Rewrite_Within (N : Node) return Node is @@ -291,10 +291,10 @@ package body PSL.Rewrites is return N; when N_Goto_Repeat_Seq => return Rewrite_Goto_Repeat_Seq - (Rewrite_SERE (Get_Sequence (N)), + (Rewrite_SERE (Get_Boolean (N)), Get_Low_Bound (N), Get_High_Bound (N)); when N_Equal_Repeat_Seq => - Set_Sequence (N, Rewrite_SERE (Get_Sequence (N))); + Set_Boolean (N, Rewrite_SERE (Get_Boolean (N))); return Rewrite_Equal_Repeat_Seq (N); when N_Braced_SERE => return Rewrite_SERE (Get_SERE (N)); diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb index eaabd852b..b7d6c1df4 100644 --- a/src/vhdl/vhdl-parse_psl.adb +++ b/src/vhdl/vhdl-parse_psl.adb @@ -337,23 +337,26 @@ package body Vhdl.Parse_Psl is end Parse_Braced_SERE; -- Parse [ Count ] ']' - function Parse_Maybe_Count (Kind : Nkind; Seq : Node) return Node + function Parse_Brack_Star (Seq : Node) return Node is - N : Node; + Res : Node; begin - N := Create_Node_Loc (Kind); - Set_Sequence (N, Seq); + Res := Create_Node_Loc (N_Star_Repeat_Seq); + Set_Sequence (Res, Seq); + + -- Skip '[->' Scan; + if Current_Token /= Tok_Right_Bracket then - Parse_Count (N); + Parse_Count (Res); end if; if Current_Token /= Tok_Right_Bracket then Error_Msg_Parse ("missing ']'"); else Scan; end if; - return N; - end Parse_Maybe_Count; + return Res; + end Parse_Brack_Star; procedure Parse_Bracket_Range (N : Node) is begin @@ -396,6 +399,44 @@ package body Vhdl.Parse_Psl is end if; end Parse_Bracket_Number; + function Parse_Brack_Equal (Left : Node) return Node + is + Res : Node; + begin + Res := Create_Node_Loc (N_Equal_Repeat_Seq); + Set_Boolean (Res, Left); + + -- Skip '[=' + Scan; + Parse_Count (Res); + if Current_Token /= Tok_Right_Bracket then + Error_Msg_Parse ("missing ']'"); + else + Scan; + end if; + return Res; + end Parse_Brack_Equal; + + function Parse_Brack_Arrow (Left : Node) return Node + is + Res : Node; + begin + Res := Create_Node_Loc (N_Goto_Repeat_Seq); + Set_Boolean (Res, Left); + + -- Skip '[->' + Scan; + if Current_Token /= Tok_Right_Bracket then + Parse_Count (Res); + end if; + if Current_Token /= Tok_Right_Bracket then + Error_Msg_Parse ("missing ']'"); + else + Scan; + end if; + return Res; + end Parse_Brack_Arrow; + function Parse_Psl_Sequence_Or_SERE (Full_Hdl_Expr : Boolean) return Node is Res, N : Node; @@ -414,7 +455,7 @@ package body Vhdl.Parse_Psl is Res := N; end if; when Tok_Brack_Star => - return Parse_Maybe_Count (N_Star_Repeat_Seq, Null_Node); + return Parse_Brack_Star (Null_Node); when Tok_Left_Paren => if Parse.Flag_Parse_Parenthesis then Res := Create_Node_Loc (N_Paren_Bool); @@ -438,14 +479,24 @@ package body Vhdl.Parse_Psl is Res := Create_Node_Loc (N_Plus_Repeat_Seq); Scan; return Res; + when others => -- Repeated_SERE Res := Parse_Unary_Boolean (Full_Hdl_Expr); + + case Current_Token is + when Tok_Brack_Equal => + Res := Parse_Brack_Equal (Res); + when Tok_Brack_Arrow => + Res := Parse_Brack_Arrow (Res); + when others => + null; + end case; end case; loop case Current_Token is when Tok_Brack_Star => - Res := Parse_Maybe_Count (N_Star_Repeat_Seq, Res); + Res := Parse_Brack_Star (Res); when Tok_Brack_Plus_Brack => N := Create_Node_Loc (N_Plus_Repeat_Seq); Set_Sequence (N, Res); @@ -454,20 +505,11 @@ package body Vhdl.Parse_Psl is Scan; Res := N; when Tok_Brack_Arrow => - Res := Parse_Maybe_Count (N_Goto_Repeat_Seq, Res); + Error_Msg_Parse ("'[->' not allowed on a SERE"); + Res := Parse_Brack_Arrow (Res); when Tok_Brack_Equal => - N := Create_Node_Loc (N_Equal_Repeat_Seq); - Set_Sequence (N, Res); - - -- Skip '[=' - Scan; - Parse_Count (N); - if Current_Token /= Tok_Right_Bracket then - Error_Msg_Parse ("missing ']'"); - else - Scan; - end if; - Res := N; + Error_Msg_Parse ("'[=' not allowed on a SERE"); + Res := Parse_Brack_Equal (Res); when others => exit; end case; diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb index 6016c23e2..35a6f4958 100644 --- a/src/vhdl/vhdl-prints.adb +++ b/src/vhdl/vhdl-prints.adb @@ -2032,19 +2032,26 @@ package body Vhdl.Prints is Print_Sequence (Ctxt, Get_Right (N), Prio); end Print_Binary_Sequence; - procedure Print_Repeat_Sequence - (Ctxt : in out Ctxt_Class; Tok : Token_Type; N : PSL_Node) + procedure Print_Seq_Repeat_Sere (Ctxt : in out Ctxt_Class; N : PSL_Node) is - S : PSL_Node; + S : constant PSL_Node := Get_Sequence (N); begin - S := Get_Sequence (N); if S /= Null_PSL_Node then Print_Sequence (Ctxt, S, Prio_SERE_Repeat); end if; + Disp_Token (Ctxt, Tok_Brack_Star); + Print_Count (Ctxt, N); + Disp_Token (Ctxt, Tok_Right_Bracket); + end Print_Seq_Repeat_Sere; + + procedure Print_Bool_Repeat_Sere + (Ctxt : in out Ctxt_Class; Tok : Token_Type; N : PSL_Node) is + begin + Print_Expr (Ctxt, Get_Boolean (N)); Disp_Token (Ctxt, Tok); Print_Count (Ctxt, N); Disp_Token (Ctxt, Tok_Right_Bracket); - end Print_Repeat_Sequence; + end Print_Bool_Repeat_Sere; procedure Print_Sequence (Ctxt : in out Ctxt_Class; Seq : PSL_Node; @@ -2075,11 +2082,11 @@ package body Vhdl.Prints is when N_And_Seq => Print_Binary_Sequence (Ctxt, Tok_Ampersand, Seq, Prio); when N_Star_Repeat_Seq => - Print_Repeat_Sequence (Ctxt, Tok_Brack_Star, Seq); + Print_Seq_Repeat_Sere (Ctxt, Seq); when N_Goto_Repeat_Seq => - Print_Repeat_Sequence (Ctxt, Tok_Brack_Arrow, Seq); + Print_Bool_Repeat_Sere (Ctxt, Tok_Brack_Arrow, Seq); when N_Equal_Repeat_Seq => - Print_Repeat_Sequence (Ctxt, Tok_Brack_Equal, Seq); + Print_Bool_Repeat_Sere (Ctxt, Tok_Brack_Equal, Seq); when N_Plus_Repeat_Seq => Print_Sequence (Ctxt, Get_Sequence (Seq), Prio); Disp_Token (Ctxt, Tok_Brack_Plus_Brack); diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb index 7e1f805eb..f6be38207 100644 --- a/src/vhdl/vhdl-sem_psl.adb +++ b/src/vhdl/vhdl-sem_psl.adb @@ -435,20 +435,24 @@ package body Vhdl.Sem_Psl is Set_Right (Seq, R); return Seq; when N_Star_Repeat_Seq - | N_Plus_Repeat_Seq - | N_Equal_Repeat_Seq - | N_Goto_Repeat_Seq => + | N_Plus_Repeat_Seq => Res := Get_Sequence (Seq); if Res /= Null_PSL_Node then - Res := Sem_Sequence (Get_Sequence (Seq)); + Res := Sem_Sequence (Res); Set_Sequence (Seq, Res); end if; - -- TODO: Fix here if SERE is not of boolean type for - -- Equal Repeat and goto repeat!! + return Seq; + when N_Equal_Repeat_Seq + | N_Goto_Repeat_Seq => + Res := Get_Boolean (Seq); + if Res /= Null_PSL_Node then + Res := Sem_Boolean (Res); + Set_Boolean (Seq, Res); + end if; return Seq; when N_And_Bool - | N_Or_Bool - | N_Not_Bool => + | N_Or_Bool + | N_Not_Bool => return Sem_Boolean (Seq); when N_HDL_Expr => Res := Sem_Hdl_Expr (Seq); |