PSL: move canon code to canon.adb

7 files changed, 308 insertions, 135 deletions

diff --git a/src/vhdl/canon.adb b/src/vhdl/canon.adb
index d1ddd55d7..c498ba55c 100644
--- a/src/vhdl/canon.adb
+++ b/src/vhdl/canon.adb
@@ -25,6 +25,9 @@ with Iir_Chains; use Iir_Chains;
 with PSL.Nodes;
 with PSL.Rewrites;
 with PSL.Build;
+with PSL.NFAs;
+with PSL.NFAs.Utils;
+with Canon_PSL;
 
 package body Canon is
    --  Canonicalize a list of declarations.  LIST can be null.
@@ -759,6 +762,26 @@ package body Canon is
       end case;
    end Canon_Expression;
 
+   procedure Canon_PSL_Expression (Expr : PSL_Node)
+   is
+      use PSL.Nodes;
+   begin
+      case Get_Kind (Expr) is
+         when N_HDL_Expr =>
+            Canon_Expression (Get_HDL_Node (Expr));
+         when N_True | N_EOS =>
+            null;
+         when N_Not_Bool =>
+            Canon_PSL_Expression (Get_Boolean (Expr));
+         when N_And_Bool
+           | N_Or_Bool =>
+            Canon_PSL_Expression (Get_Left (Expr));
+            Canon_PSL_Expression (Get_Right (Expr));
+         when others =>
+            Error_Kind ("canon_psl_expression", Expr);
+      end case;
+   end Canon_PSL_Expression;
+
    procedure Canon_Discrete_Range (Rng : Iir) is
    begin
       case Get_Kind (Rng) is
@@ -1594,6 +1617,25 @@ package body Canon is
       Canon_Concurrent_Stmts (Top, Bod);
    end Canon_Generate_Statement_Body;
 
+   --  Return TRUE iff NFA has an edge with an EOS.
+   --  If so, we need to create a finalizer.
+   function Psl_Need_Finalizer (Nfa : PSL_NFA) return Boolean
+   is
+      use PSL.NFAs;
+      S : NFA_State;
+      E : NFA_Edge;
+   begin
+      S := Get_Final_State (Nfa);
+      E := Get_First_Dest_Edge (S);
+      while E /= No_Edge loop
+         if PSL.NFAs.Utils.Has_EOS (Get_Edge_Expr (E)) then
+            return True;
+         end if;
+         E := Get_Next_Dest_Edge (E);
+      end loop;
+      return False;
+   end Psl_Need_Finalizer;
+
    procedure Canon_Concurrent_Stmts (Top : Iir_Design_Unit; Parent : Iir)
    is
       --  Current element in the chain of concurrent statements.
@@ -1861,6 +1903,8 @@ package body Canon is
                   use PSL.Nodes;
                   Prop : PSL_Node;
                   Fa : PSL_NFA;
+                  Num : Natural;
+                  List : Iir_List;
                begin
                   Prop := Get_Psl_Property (El);
                   Prop := PSL.Rewrites.Rewrite_Property (Prop);
@@ -1869,7 +1913,21 @@ package body Canon is
                   Fa := PSL.Build.Build_FA (Prop);
                   Set_PSL_NFA (El, Fa);
 
-                  --  FIXME: report/severity.
+                  PSL.NFAs.Labelize_States (Fa, Num);
+                  Set_PSL_Nbr_States (El, Int32 (Num));
+
+                  Set_PSL_EOS_Flag (El, Psl_Need_Finalizer (Fa));
+
+                  List := Create_Iir_List;
+                  Canon_PSL.Canon_Extract_Sensitivity
+                    (Get_PSL_Clock (El), List);
+                  Set_PSL_Clock_Sensitivity (El, List);
+
+                  if Canon_Flag_Expressions then
+                     Canon_PSL_Expression (Get_PSL_Clock (El));
+                     Canon_Expression (Get_Severity_Expression (El));
+                     Canon_Expression (Get_Report_Expression (El));
+                  end if;
                end;
 
             when Iir_Kind_Psl_Default_Clock =>
diff --git a/src/vhdl/iirs.adb b/src/vhdl/iirs.adb
index 4bb4fef7a..00614233c 100644
--- a/src/vhdl/iirs.adb
+++ b/src/vhdl/iirs.adb
@@ -5309,4 +5309,52 @@ package body Iirs is
       Set_Field8 (N, PSL_NFA_To_Iir (Fa));
    end Set_PSL_NFA;
 
+   function Get_PSL_Nbr_States (N : Iir) return Int32 is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_Nbr_States (Get_Kind (N)),
+                     "no field PSL_Nbr_States");
+      return Iir_To_Int32 (Get_Field9 (N));
+   end Get_PSL_Nbr_States;
+
+   procedure Set_PSL_Nbr_States (N : Iir; Nbr : Int32) is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_Nbr_States (Get_Kind (N)),
+                     "no field PSL_Nbr_States");
+      Set_Field9 (N, Int32_To_Iir (Nbr));
+   end Set_PSL_Nbr_States;
+
+   function Get_PSL_Clock_Sensitivity (N : Iir) return Iir_List is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_Clock_Sensitivity (Get_Kind (N)),
+                     "no field PSL_Clock_Sensitivity");
+      return Iir_To_Iir_List (Get_Field10 (N));
+   end Get_PSL_Clock_Sensitivity;
+
+   procedure Set_PSL_Clock_Sensitivity (N : Iir; List : Iir_List) is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_Clock_Sensitivity (Get_Kind (N)),
+                     "no field PSL_Clock_Sensitivity");
+      Set_Field10 (N, Iir_List_To_Iir (List));
+   end Set_PSL_Clock_Sensitivity;
+
+   function Get_PSL_EOS_Flag (N : Iir) return Boolean is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_EOS_Flag (Get_Kind (N)),
+                     "no field PSL_EOS_Flag");
+      return Get_Flag1 (N);
+   end Get_PSL_EOS_Flag;
+
+   procedure Set_PSL_EOS_Flag (N : Iir; Flag : Boolean) is
+   begin
+      pragma Assert (N /= Null_Iir);
+      pragma Assert (Has_PSL_EOS_Flag (Get_Kind (N)),
+                     "no field PSL_EOS_Flag");
+      Set_Flag1 (N, Flag);
+   end Set_PSL_EOS_Flag;
+
 end Iirs;
diff --git a/src/vhdl/iirs.ads b/src/vhdl/iirs.ads
index 56a1794a9..1272e7723 100644
--- a/src/vhdl/iirs.ads
+++ b/src/vhdl/iirs.ads
@@ -2517,10 +2517,19 @@ package Iirs is
    --
    --   Get/Set_Report_Expression (Field5)
    --
+   --  The following fields are set by canon.
    --   Get/Set_PSL_Clock (Field7)
    --
    --   Get/Set_PSL_NFA (Field8)
    --
+   --  Number of states in the NFA.
+   --   Get/Set_PSL_Nbr_States (Field9)
+   --
+   --   Get/Set_PSL_Clock_Sensitivity (Field10)
+   --
+   --  True if at least one of the NFA edge has the EOS flag.
+   --   Get/Set_PSL_EOS_Flag (Flag1)
+   --
    --   Get/Set_Visible_Flag (Flag4)
 
    -- Iir_Kind_Component_Instantiation_Statement (Medium)
@@ -6655,4 +6664,17 @@ package Iirs is
    --  Field: Field8 (uc)
    function Get_PSL_NFA (N : Iir) return PSL_NFA;
    procedure Set_PSL_NFA (N : Iir; Fa : PSL_NFA);
+
+   --  Field: Field9 (uc)
+   function Get_PSL_Nbr_States (N : Iir) return Int32;
+   procedure Set_PSL_Nbr_States (N : Iir; Nbr : Int32);
+
+   --  Field: Field10 (uc)
+   function Get_PSL_Clock_Sensitivity (N : Iir) return Iir_List;
+   procedure Set_PSL_Clock_Sensitivity (N : Iir; List : Iir_List);
+
+   --  Field: Flag1
+   function Get_PSL_EOS_Flag (N : Iir) return Boolean;
+   procedure Set_PSL_EOS_Flag (N : Iir; Flag : Boolean);
+
 end Iirs;
diff --git a/src/vhdl/nodes_meta.adb b/src/vhdl/nodes_meta.adb
index c1725ea40..d5a3c62a0 100644
--- a/src/vhdl/nodes_meta.adb
+++ b/src/vhdl/nodes_meta.adb
@@ -316,7 +316,10 @@ package body Nodes_Meta is
       Field_Psl_Expression => Type_PSL_Node,
       Field_Psl_Boolean => Type_PSL_Node,
       Field_PSL_Clock => Type_PSL_Node,
-      Field_PSL_NFA => Type_PSL_NFA
+      Field_PSL_NFA => Type_PSL_NFA,
+      Field_PSL_Nbr_States => Type_Int32,
+      Field_PSL_Clock_Sensitivity => Type_Iir_List,
+      Field_PSL_EOS_Flag => Type_Boolean
      );
 
    function Get_Field_Type (F : Fields_Enum) return Types_Enum is
@@ -923,6 +926,12 @@ package body Nodes_Meta is
             return "psl_clock";
          when Field_PSL_NFA =>
             return "psl_nfa";
+         when Field_PSL_Nbr_States =>
+            return "psl_nbr_states";
+         when Field_PSL_Clock_Sensitivity =>
+            return "psl_clock_sensitivity";
+         when Field_PSL_EOS_Flag =>
+            return "psl_eos_flag";
       end case;
    end Get_Field_Image;
 
@@ -2039,6 +2048,12 @@ package body Nodes_Meta is
             return Attr_None;
          when Field_PSL_NFA =>
             return Attr_None;
+         when Field_PSL_Nbr_States =>
+            return Attr_None;
+         when Field_PSL_Clock_Sensitivity =>
+            return Attr_None;
+         when Field_PSL_EOS_Flag =>
+            return Attr_None;
       end case;
    end Get_Field_Attribute;
 
@@ -3449,7 +3464,10 @@ package body Nodes_Meta is
       Field_Label,
       Field_PSL_Clock,
       Field_PSL_NFA,
+      Field_PSL_Nbr_States,
+      Field_PSL_EOS_Flag,
       Field_Visible_Flag,
+      Field_PSL_Clock_Sensitivity,
       Field_Chain,
       Field_Severity_Expression,
       Field_Report_Expression,
@@ -3459,7 +3477,10 @@ package body Nodes_Meta is
       Field_Label,
       Field_PSL_Clock,
       Field_PSL_NFA,
+      Field_PSL_Nbr_States,
+      Field_PSL_EOS_Flag,
       Field_Visible_Flag,
+      Field_PSL_Clock_Sensitivity,
       Field_Chain,
       Field_Severity_Expression,
       Field_Report_Expression,
@@ -4197,85 +4218,85 @@ package body Nodes_Meta is
       Iir_Kind_Concurrent_Selected_Signal_Assignment => 1212,
       Iir_Kind_Concurrent_Assertion_Statement => 1220,
       Iir_Kind_Psl_Default_Clock => 1224,
-      Iir_Kind_Psl_Assert_Statement => 1233,
-      Iir_Kind_Psl_Cover_Statement => 1242,
-      Iir_Kind_Concurrent_Procedure_Call_Statement => 1249,
-      Iir_Kind_Block_Statement => 1262,
-      Iir_Kind_If_Generate_Statement => 1272,
-      Iir_Kind_For_Generate_Statement => 1281,
-      Iir_Kind_Component_Instantiation_Statement => 1291,
-      Iir_Kind_Simple_Simultaneous_Statement => 1298,
-      Iir_Kind_Generate_Statement_Body => 1309,
-      Iir_Kind_If_Generate_Else_Clause => 1314,
-      Iir_Kind_Simple_Signal_Assignment_Statement => 1323,
-      Iir_Kind_Conditional_Signal_Assignment_Statement => 1332,
-      Iir_Kind_Null_Statement => 1336,
-      Iir_Kind_Assertion_Statement => 1343,
-      Iir_Kind_Report_Statement => 1349,
-      Iir_Kind_Wait_Statement => 1356,
-      Iir_Kind_Variable_Assignment_Statement => 1362,
-      Iir_Kind_Conditional_Variable_Assignment_Statement => 1368,
-      Iir_Kind_Return_Statement => 1374,
-      Iir_Kind_For_Loop_Statement => 1383,
-      Iir_Kind_While_Loop_Statement => 1391,
-      Iir_Kind_Next_Statement => 1397,
-      Iir_Kind_Exit_Statement => 1403,
-      Iir_Kind_Case_Statement => 1411,
-      Iir_Kind_Procedure_Call_Statement => 1417,
-      Iir_Kind_If_Statement => 1426,
-      Iir_Kind_Elsif => 1431,
-      Iir_Kind_Character_Literal => 1438,
-      Iir_Kind_Simple_Name => 1445,
-      Iir_Kind_Selected_Name => 1453,
-      Iir_Kind_Operator_Symbol => 1458,
-      Iir_Kind_Selected_By_All_Name => 1463,
-      Iir_Kind_Parenthesis_Name => 1467,
-      Iir_Kind_External_Constant_Name => 1476,
-      Iir_Kind_External_Signal_Name => 1485,
-      Iir_Kind_External_Variable_Name => 1494,
-      Iir_Kind_Package_Pathname => 1497,
-      Iir_Kind_Absolute_Pathname => 1498,
-      Iir_Kind_Relative_Pathname => 1499,
-      Iir_Kind_Pathname_Element => 1503,
-      Iir_Kind_Base_Attribute => 1505,
-      Iir_Kind_Left_Type_Attribute => 1510,
-      Iir_Kind_Right_Type_Attribute => 1515,
-      Iir_Kind_High_Type_Attribute => 1520,
-      Iir_Kind_Low_Type_Attribute => 1525,
-      Iir_Kind_Ascending_Type_Attribute => 1530,
-      Iir_Kind_Image_Attribute => 1536,
-      Iir_Kind_Value_Attribute => 1542,
-      Iir_Kind_Pos_Attribute => 1548,
-      Iir_Kind_Val_Attribute => 1554,
-      Iir_Kind_Succ_Attribute => 1560,
-      Iir_Kind_Pred_Attribute => 1566,
-      Iir_Kind_Leftof_Attribute => 1572,
-      Iir_Kind_Rightof_Attribute => 1578,
-      Iir_Kind_Delayed_Attribute => 1586,
-      Iir_Kind_Stable_Attribute => 1594,
-      Iir_Kind_Quiet_Attribute => 1602,
-      Iir_Kind_Transaction_Attribute => 1610,
-      Iir_Kind_Event_Attribute => 1614,
-      Iir_Kind_Active_Attribute => 1618,
-      Iir_Kind_Last_Event_Attribute => 1622,
-      Iir_Kind_Last_Active_Attribute => 1626,
-      Iir_Kind_Last_Value_Attribute => 1630,
-      Iir_Kind_Driving_Attribute => 1634,
-      Iir_Kind_Driving_Value_Attribute => 1638,
-      Iir_Kind_Behavior_Attribute => 1638,
-      Iir_Kind_Structure_Attribute => 1638,
-      Iir_Kind_Simple_Name_Attribute => 1645,
-      Iir_Kind_Instance_Name_Attribute => 1650,
-      Iir_Kind_Path_Name_Attribute => 1655,
-      Iir_Kind_Left_Array_Attribute => 1662,
-      Iir_Kind_Right_Array_Attribute => 1669,
-      Iir_Kind_High_Array_Attribute => 1676,
-      Iir_Kind_Low_Array_Attribute => 1683,
-      Iir_Kind_Length_Array_Attribute => 1690,
-      Iir_Kind_Ascending_Array_Attribute => 1697,
-      Iir_Kind_Range_Array_Attribute => 1704,
-      Iir_Kind_Reverse_Range_Array_Attribute => 1711,
-      Iir_Kind_Attribute_Name => 1719
+      Iir_Kind_Psl_Assert_Statement => 1236,
+      Iir_Kind_Psl_Cover_Statement => 1248,
+      Iir_Kind_Concurrent_Procedure_Call_Statement => 1255,
+      Iir_Kind_Block_Statement => 1268,
+      Iir_Kind_If_Generate_Statement => 1278,
+      Iir_Kind_For_Generate_Statement => 1287,
+      Iir_Kind_Component_Instantiation_Statement => 1297,
+      Iir_Kind_Simple_Simultaneous_Statement => 1304,
+      Iir_Kind_Generate_Statement_Body => 1315,
+      Iir_Kind_If_Generate_Else_Clause => 1320,
+      Iir_Kind_Simple_Signal_Assignment_Statement => 1329,
+      Iir_Kind_Conditional_Signal_Assignment_Statement => 1338,
+      Iir_Kind_Null_Statement => 1342,
+      Iir_Kind_Assertion_Statement => 1349,
+      Iir_Kind_Report_Statement => 1355,
+      Iir_Kind_Wait_Statement => 1362,
+      Iir_Kind_Variable_Assignment_Statement => 1368,
+      Iir_Kind_Conditional_Variable_Assignment_Statement => 1374,
+      Iir_Kind_Return_Statement => 1380,
+      Iir_Kind_For_Loop_Statement => 1389,
+      Iir_Kind_While_Loop_Statement => 1397,
+      Iir_Kind_Next_Statement => 1403,
+      Iir_Kind_Exit_Statement => 1409,
+      Iir_Kind_Case_Statement => 1417,
+      Iir_Kind_Procedure_Call_Statement => 1423,
+      Iir_Kind_If_Statement => 1432,
+      Iir_Kind_Elsif => 1437,
+      Iir_Kind_Character_Literal => 1444,
+      Iir_Kind_Simple_Name => 1451,
+      Iir_Kind_Selected_Name => 1459,
+      Iir_Kind_Operator_Symbol => 1464,
+      Iir_Kind_Selected_By_All_Name => 1469,
+      Iir_Kind_Parenthesis_Name => 1473,
+      Iir_Kind_External_Constant_Name => 1482,
+      Iir_Kind_External_Signal_Name => 1491,
+      Iir_Kind_External_Variable_Name => 1500,
+      Iir_Kind_Package_Pathname => 1503,
+      Iir_Kind_Absolute_Pathname => 1504,
+      Iir_Kind_Relative_Pathname => 1505,
+      Iir_Kind_Pathname_Element => 1509,
+      Iir_Kind_Base_Attribute => 1511,
+      Iir_Kind_Left_Type_Attribute => 1516,
+      Iir_Kind_Right_Type_Attribute => 1521,
+      Iir_Kind_High_Type_Attribute => 1526,
+      Iir_Kind_Low_Type_Attribute => 1531,
+      Iir_Kind_Ascending_Type_Attribute => 1536,
+      Iir_Kind_Image_Attribute => 1542,
+      Iir_Kind_Value_Attribute => 1548,
+      Iir_Kind_Pos_Attribute => 1554,
+      Iir_Kind_Val_Attribute => 1560,
+      Iir_Kind_Succ_Attribute => 1566,
+      Iir_Kind_Pred_Attribute => 1572,
+      Iir_Kind_Leftof_Attribute => 1578,
+      Iir_Kind_Rightof_Attribute => 1584,
+      Iir_Kind_Delayed_Attribute => 1592,
+      Iir_Kind_Stable_Attribute => 1600,
+      Iir_Kind_Quiet_Attribute => 1608,
+      Iir_Kind_Transaction_Attribute => 1616,
+      Iir_Kind_Event_Attribute => 1620,
+      Iir_Kind_Active_Attribute => 1624,
+      Iir_Kind_Last_Event_Attribute => 1628,
+      Iir_Kind_Last_Active_Attribute => 1632,
+      Iir_Kind_Last_Value_Attribute => 1636,
+      Iir_Kind_Driving_Attribute => 1640,
+      Iir_Kind_Driving_Value_Attribute => 1644,
+      Iir_Kind_Behavior_Attribute => 1644,
+      Iir_Kind_Structure_Attribute => 1644,
+      Iir_Kind_Simple_Name_Attribute => 1651,
+      Iir_Kind_Instance_Name_Attribute => 1656,
+      Iir_Kind_Path_Name_Attribute => 1661,
+      Iir_Kind_Left_Array_Attribute => 1668,
+      Iir_Kind_Right_Array_Attribute => 1675,
+      Iir_Kind_High_Array_Attribute => 1682,
+      Iir_Kind_Low_Array_Attribute => 1689,
+      Iir_Kind_Length_Array_Attribute => 1696,
+      Iir_Kind_Ascending_Array_Attribute => 1703,
+      Iir_Kind_Range_Array_Attribute => 1710,
+      Iir_Kind_Reverse_Range_Array_Attribute => 1717,
+      Iir_Kind_Attribute_Name => 1725
      );
 
    function Get_Fields (K : Iir_Kind) return Fields_Array
@@ -4419,6 +4440,8 @@ package body Nodes_Meta is
             return Get_Suspend_Flag (N);
          when Field_Is_Ref =>
             return Get_Is_Ref (N);
+         when Field_PSL_EOS_Flag =>
+            return Get_PSL_EOS_Flag (N);
          when others =>
             raise Internal_Error;
       end case;
@@ -4527,6 +4550,8 @@ package body Nodes_Meta is
             Set_Suspend_Flag (N, V);
          when Field_Is_Ref =>
             Set_Is_Ref (N, V);
+         when Field_PSL_EOS_Flag =>
+            Set_PSL_EOS_Flag (N, V);
          when others =>
             raise Internal_Error;
       end case;
@@ -5601,6 +5626,8 @@ package body Nodes_Meta is
             return Get_Type_Marks_List (N);
          when Field_Overload_List =>
             return Get_Overload_List (N);
+         when Field_PSL_Clock_Sensitivity =>
+            return Get_PSL_Clock_Sensitivity (N);
          when others =>
             raise Internal_Error;
       end case;
@@ -5651,6 +5678,8 @@ package body Nodes_Meta is
             Set_Type_Marks_List (N, V);
          when Field_Overload_List =>
             Set_Overload_List (N, V);
+         when Field_PSL_Clock_Sensitivity =>
+            Set_PSL_Clock_Sensitivity (N, V);
          when others =>
             raise Internal_Error;
       end case;
@@ -5803,6 +5832,8 @@ package body Nodes_Meta is
             return Get_Design_Unit_Source_Col (N);
          when Field_String_Length =>
             return Get_String_Length (N);
+         when Field_PSL_Nbr_States =>
+            return Get_PSL_Nbr_States (N);
          when others =>
             raise Internal_Error;
       end case;
@@ -5819,6 +5850,8 @@ package body Nodes_Meta is
             Set_Design_Unit_Source_Col (N, V);
          when Field_String_Length =>
             Set_String_Length (N, V);
+         when Field_PSL_Nbr_States =>
+            Set_PSL_Nbr_States (N, V);
          when others =>
             raise Internal_Error;
       end case;
@@ -9777,4 +9810,37 @@ package body Nodes_Meta is
       end case;
    end Has_PSL_NFA;
 
+   function Has_PSL_Nbr_States (K : Iir_Kind) return Boolean is
+   begin
+      case K is
+         when Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Cover_Statement =>
+            return True;
+         when others =>
+            return False;
+      end case;
+   end Has_PSL_Nbr_States;
+
+   function Has_PSL_Clock_Sensitivity (K : Iir_Kind) return Boolean is
+   begin
+      case K is
+         when Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Cover_Statement =>
+            return True;
+         when others =>
+            return False;
+      end case;
+   end Has_PSL_Clock_Sensitivity;
+
+   function Has_PSL_EOS_Flag (K : Iir_Kind) return Boolean is
+   begin
+      case K is
+         when Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Cover_Statement =>
+            return True;
+         when others =>
+            return False;
+      end case;
+   end Has_PSL_EOS_Flag;
+
 end Nodes_Meta;
diff --git a/src/vhdl/nodes_meta.ads b/src/vhdl/nodes_meta.ads
index f688d527f..d4ae3a060 100644
--- a/src/vhdl/nodes_meta.ads
+++ b/src/vhdl/nodes_meta.ads
@@ -356,7 +356,10 @@ package Nodes_Meta is
       Field_Psl_Expression,
       Field_Psl_Boolean,
       Field_PSL_Clock,
-      Field_PSL_NFA
+      Field_PSL_NFA,
+      Field_PSL_Nbr_States,
+      Field_PSL_Clock_Sensitivity,
+      Field_PSL_EOS_Flag
      );
    pragma Discard_Names (Fields_Enum);
 
@@ -844,4 +847,7 @@ package Nodes_Meta is
    function Has_Psl_Boolean (K : Iir_Kind) return Boolean;
    function Has_PSL_Clock (K : Iir_Kind) return Boolean;
    function Has_PSL_NFA (K : Iir_Kind) return Boolean;
+   function Has_PSL_Nbr_States (K : Iir_Kind) return Boolean;
+   function Has_PSL_Clock_Sensitivity (K : Iir_Kind) return Boolean;
+   function Has_PSL_EOS_Flag (K : Iir_Kind) return Boolean;
 end Nodes_Meta;
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index ae6efeac0..b2138cd06 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -22,7 +22,6 @@ with Std_Package; use Std_Package;
 with Flags;
 with Libraries;
 with Canon;
-with Canon_PSL;
 with Trans_Analyzes;
 with Nodes_Meta;
 with PSL.Nodes;
@@ -299,8 +298,6 @@ package body Trans.Chap9 is
       use PSL.Nodes;
       use PSL.NFAs;
 
-      N : constant NFA := Get_PSL_NFA (Stmt);
-
       Mark : Id_Mark_Type;
       Info : Ortho_Info_Acc;
    begin
@@ -310,12 +307,14 @@ package body Trans.Chap9 is
       Push_Identifier_Prefix (Mark, Get_Identifier (Stmt));
       Push_Instance_Factory (Info.Psl_Scope'Access);
 
-      Labelize_States (N, Info.Psl_Vect_Len);
+      --  Create the state vector type.
       Info.Psl_Vect_Type := New_Constrained_Array_Type
         (Std_Boolean_Array_Type,
          New_Unsigned_Literal (Ghdl_Index_Type,
-           Unsigned_64 (Info.Psl_Vect_Len)));
+                               Unsigned_64 (Get_PSL_Nbr_States (Stmt))));
       New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type);
+
+      --  Create the variables.
       Info.Psl_Vect_Var := Create_Var
         (Create_Var_Identifier ("VECT"), Info.Psl_Vect_Type);
 
@@ -387,25 +386,6 @@ package body Trans.Chap9 is
       end case;
    end Translate_Psl_Expr;
 
-   --  Return TRUE iff NFA has an edge with an EOS.
-   --  If so, we need to create a finalizer.
-   function Psl_Need_Finalizer (Nfa : PSL_NFA) return Boolean
-   is
-      use PSL.NFAs;
-      S : NFA_State;
-      E : NFA_Edge;
-   begin
-      S := Get_Final_State (Nfa);
-      E := Get_First_Dest_Edge (S);
-      while E /= No_Edge loop
-         if PSL.NFAs.Utils.Has_EOS (Get_Edge_Expr (E)) then
-            return True;
-         end if;
-         E := Get_Next_Dest_Edge (E);
-      end loop;
-      return False;
-   end Psl_Need_Finalizer;
-
    procedure Create_Psl_Final_Proc
      (Stmt : Iir; Base : Block_Info_Acc; Instance : out O_Dnode)
    is
@@ -474,19 +454,19 @@ package body Trans.Chap9 is
       Gen_Exit_When
         (Label,
          New_Compare_Op (ON_Ge,
-           New_Obj_Value (Var_I),
-           New_Lit (New_Unsigned_Literal
-             (Ghdl_Index_Type,
-                Unsigned_64 (Info.Psl_Vect_Len))),
-           Ghdl_Bool_Type));
+                         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 (New_Obj (Var_Nvec),
-                       New_Obj_Value (Var_I)),
+                                            New_Obj_Value (Var_I)),
                        New_Lit (Std_Boolean_False_Node));
       Inc_Var (Var_I);
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
 
-      --  Global if statement for the clock.
+      --  Global 'if' statement for the clock.
       Open_Temp;
       Start_If_Stmt (Clk_Blk,
                      Translate_Psl_Expr (Get_PSL_Clock (Stmt), False));
@@ -535,7 +515,7 @@ package body Trans.Chap9 is
       --  Check fail state.
       S := Get_Final_State (NFA);
       S_Num := Get_State_Label (S);
-      pragma Assert (Integer (S_Num) = Info.Psl_Vect_Len - 1);
+      pragma Assert (S_Num = Get_PSL_Nbr_States (Stmt) - 1);
       Start_If_Stmt
         (S_Blk,
          New_Value (New_Indexed_Element (New_Obj (Var_Nvec),
@@ -565,16 +545,16 @@ package body Trans.Chap9 is
       Gen_Exit_When
         (Label,
          New_Compare_Op (ON_Ge,
-           New_Obj_Value (Var_I),
-           New_Lit (New_Unsigned_Literal
-             (Ghdl_Index_Type,
-                Unsigned_64 (Info.Psl_Vect_Len))),
-           Ghdl_Bool_Type));
+                         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_Value (New_Indexed_Element (New_Obj (Var_Nvec),
-           New_Obj_Value (Var_I))));
+                                         New_Obj_Value (Var_I))));
       Inc_Var (Var_I);
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
@@ -589,7 +569,7 @@ package body Trans.Chap9 is
       --  The finalizer.
       case Get_Kind (Stmt) is
          when Iir_Kind_Psl_Assert_Statement =>
-            if Psl_Need_Finalizer (NFA) then
+            if Get_PSL_EOS_Flag (Stmt) then
                Create_Psl_Final_Proc (Stmt, Base, Instance);
 
                Start_Subprogram_Body (Info.Psl_Proc_Final_Subprg);
@@ -644,7 +624,7 @@ package body Trans.Chap9 is
             Start_If_Stmt
               (S_Blk,
                New_Monadic_Op (ON_Not,
-                 New_Value (Get_Var (Info.Psl_Bool_Var))));
+                               New_Value (Get_Var (Info.Psl_Bool_Var))));
             Chap8.Translate_Report
               (Stmt, Ghdl_Psl_Cover_Failed, Severity_Level_Error);
             Finish_If_Stmt (S_Blk);
@@ -1352,7 +1332,6 @@ package body Trans.Chap9 is
       Info   : constant Psl_Info_Acc := Get_Info (Stmt);
       Constr : O_Assoc_List;
       List   : Iir_List;
-      Clk    : PSL_Node;
       Var_I  : O_Dnode;
       Label  : O_Snode;
    begin
@@ -1371,12 +1350,9 @@ package body Trans.Chap9 is
       New_Procedure_Call (Constr);
 
       --  Register clock sensitivity.
-      Clk := Get_PSL_Clock (Stmt);
-      List := Create_Iir_List;
-      Canon_PSL.Canon_Extract_Sensitivity (Clk, List);
+      List := Get_PSL_Clock_Sensitivity (Stmt);
       Destroy_Types_In_List (List);
       Register_Signal_List (List, Ghdl_Process_Add_Sensitivity);
-      Destroy_Iir_List (List);
 
       --  Register finalizer (if any).
       if Info.Psl_Proc_Final_Subprg /= O_Dnode_Null then
@@ -1403,11 +1379,11 @@ package body Trans.Chap9 is
       Gen_Exit_When
         (Label,
          New_Compare_Op (ON_Ge,
-           New_Obj_Value (Var_I),
-           New_Lit (New_Unsigned_Literal
-             (Ghdl_Index_Type,
-                Unsigned_64 (Info.Psl_Vect_Len))),
-           Ghdl_Bool_Type));
+                         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));
diff --git a/src/vhdl/translate/trans.ads b/src/vhdl/translate/trans.ads
index 1a7c2e53f..63db84bd8 100644
--- a/src/vhdl/translate/trans.ads
+++ b/src/vhdl/translate/trans.ads
@@ -1305,9 +1305,6 @@ package Trans is
             --  Procedure for finalization.  Handles EOS.
             Psl_Proc_Final_Subprg : O_Dnode;
 
-            --  Length of the state vector.
-            Psl_Vect_Len : Natural;
-
             --  Type of the state vector.
             Psl_Vect_Type : O_Tnode;