trans-chap9.adb: handle async_abort, sync_abort. Fix #1654

5 files changed, 255 insertions, 145 deletions

diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb
index 9ff16a6ff..44d74499b 100644
--- a/src/psl/psl-subsets.adb
+++ b/src/psl/psl-subsets.adb
@@ -14,6 +14,8 @@
 --  You should have received a copy of the GNU General Public License
 --  along with this program.  If not, see <gnu.org/licenses>.
 
+with Types; use Types;
+
 with PSL.Types; use PSL.Types;
 with PSL.Errors; use PSL.Errors;
 
@@ -197,4 +199,19 @@ package body PSL.Subsets is
             null;
       end case;
    end Check_Simple;
+
+   function Is_Async_Abort (N : Node) return Boolean is
+   begin
+      case Get_Kind (N) is
+         when N_Async_Abort =>
+            return True;
+         when N_Sync_Abort =>
+            return False;
+         when N_Abort =>
+            return False;
+         when others =>
+            raise Internal_Error;
+      end case;
+   end Is_Async_Abort;
+
 end PSL.Subsets;
diff --git a/src/psl/psl-subsets.ads b/src/psl/psl-subsets.ads
index 50aeba6d4..472c4579b 100644
--- a/src/psl/psl-subsets.ads
+++ b/src/psl/psl-subsets.ads
@@ -36,4 +36,9 @@ package PSL.Subsets is
    --  All other operators not mentioned above are supported in the simple
    --  subset without restriction.
    procedure Check_Simple (N : Node);
+
+   --  Return True iff N is an async abort.
+   --  True for N_Async_Abort, False for N_Sync_Abort.
+   --  Here we also decide for N_Abort.
+   function Is_Async_Abort (N : Node) return Boolean;
 end PSL.Subsets;
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index fe5a291b5..fef616ce1 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -14,20 +14,25 @@
 --  You should have received a copy of the GNU General Public License
 --  along with this program.  If not, see <gnu.org/licenses>.
 
-with Vhdl.Utils; use Vhdl.Utils;
-with Vhdl.Errors; use Vhdl.Errors;
-with Vhdl.Std_Package; use Vhdl.Std_Package;
 with Flags;
 with Libraries;
+
 with Vhdl.Canon;
-with Trans_Analyzes;
+with Vhdl.Canon_PSL;
+with Vhdl.Utils; use Vhdl.Utils;
+with Vhdl.Errors; use Vhdl.Errors;
+with Vhdl.Std_Package; use Vhdl.Std_Package;
 with Vhdl.Nodes_Meta;
+with Vhdl.Ieee.Std_Logic_1164;
+
 with PSL.Types; use PSL.Types;
 with PSL.Nodes;
 with PSL.NFAs;
 with PSL.NFAs.Utils;
+with PSL.Subsets;
 with PSL.Errors; use PSL.Errors;
-with Vhdl.Ieee.Std_Logic_1164;
+
+with Trans_Analyzes;
 with Trans.Chap1;
 with Trans.Chap3;
 with Trans.Chap4;
@@ -373,6 +378,36 @@ package body Trans.Chap9 is
         (Create_Identifier_Without_Prefix (Stmt), Info.Psl_Scope);
    end Translate_Psl_Directive_Declarations;
 
+   --  Initialize/reset the PSL state vector for STMT.
+   procedure Elab_PSL_State_Vector (Stmt : Iir)
+   is
+      Info   : constant Psl_Info_Acc := Get_Info (Stmt);
+      Var_I  : O_Dnode;
+      Label  : O_Snode;
+   begin
+      Start_Declare_Stmt;
+      New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
+      New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
+                                            New_Lit (Ghdl_Index_0)),
+                       New_Lit (Std_Boolean_True_Node));
+      New_Assign_Stmt (New_Obj (Var_I), New_Lit (Ghdl_Index_1));
+      Start_Loop_Stmt (Label);
+      Gen_Exit_When
+        (Label,
+         New_Compare_Op (ON_Ge,
+                         New_Obj_Value (Var_I),
+                         New_Lit (New_Unsigned_Literal
+                                    (Ghdl_Index_Type,
+                                     Unsigned_64 (Get_PSL_Nbr_States (Stmt)))),
+                         Ghdl_Bool_Type));
+      New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
+                       New_Obj_Value (Var_I)),
+                       New_Lit (Std_Boolean_False_Node));
+      Inc_Var (Var_I);
+      Finish_Loop_Stmt (Label);
+      Finish_Declare_Stmt;
+   end Elab_PSL_State_Vector;
+
    function Translate_Psl_Expr (Expr : PSL_Node; Eos : Boolean)
                                return O_Enode
    is
@@ -548,6 +583,8 @@ package body Trans.Chap9 is
      (Stmt : Iir; Base : Block_Info_Acc)
    is
       use PSL.NFAs;
+      use PSL.Nodes;
+      use PSL.Subsets;
       Info       : constant Psl_Info_Acc := Get_Info (Stmt);
       Inter_List : O_Inter_List;
       Instance   : O_Dnode;
@@ -557,6 +594,7 @@ package body Trans.Chap9 is
       Report_Proc : O_Dnode;
       Label      : O_Snode;
       Clk_Blk    : O_If_Block;
+      Abort_Blk  : O_If_Block;
       S_Blk      : O_If_Block;
       E_Blk      : O_If_Block;
       S          : NFA_State;
@@ -567,12 +605,28 @@ package body Trans.Chap9 is
       NFA        : PSL_NFA;
       D_Lit      : O_Cnode;
       Assocs     : O_Assoc_List;
+      Has_Sync_Abort  : Boolean;
+      Has_Async_Abort : Boolean;
+      Abort_Prop : PSL_Node;
    begin
+      Has_Async_Abort := False;
+      Has_Sync_Abort := False;
+      Abort_Prop := Null_PSL_Node;
       case Get_Kind (Stmt) is
          when Iir_Kind_Psl_Cover_Directive =>
             Translate_Psl_Report (Stmt, Base, Report_Proc);
-         when others =>
+         when Iir_Kind_Psl_Restrict_Directive =>
             null;
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            null;
+         when Iir_Kinds_Psl_Property_Directive =>
+            if Get_PSL_Abort_Flag (Stmt) then
+               Abort_Prop := Get_Psl_Property (Stmt);
+               Has_Async_Abort := Is_Async_Abort (Abort_Prop);
+               Has_Sync_Abort := not Has_Async_Abort;
+            end if;
+         when others =>
+            raise Internal_Error;
       end case;
 
       Start_Procedure_Decl (Inter_List, Create_Identifier ("PROC"),
@@ -592,6 +646,27 @@ package body Trans.Chap9 is
       --  Flag for active edge from start state (assertion "started" flag).
       New_Var_Decl (Var_SFlag, Wki_Flag, O_Storage_Local, Ghdl_Bool_Type);
 
+      --  'if' statement for async abort
+      Open_Temp;
+      if Has_Async_Abort then
+         Start_If_Stmt (Abort_Blk,
+                        Translate_Psl_Expr (Get_Boolean (Abort_Prop), False));
+         Elab_PSL_State_Vector (Stmt);
+         New_Else_Stmt (Abort_Blk);
+      end if;
+
+      --  Global 'if' statement for the clock.
+      Start_If_Stmt (Clk_Blk,
+                     Translate_Psl_Expr (Get_PSL_Clock (Stmt), False));
+
+      --  'if' statement for sync abort.
+      if Has_Sync_Abort then
+         Start_If_Stmt (Abort_Blk,
+                        Translate_Psl_Expr (Get_Boolean (Abort_Prop), False));
+         Elab_PSL_State_Vector (Stmt);
+         New_Else_Stmt (Abort_Blk);
+      end if;
+
       --  Initialize the new state vector.
       Start_Declare_Stmt;
       New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
@@ -624,11 +699,6 @@ package body Trans.Chap9 is
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
 
-      --  Global 'if' statement for the clock.
-      Open_Temp;
-      Start_If_Stmt (Clk_Blk,
-                     Translate_Psl_Expr (Get_PSL_Clock (Stmt), False));
-
       -- Default "started" flag is not set
       New_Assign_Stmt (New_Obj (Var_SFlag), New_Lit (Ghdl_Bool_False_Node));
 
@@ -773,9 +843,17 @@ package body Trans.Chap9 is
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
 
-      Close_Temp;
+      if Has_Sync_Abort then
+         Finish_If_Stmt (Abort_Blk);
+      end if;
+
       Finish_If_Stmt (Clk_Blk);
 
+      if Has_Async_Abort then
+         Finish_If_Stmt (Abort_Blk);
+      end if;
+      Close_Temp;
+
       Clear_Scope (Base.Block_Scope);
       Pop_Local_Factory;
       Finish_Subprogram_Body;
@@ -1933,8 +2011,6 @@ package body Trans.Chap9 is
       Info   : constant Psl_Info_Acc := Get_Info (Stmt);
       Constr : O_Assoc_List;
       List   : Iir_List;
-      Var_I  : O_Dnode;
-      Label  : O_Snode;
       Init   : O_Cnode;
    begin
       New_Debug_Line_Stmt (Get_Line_Number (Stmt));
@@ -1956,6 +2032,26 @@ package body Trans.Chap9 is
       Destroy_Types_In_List (List);
       Register_Signal_List (List, Ghdl_Process_Add_Sensitivity);
 
+      --  Register async sensitivity.
+      if Get_Kind (Stmt) in Iir_Kinds_Psl_Property_Directive
+        and then Get_PSL_Abort_Flag (Stmt)
+      then
+         declare
+            use PSL.Nodes;
+            Prop : constant PSL_Node := Get_Psl_Property (Stmt);
+            List : Iir_List;
+         begin
+            if PSL.Subsets.Is_Async_Abort (Prop) then
+               List := Create_Iir_List;
+               Vhdl.Canon_PSL.Canon_Extract_Sensitivity
+                 (Get_Boolean (Prop), List);
+               Destroy_Types_In_List (List);
+               Register_Signal_List (List, Ghdl_Process_Add_Sensitivity);
+               Destroy_Iir_List (List);
+            end if;
+         end;
+      end if;
+
       --  Register finalizer (if any).
       if Info.Psl_Proc_Final_Subprg /= O_Dnode_Null then
          Start_Association (Constr, Ghdl_Finalize_Register);
@@ -1971,27 +2067,7 @@ package body Trans.Chap9 is
       end if;
 
       --  Initialize state vector.
-      Start_Declare_Stmt;
-      New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
-      New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
-                                            New_Lit (Ghdl_Index_0)),
-                       New_Lit (Std_Boolean_True_Node));
-      New_Assign_Stmt (New_Obj (Var_I), New_Lit (Ghdl_Index_1));
-      Start_Loop_Stmt (Label);
-      Gen_Exit_When
-        (Label,
-         New_Compare_Op (ON_Ge,
-                         New_Obj_Value (Var_I),
-                         New_Lit (New_Unsigned_Literal
-                                    (Ghdl_Index_Type,
-                                     Unsigned_64 (Get_PSL_Nbr_States (Stmt)))),
-                         Ghdl_Bool_Type));
-      New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
-                       New_Obj_Value (Var_I)),
-                       New_Lit (Std_Boolean_False_Node));
-      Inc_Var (Var_I);
-      Finish_Loop_Stmt (Label);
-      Finish_Declare_Stmt;
+      Elab_PSL_State_Vector (Stmt);
 
       if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
          Init := Std_Boolean_False_Node;
diff --git a/src/vhdl/vhdl-nodes.ads b/src/vhdl/vhdl-nodes.ads
index 90f74cdc1..741ddb56f 100644
--- a/src/vhdl/vhdl-nodes.ads
+++ b/src/vhdl/vhdl-nodes.ads
@@ -3357,6 +3357,8 @@ package Vhdl.Nodes is
    --   Get/Set_PSL_EOS_Flag (Flag1)
    --
    --  True if there is an outer abort is present (but not in the NFA)
+   -- Only for Iir_Kind_Psl_Assert_Directive:
+   -- Only for Iir_Kind_Psl_Assume_Directive:
    --   Get/Set_PSL_Abort_Flag (Flag2)
    --
    --   Get/Set_Postponed_Flag (Flag3)
@@ -6879,6 +6881,20 @@ package Vhdl.Nodes is
    --Iir_Kind_Psl_Cover_Directive
      Iir_Kind_Psl_Restrict_Directive;
 
+   subtype Iir_Kinds_Psl_Property_Directive is Iir_Kind range
+     Iir_Kind_Psl_Assert_Directive ..
+     Iir_Kind_Psl_Assume_Directive;
+
+   subtype Iir_Kinds_Psl_Sequence_Directive is Iir_Kind range
+     Iir_Kind_Psl_Cover_Directive ..
+     Iir_Kind_Psl_Restrict_Directive;
+
+   subtype Iir_Kinds_Psl_Directive is Iir_Kind range
+     Iir_Kind_Psl_Assert_Directive ..
+   --Iir_Kind_Psl_Assume_Directive
+   --Iir_Kind_Psl_Cover_Directive
+     Iir_Kind_Psl_Restrict_Directive;
+
    subtype Iir_Kinds_Generate_Statement is Iir_Kind range
      Iir_Kind_If_Generate_Statement ..
    --Iir_Kind_Case_Generate_Statement
diff --git a/src/vhdl/vhdl-nodes_meta.adb b/src/vhdl/vhdl-nodes_meta.adb
index d470935e4..2981b9f5c 100644
--- a/src/vhdl/vhdl-nodes_meta.adb
+++ b/src/vhdl/vhdl-nodes_meta.adb
@@ -4417,7 +4417,6 @@ package body Vhdl.Nodes_Meta is
       Field_PSL_NFA,
       Field_PSL_Nbr_States,
       Field_PSL_EOS_Flag,
-      Field_PSL_Abort_Flag,
       Field_Postponed_Flag,
       Field_Visible_Flag,
       Field_Parent,
@@ -4431,7 +4430,6 @@ package body Vhdl.Nodes_Meta is
       Field_PSL_NFA,
       Field_PSL_Nbr_States,
       Field_PSL_EOS_Flag,
-      Field_PSL_Abort_Flag,
       Field_Postponed_Flag,
       Field_Visible_Flag,
       Field_Parent,
@@ -5455,111 +5453,111 @@ package body Vhdl.Nodes_Meta is
       Iir_Kind_Concurrent_Break_Statement => 1635,
       Iir_Kind_Psl_Assert_Directive => 1649,
       Iir_Kind_Psl_Assume_Directive => 1661,
-      Iir_Kind_Psl_Cover_Directive => 1674,
-      Iir_Kind_Psl_Restrict_Directive => 1686,
-      Iir_Kind_Block_Statement => 1700,
-      Iir_Kind_If_Generate_Statement => 1711,
-      Iir_Kind_Case_Generate_Statement => 1720,
-      Iir_Kind_For_Generate_Statement => 1729,
-      Iir_Kind_Component_Instantiation_Statement => 1740,
-      Iir_Kind_Psl_Default_Clock => 1743,
-      Iir_Kind_Generate_Statement_Body => 1754,
-      Iir_Kind_If_Generate_Else_Clause => 1760,
-      Iir_Kind_Simple_Simultaneous_Statement => 1767,
-      Iir_Kind_Simultaneous_Null_Statement => 1771,
-      Iir_Kind_Simultaneous_Procedural_Statement => 1782,
-      Iir_Kind_Simultaneous_Case_Statement => 1791,
-      Iir_Kind_Simultaneous_If_Statement => 1800,
-      Iir_Kind_Simultaneous_Elsif => 1806,
-      Iir_Kind_Simple_Signal_Assignment_Statement => 1817,
-      Iir_Kind_Conditional_Signal_Assignment_Statement => 1828,
-      Iir_Kind_Selected_Waveform_Assignment_Statement => 1840,
-      Iir_Kind_Signal_Force_Assignment_Statement => 1850,
-      Iir_Kind_Signal_Release_Assignment_Statement => 1859,
-      Iir_Kind_Null_Statement => 1863,
-      Iir_Kind_Assertion_Statement => 1870,
-      Iir_Kind_Report_Statement => 1876,
-      Iir_Kind_Wait_Statement => 1884,
-      Iir_Kind_Variable_Assignment_Statement => 1891,
-      Iir_Kind_Conditional_Variable_Assignment_Statement => 1898,
-      Iir_Kind_Return_Statement => 1904,
-      Iir_Kind_For_Loop_Statement => 1915,
-      Iir_Kind_While_Loop_Statement => 1926,
-      Iir_Kind_Next_Statement => 1933,
-      Iir_Kind_Exit_Statement => 1940,
-      Iir_Kind_Case_Statement => 1948,
-      Iir_Kind_Procedure_Call_Statement => 1954,
-      Iir_Kind_Break_Statement => 1961,
-      Iir_Kind_If_Statement => 1971,
-      Iir_Kind_Elsif => 1977,
-      Iir_Kind_Character_Literal => 1984,
-      Iir_Kind_Simple_Name => 1991,
-      Iir_Kind_Selected_Name => 1999,
-      Iir_Kind_Operator_Symbol => 2004,
-      Iir_Kind_Reference_Name => 2009,
-      Iir_Kind_External_Constant_Name => 2018,
-      Iir_Kind_External_Signal_Name => 2027,
-      Iir_Kind_External_Variable_Name => 2037,
-      Iir_Kind_Selected_By_All_Name => 2043,
-      Iir_Kind_Parenthesis_Name => 2048,
-      Iir_Kind_Package_Pathname => 2052,
-      Iir_Kind_Absolute_Pathname => 2053,
-      Iir_Kind_Relative_Pathname => 2054,
-      Iir_Kind_Pathname_Element => 2059,
-      Iir_Kind_Base_Attribute => 2061,
-      Iir_Kind_Subtype_Attribute => 2066,
-      Iir_Kind_Element_Attribute => 2071,
-      Iir_Kind_Across_Attribute => 2076,
-      Iir_Kind_Through_Attribute => 2081,
-      Iir_Kind_Nature_Reference_Attribute => 2085,
-      Iir_Kind_Left_Type_Attribute => 2090,
-      Iir_Kind_Right_Type_Attribute => 2095,
-      Iir_Kind_High_Type_Attribute => 2100,
-      Iir_Kind_Low_Type_Attribute => 2105,
-      Iir_Kind_Ascending_Type_Attribute => 2110,
-      Iir_Kind_Image_Attribute => 2116,
-      Iir_Kind_Value_Attribute => 2122,
-      Iir_Kind_Pos_Attribute => 2128,
-      Iir_Kind_Val_Attribute => 2134,
-      Iir_Kind_Succ_Attribute => 2140,
-      Iir_Kind_Pred_Attribute => 2146,
-      Iir_Kind_Leftof_Attribute => 2152,
-      Iir_Kind_Rightof_Attribute => 2158,
-      Iir_Kind_Signal_Slew_Attribute => 2166,
-      Iir_Kind_Quantity_Slew_Attribute => 2174,
-      Iir_Kind_Ramp_Attribute => 2182,
-      Iir_Kind_Zoh_Attribute => 2190,
-      Iir_Kind_Ltf_Attribute => 2198,
-      Iir_Kind_Ztf_Attribute => 2208,
-      Iir_Kind_Dot_Attribute => 2215,
-      Iir_Kind_Integ_Attribute => 2222,
-      Iir_Kind_Above_Attribute => 2230,
-      Iir_Kind_Quantity_Delayed_Attribute => 2238,
-      Iir_Kind_Delayed_Attribute => 2247,
-      Iir_Kind_Stable_Attribute => 2256,
-      Iir_Kind_Quiet_Attribute => 2265,
-      Iir_Kind_Transaction_Attribute => 2274,
-      Iir_Kind_Event_Attribute => 2278,
-      Iir_Kind_Active_Attribute => 2282,
-      Iir_Kind_Last_Event_Attribute => 2286,
-      Iir_Kind_Last_Active_Attribute => 2290,
-      Iir_Kind_Last_Value_Attribute => 2294,
-      Iir_Kind_Driving_Attribute => 2298,
-      Iir_Kind_Driving_Value_Attribute => 2302,
-      Iir_Kind_Behavior_Attribute => 2302,
-      Iir_Kind_Structure_Attribute => 2302,
-      Iir_Kind_Simple_Name_Attribute => 2309,
-      Iir_Kind_Instance_Name_Attribute => 2314,
-      Iir_Kind_Path_Name_Attribute => 2319,
-      Iir_Kind_Left_Array_Attribute => 2326,
-      Iir_Kind_Right_Array_Attribute => 2333,
-      Iir_Kind_High_Array_Attribute => 2340,
-      Iir_Kind_Low_Array_Attribute => 2347,
-      Iir_Kind_Length_Array_Attribute => 2354,
-      Iir_Kind_Ascending_Array_Attribute => 2361,
-      Iir_Kind_Range_Array_Attribute => 2368,
-      Iir_Kind_Reverse_Range_Array_Attribute => 2375,
-      Iir_Kind_Attribute_Name => 2384
+      Iir_Kind_Psl_Cover_Directive => 1673,
+      Iir_Kind_Psl_Restrict_Directive => 1684,
+      Iir_Kind_Block_Statement => 1698,
+      Iir_Kind_If_Generate_Statement => 1709,
+      Iir_Kind_Case_Generate_Statement => 1718,
+      Iir_Kind_For_Generate_Statement => 1727,
+      Iir_Kind_Component_Instantiation_Statement => 1738,
+      Iir_Kind_Psl_Default_Clock => 1741,
+      Iir_Kind_Generate_Statement_Body => 1752,
+      Iir_Kind_If_Generate_Else_Clause => 1758,
+      Iir_Kind_Simple_Simultaneous_Statement => 1765,
+      Iir_Kind_Simultaneous_Null_Statement => 1769,
+      Iir_Kind_Simultaneous_Procedural_Statement => 1780,
+      Iir_Kind_Simultaneous_Case_Statement => 1789,
+      Iir_Kind_Simultaneous_If_Statement => 1798,
+      Iir_Kind_Simultaneous_Elsif => 1804,
+      Iir_Kind_Simple_Signal_Assignment_Statement => 1815,
+      Iir_Kind_Conditional_Signal_Assignment_Statement => 1826,
+      Iir_Kind_Selected_Waveform_Assignment_Statement => 1838,
+      Iir_Kind_Signal_Force_Assignment_Statement => 1848,
+      Iir_Kind_Signal_Release_Assignment_Statement => 1857,
+      Iir_Kind_Null_Statement => 1861,
+      Iir_Kind_Assertion_Statement => 1868,
+      Iir_Kind_Report_Statement => 1874,
+      Iir_Kind_Wait_Statement => 1882,
+      Iir_Kind_Variable_Assignment_Statement => 1889,
+      Iir_Kind_Conditional_Variable_Assignment_Statement => 1896,
+      Iir_Kind_Return_Statement => 1902,
+      Iir_Kind_For_Loop_Statement => 1913,
+      Iir_Kind_While_Loop_Statement => 1924,
+      Iir_Kind_Next_Statement => 1931,
+      Iir_Kind_Exit_Statement => 1938,
+      Iir_Kind_Case_Statement => 1946,
+      Iir_Kind_Procedure_Call_Statement => 1952,
+      Iir_Kind_Break_Statement => 1959,
+      Iir_Kind_If_Statement => 1969,
+      Iir_Kind_Elsif => 1975,
+      Iir_Kind_Character_Literal => 1982,
+      Iir_Kind_Simple_Name => 1989,
+      Iir_Kind_Selected_Name => 1997,
+      Iir_Kind_Operator_Symbol => 2002,
+      Iir_Kind_Reference_Name => 2007,
+      Iir_Kind_External_Constant_Name => 2016,
+      Iir_Kind_External_Signal_Name => 2025,
+      Iir_Kind_External_Variable_Name => 2035,
+      Iir_Kind_Selected_By_All_Name => 2041,
+      Iir_Kind_Parenthesis_Name => 2046,
+      Iir_Kind_Package_Pathname => 2050,
+      Iir_Kind_Absolute_Pathname => 2051,
+      Iir_Kind_Relative_Pathname => 2052,
+      Iir_Kind_Pathname_Element => 2057,
+      Iir_Kind_Base_Attribute => 2059,
+      Iir_Kind_Subtype_Attribute => 2064,
+      Iir_Kind_Element_Attribute => 2069,
+      Iir_Kind_Across_Attribute => 2074,
+      Iir_Kind_Through_Attribute => 2079,
+      Iir_Kind_Nature_Reference_Attribute => 2083,
+      Iir_Kind_Left_Type_Attribute => 2088,
+      Iir_Kind_Right_Type_Attribute => 2093,
+      Iir_Kind_High_Type_Attribute => 2098,
+      Iir_Kind_Low_Type_Attribute => 2103,
+      Iir_Kind_Ascending_Type_Attribute => 2108,
+      Iir_Kind_Image_Attribute => 2114,
+      Iir_Kind_Value_Attribute => 2120,
+      Iir_Kind_Pos_Attribute => 2126,
+      Iir_Kind_Val_Attribute => 2132,
+      Iir_Kind_Succ_Attribute => 2138,
+      Iir_Kind_Pred_Attribute => 2144,
+      Iir_Kind_Leftof_Attribute => 2150,
+      Iir_Kind_Rightof_Attribute => 2156,
+      Iir_Kind_Signal_Slew_Attribute => 2164,
+      Iir_Kind_Quantity_Slew_Attribute => 2172,
+      Iir_Kind_Ramp_Attribute => 2180,
+      Iir_Kind_Zoh_Attribute => 2188,
+      Iir_Kind_Ltf_Attribute => 2196,
+      Iir_Kind_Ztf_Attribute => 2206,
+      Iir_Kind_Dot_Attribute => 2213,
+      Iir_Kind_Integ_Attribute => 2220,
+      Iir_Kind_Above_Attribute => 2228,
+      Iir_Kind_Quantity_Delayed_Attribute => 2236,
+      Iir_Kind_Delayed_Attribute => 2245,
+      Iir_Kind_Stable_Attribute => 2254,
+      Iir_Kind_Quiet_Attribute => 2263,
+      Iir_Kind_Transaction_Attribute => 2272,
+      Iir_Kind_Event_Attribute => 2276,
+      Iir_Kind_Active_Attribute => 2280,
+      Iir_Kind_Last_Event_Attribute => 2284,
+      Iir_Kind_Last_Active_Attribute => 2288,
+      Iir_Kind_Last_Value_Attribute => 2292,
+      Iir_Kind_Driving_Attribute => 2296,
+      Iir_Kind_Driving_Value_Attribute => 2300,
+      Iir_Kind_Behavior_Attribute => 2300,
+      Iir_Kind_Structure_Attribute => 2300,
+      Iir_Kind_Simple_Name_Attribute => 2307,
+      Iir_Kind_Instance_Name_Attribute => 2312,
+      Iir_Kind_Path_Name_Attribute => 2317,
+      Iir_Kind_Left_Array_Attribute => 2324,
+      Iir_Kind_Right_Array_Attribute => 2331,
+      Iir_Kind_High_Array_Attribute => 2338,
+      Iir_Kind_Low_Array_Attribute => 2345,
+      Iir_Kind_Length_Array_Attribute => 2352,
+      Iir_Kind_Ascending_Array_Attribute => 2359,
+      Iir_Kind_Range_Array_Attribute => 2366,
+      Iir_Kind_Reverse_Range_Array_Attribute => 2373,
+      Iir_Kind_Attribute_Name => 2382
      );
 
    function Get_Fields_First (K : Iir_Kind) return Fields_Index is
@@ -12684,9 +12682,7 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Psl_Assert_Directive
-           | Iir_Kind_Psl_Assume_Directive
-           | Iir_Kind_Psl_Cover_Directive
-           | Iir_Kind_Psl_Restrict_Directive =>
+           | Iir_Kind_Psl_Assume_Directive =>
             return True;
          when others =>
             return False;