psl: prefix of goto/non-consecutive repetition is a bool. Fix #1708

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);