aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/psl/psl-nodes.adb114
-rw-r--r--src/psl/psl-nodes.adb.in123
-rw-r--r--src/psl/psl-nodes.ads4
-rw-r--r--src/psl/psl-nodes_meta.adb100
-rw-r--r--src/psl/psl-qm.adb16
-rw-r--r--src/psl/psl-rewrites.adb5
-rw-r--r--src/psl/psl-subsets.adb52
-rw-r--r--src/vhdl/vhdl-parse_psl.adb110
-rw-r--r--src/vhdl/vhdl-scanner.adb8
-rw-r--r--src/vhdl/vhdl-sem_psl.adb11
-rw-r--r--src/vhdl/vhdl-tokens.adb2
-rw-r--r--src/vhdl/vhdl-tokens.ads1
12 files changed, 316 insertions, 230 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-13 19:59:37 +0000