aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/psl/psl-nodes.ads15
-rw-r--r--src/psl/psl-nodes_meta.adb10
-rw-r--r--src/psl/psl-rewrites.adb22
-rw-r--r--src/vhdl/vhdl-parse_psl.adb86
-rw-r--r--src/vhdl/vhdl-prints.adb23
-rw-r--r--src/vhdl/vhdl-sem_psl.adb20
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);
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-30 00:06:05 +0000