PSL: add clocked SERE, make endpoints visible from VHDL.

26 files changed, 513 insertions, 273 deletions

diff --git a/src/grt/grt-disp_rti.adb b/src/grt/grt-disp_rti.adb
index 57f6ae146..ad1798f99 100644
--- a/src/grt/grt-disp_rti.adb
+++ b/src/grt/grt-disp_rti.adb
@@ -427,6 +427,8 @@ package body Grt.Disp_Rti is
             Put ("ghdl_rtik_psl_assert");
          when Ghdl_Rtik_Psl_Cover =>
             Put ("ghdl_rtik_psl_cover");
+         when Ghdl_Rtik_Psl_Endpoint =>
+            Put ("ghdl_rtik_psl_endpoint");
 
          when others =>
             Put ("ghdl_rtik_#");
@@ -773,13 +775,7 @@ package body Grt.Disp_Rti is
       end loop;
    end Disp_For_Generate;
 
-   procedure Disp_Object (Obj : Ghdl_Rtin_Object_Acc;
-                          Is_Sig : Boolean;
-                          Ctxt : Rti_Context;
-                          Indent : Natural)
-   is
-      Addr : Address;
-      Obj_Type : Ghdl_Rti_Access;
+   procedure Disp_Obj_Header (Obj : Ghdl_Rtin_Object_Acc; Indent : Natural) is
    begin
       Disp_Indent (Indent);
       Disp_Kind (Obj.Common.Kind);
@@ -789,6 +785,18 @@ package body Grt.Disp_Rti is
       Put ("; ");
       Disp_Name (Obj.Name);
       Put (": ");
+   end Disp_Obj_Header;
+
+   procedure Disp_Object (Obj : Ghdl_Rtin_Object_Acc;
+                          Is_Sig : Boolean;
+                          Ctxt : Rti_Context;
+                          Indent : Natural)
+   is
+      Addr : Address;
+      Obj_Type : Ghdl_Rti_Access;
+   begin
+      Disp_Obj_Header (Obj, Indent);
+
       Addr := Loc_To_Addr (Obj.Common.Depth, Obj.Loc, Ctxt);
       Obj_Type := Obj.Obj_Type;
       Disp_Subtype_Indication (Obj_Type, Ctxt, Addr);
@@ -811,19 +819,32 @@ package body Grt.Disp_Rti is
    is
       Addr : Address;
    begin
-      Disp_Indent (Indent);
-      Disp_Kind (Obj.Common.Kind);
-      Disp_Depth (Obj.Common.Depth);
-      Put (", ");
-      Disp_Linecol (Obj.Linecol);
-      Put ("; ");
-      Disp_Name (Obj.Name);
-      Put (": count = ");
+      Disp_Obj_Header (Obj, Indent);
+      Put ("count = ");
       Addr := Loc_To_Addr (Obj.Common.Depth, Obj.Loc, Ctxt);
       Put_U32 (stdout, Ghdl_U32 (To_Ghdl_Index_Ptr (Addr).all));
       New_Line;
    end Disp_Psl_Directive;
 
+   procedure Disp_Psl_Endpoint_Directive (Obj : Ghdl_Rtin_Object_Acc;
+                                          Ctxt : Rti_Context;
+                                          Indent : Natural)
+   is
+      Addr : Address;
+      C : Character;
+   begin
+      Disp_Obj_Header (Obj, Indent);
+      Put ("endpoint = ");
+      Addr := Loc_To_Addr (Obj.Common.Depth, Obj.Loc, Ctxt);
+      if To_Ghdl_Value_Ptr (Addr).B1 then
+         C := 'T';
+      else
+         C := 'F';
+      end if;
+      Put (stdout, C);
+      New_Line;
+   end Disp_Psl_Endpoint_Directive;
+
    procedure Disp_Attribute (Obj : Ghdl_Rtin_Object_Acc;
                              Ctxt : Rti_Context;
                              Indent : Natural)
@@ -1180,6 +1201,9 @@ package body Grt.Disp_Rti is
          when Ghdl_Rtik_Psl_Cover
            | Ghdl_Rtik_Psl_Assert =>
             Disp_Psl_Directive (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent);
+         when Ghdl_Rtik_Psl_Endpoint =>
+            Disp_Psl_Endpoint_Directive
+              (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent);
          when others =>
             Disp_Indent (Indent);
             Disp_Kind (Rti.Kind);
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
index 0ff366f89..04c338a21 100644
--- a/src/grt/grt-psl.adb
+++ b/src/grt/grt-psl.adb
@@ -171,7 +171,7 @@ package body Grt.Psl is
 
       Report_Stream := F;
       Status := Psl_Traverse_Blocks (Get_Top_Context);
-      pragma Assert (Status = Traverse_Ok);
+      pragma Assert (Status = Traverse_Ok or Status = Traverse_Skip);
 
       Put_Line (F, "],");
       Put_Line (F, " ""summary"" : {");
diff --git a/src/grt/grt-rtis.ads b/src/grt/grt-rtis.ads
index 06e09647c..97687ba33 100644
--- a/src/grt/grt-rtis.ads
+++ b/src/grt/grt-rtis.ads
@@ -89,6 +89,8 @@ package Grt.Rtis is
       Ghdl_Rtik_Attribute_Stable,
       Ghdl_Rtik_Psl_Assert,
       Ghdl_Rtik_Psl_Cover,
+      Ghdl_Rtik_Psl_Endpoint,
+
       Ghdl_Rtik_Error);
    for Ghdl_Rtik'Size use 8;
 
diff --git a/src/psl/psl-nodes.adb b/src/psl/psl-nodes.adb
index 263994d21..d7de320a8 100644
--- a/src/psl/psl-nodes.adb
+++ b/src/psl/psl-nodes.adb
@@ -346,6 +346,7 @@ package body PSL.Nodes is
            | N_Concat_SERE
            | N_Fusion_SERE
            | N_Within_SERE
+           | N_Clocked_SERE
            | N_Overlap_Imp_Seq
            | N_Imp_Seq
            | N_And_Seq
@@ -442,6 +443,7 @@ package body PSL.Nodes is
            | N_Concat_SERE
            | N_Fusion_SERE
            | N_Within_SERE
+           | N_Clocked_SERE
            | N_Match_And_Seq
            | N_And_Seq
            | N_Or_Seq
diff --git a/src/psl/psl-nodes.adb.in b/src/psl/psl-nodes.adb.in
index 0ab97b572..220ffee71 100644
--- a/src/psl/psl-nodes.adb.in
+++ b/src/psl/psl-nodes.adb.in
@@ -346,6 +346,7 @@ package body PSL.Nodes is
            | N_Concat_SERE
            | N_Fusion_SERE
            | N_Within_SERE
+           | N_Clocked_SERE
            | N_Overlap_Imp_Seq
            | N_Imp_Seq
            | N_And_Seq
diff --git a/src/psl/psl-nodes.ads b/src/psl/psl-nodes.ads
index 9d6388c1d..b3887a075 100644
--- a/src/psl/psl-nodes.ads
+++ b/src/psl/psl-nodes.ads
@@ -72,6 +72,7 @@ package PSL.Nodes is
       N_Concat_SERE,
       N_Fusion_SERE,
       N_Within_SERE,
+      N_Clocked_SERE,
 
       N_Match_And_Seq,  --  &&
       N_And_Seq,
@@ -254,6 +255,12 @@ package PSL.Nodes is
    --
    --   Get/Set_SERE (Field1)
 
+   -- N_Clocked_SERE (Short)
+   --
+   --   Get/Set_SERE (Field1)
+   --
+   --   Get/Set_Boolean (Field3)
+
    -- N_Concat_SERE (Short)
    -- N_Fusion_SERE (Short)
    -- N_Within_SERE (Short)
diff --git a/src/psl/psl-nodes_meta.adb b/src/psl/psl-nodes_meta.adb
index 2559ec4a6..d84f3092c 100644
--- a/src/psl/psl-nodes_meta.adb
+++ b/src/psl/psl-nodes_meta.adb
@@ -211,6 +211,8 @@ package body PSL.Nodes_Meta is
             return "fusion_sere";
          when N_Within_SERE =>
             return "within_sere";
+         when N_Clocked_SERE =>
+            return "clocked_sere";
          when N_Match_And_Seq =>
             return "match_and_seq";
          when N_And_Seq =>
@@ -473,6 +475,9 @@ package body PSL.Nodes_Meta is
       --  N_Within_SERE
       Field_Left,
       Field_Right,
+      --  N_Clocked_SERE
+      Field_SERE,
+      Field_Boolean,
       --  N_Match_And_Seq
       Field_Left,
       Field_Right,
@@ -583,24 +588,25 @@ package body PSL.Nodes_Meta is
       N_Concat_SERE => 106,
       N_Fusion_SERE => 108,
       N_Within_SERE => 110,
-      N_Match_And_Seq => 112,
-      N_And_Seq => 114,
-      N_Or_Seq => 116,
-      N_Star_Repeat_Seq => 119,
-      N_Goto_Repeat_Seq => 122,
-      N_Plus_Repeat_Seq => 123,
-      N_Equal_Repeat_Seq => 126,
-      N_Not_Bool => 130,
-      N_And_Bool => 135,
-      N_Or_Bool => 140,
-      N_Imp_Bool => 145,
-      N_HDL_Expr => 150,
-      N_False => 150,
-      N_True => 150,
-      N_EOS => 153,
-      N_Name => 155,
-      N_Name_Decl => 157,
-      N_Number => 158
+      N_Clocked_SERE => 112,
+      N_Match_And_Seq => 114,
+      N_And_Seq => 116,
+      N_Or_Seq => 118,
+      N_Star_Repeat_Seq => 121,
+      N_Goto_Repeat_Seq => 124,
+      N_Plus_Repeat_Seq => 125,
+      N_Equal_Repeat_Seq => 128,
+      N_Not_Bool => 132,
+      N_And_Bool => 137,
+      N_Or_Bool => 142,
+      N_Imp_Bool => 147,
+      N_HDL_Expr => 152,
+      N_False => 152,
+      N_True => 152,
+      N_EOS => 155,
+      N_Name => 157,
+      N_Name_Decl => 159,
+      N_Number => 160
      );
 
    function Get_Fields (K : Nkind) return Fields_Array
@@ -1015,7 +1021,13 @@ package body PSL.Nodes_Meta is
 
    function Has_SERE (K : Nkind) return Boolean is
    begin
-      return K = N_Braced_SERE;
+      case K is
+         when N_Braced_SERE
+           | N_Clocked_SERE =>
+            return True;
+         when others =>
+            return False;
+      end case;
    end Has_SERE;
 
    function Has_Left (K : Nkind) return Boolean is
@@ -1165,6 +1177,7 @@ package body PSL.Nodes_Meta is
            | N_Next_Event_A
            | N_Next_Event_E
            | N_Abort
+           | N_Clocked_SERE
            | N_Not_Bool =>
             return True;
          when others =>
diff --git a/src/psl/psl-rewrites.adb b/src/psl/psl-rewrites.adb
index 173f4da94..de88939de 100644
--- a/src/psl/psl-rewrites.adb
+++ b/src/psl/psl-rewrites.adb
@@ -294,6 +294,10 @@ package body PSL.Rewrites is
             return Rewrite_Equal_Repeat_Seq (N);
          when N_Braced_SERE =>
             return Rewrite_SERE (Get_SERE (N));
+         when N_Clocked_SERE =>
+            Set_SERE (N, Rewrite_SERE (Get_SERE (N)));
+            Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N)));
+            return N;
          when N_Within_SERE =>
             Set_Left (N, Rewrite_SERE (Get_Left (N)));
             Set_Right (N, Rewrite_SERE (Get_Right (N)));
diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb
index 6b0e5d50c..520cc32ff 100644
--- a/src/psl/psl-subsets.adb
+++ b/src/psl/psl-subsets.adb
@@ -120,7 +120,8 @@ package body PSL.Subsets is
            | N_Eventually
            | N_Strong =>
             Check_Simple (Get_Property (N));
-         when N_Braced_SERE =>
+         when N_Braced_SERE
+           | N_Clocked_SERE =>
             Check_Simple (Get_SERE (N));
          when N_Concat_SERE
            | N_Fusion_SERE
diff --git a/src/vhdl/canon.adb b/src/vhdl/canon.adb
index bf4536088..129ce95da 100644
--- a/src/vhdl/canon.adb
+++ b/src/vhdl/canon.adb
@@ -235,6 +235,18 @@ package body Canon is
                Add_Element (Sensitivity_List, Expr);
             end if;
 
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            declare
+               List : constant Iir_List := Get_PSL_Clock_Sensitivity (Expr);
+               El : Iir;
+            begin
+               for I in Natural loop
+                  El := Get_Nth_Element (List, I);
+                  exit when El = Null_Iir;
+                  Add_Element (Sensitivity_List, El);
+               end loop;
+            end;
+
          when Iir_Kind_Object_Alias_Declaration =>
             Canon_Extract_Sensitivity
               (Get_Name (Expr), Sensitivity_List, Is_Target);
@@ -1636,15 +1648,14 @@ package body Canon is
       return False;
    end Psl_Need_Finalizer;
 
-   procedure Canon_Psl_Directive (Stmt : Iir)
+   --  Size the NFA and extract clock sensitivity.
+   procedure Canon_Psl_Clocked_NFA (Stmt : Iir)
    is
       use PSL.Nodes;
-      Fa : PSL_NFA;
+      Fa : constant PSL_NFA := Get_PSL_NFA (Stmt);
       Num : Natural;
       List : Iir_List;
    begin
-      Fa := Get_PSL_NFA (Stmt);
-
       PSL.NFAs.Labelize_States (Fa, Num);
       Set_PSL_Nbr_States (Stmt, Int32 (Num));
 
@@ -1653,6 +1664,11 @@ package body Canon is
       List := Create_Iir_List;
       Canon_PSL.Canon_Extract_Sensitivity (Get_PSL_Clock (Stmt), List);
       Set_PSL_Clock_Sensitivity (Stmt, List);
+   end Canon_Psl_Clocked_NFA;
+
+   procedure Canon_Psl_Directive (Stmt : Iir) is
+   begin
+      Canon_Psl_Clocked_NFA (Stmt);
 
       if Canon_Flag_Expressions then
          Canon_PSL_Expression (Get_PSL_Clock (Stmt));
@@ -1693,7 +1709,8 @@ package body Canon is
          --  Add a label if required.
          if Canon_Flag_Add_Labels then
             case Get_Kind (El) is
-               when Iir_Kind_Psl_Declaration =>
+               when Iir_Kind_Psl_Declaration
+                 | Iir_Kind_Psl_Endpoint_Declaration =>
                   null;
                when others =>
                   if Get_Label (El) = Null_Identifier then
@@ -1961,11 +1978,10 @@ package body Canon is
             when Iir_Kind_Psl_Declaration =>
                declare
                   use PSL.Nodes;
-                  Decl : PSL_Node;
+                  Decl : constant PSL_Node := Get_Psl_Declaration (El);
                   Prop : PSL_Node;
                   Fa : PSL_NFA;
                begin
-                  Decl := Get_Psl_Declaration (El);
                   case Get_Kind (Decl) is
                      when N_Property_Declaration =>
                         Prop := Get_Property (Decl);
@@ -1985,6 +2001,22 @@ package body Canon is
                         Error_Kind ("canon psl_declaration", Decl);
                   end case;
                end;
+            when Iir_Kind_Psl_Endpoint_Declaration =>
+               declare
+                  use PSL.Nodes;
+                  Decl : constant PSL_Node := Get_Psl_Declaration (El);
+                  Seq : PSL_Node;
+                  Fa : PSL_NFA;
+               begin
+                  pragma Assert (Get_Parameter_List (Decl) = Null_Node);
+                  Seq := Get_Sequence (Decl);
+                  Seq := PSL.Rewrites.Rewrite_SERE (Seq);
+                  Set_Sequence (Decl, Seq);
+                  --  Generate the NFA.
+                  Fa := PSL.Build.Build_SERE_FA (Seq);
+                  Set_PSL_NFA (El, Fa);
+                  Canon_Psl_Clocked_NFA (El);
+               end;
 
             when Iir_Kind_Simple_Simultaneous_Statement =>
                if Canon_Flag_Expressions then
@@ -2845,6 +2877,7 @@ package body Canon is
               | Iir_Kind_Psl_Cover_Statement
               | Iir_Kind_Psl_Default_Clock
               | Iir_Kind_Psl_Declaration
+              | Iir_Kind_Psl_Endpoint_Declaration
               | Iir_Kind_Simple_Simultaneous_Statement =>
                null;
 
diff --git a/src/vhdl/configuration.adb b/src/vhdl/configuration.adb
index e7890da62..dea38ce13 100644
--- a/src/vhdl/configuration.adb
+++ b/src/vhdl/configuration.adb
@@ -244,6 +244,7 @@ package body Configuration is
               | Iir_Kind_Psl_Cover_Statement
               | Iir_Kind_Psl_Default_Clock
               | Iir_Kind_Psl_Declaration
+              | Iir_Kind_Psl_Endpoint_Declaration
               | Iir_Kind_Simple_Simultaneous_Statement =>
                null;
             when others =>
diff --git a/src/vhdl/disp_vhdl.adb b/src/vhdl/disp_vhdl.adb
index 4cccdf576..ffe8e3f10 100644
--- a/src/vhdl/disp_vhdl.adb
+++ b/src/vhdl/disp_vhdl.adb
@@ -1142,7 +1142,8 @@ package body Disp_Vhdl is
       Disp_Interface_Chain (Get_Generic_Chain (Parent), ";");
    end Disp_Generics;
 
-   procedure Disp_Entity_Declaration (Decl: Iir_Entity_Declaration) is
+   procedure Disp_Entity_Declaration (Decl: Iir_Entity_Declaration)
+   is
       Start: constant Count := Col;
    begin
       Put ("entity ");
@@ -2997,15 +2998,23 @@ package body Disp_Vhdl is
             Disp_Ident (Get_Identifier (Decl));
             Put (" is ");
             Disp_Psl_Expression (Get_Property (Decl));
+            Put_Line (";");
          when N_Sequence_Declaration =>
             Put ("sequence ");
             Disp_Ident (Get_Identifier (Decl));
             Put (" is ");
             Disp_Psl_Sequence (Get_Sequence (Decl));
+            Put_Line (";");
+         when N_Endpoint_Declaration =>
+            Put ("endpoint ");
+            Disp_Ident (Get_Identifier (Decl));
+            Put (" is ");
+            Disp_Psl_Sequence (Get_Sequence (Decl));
+            Put_Line (";");
+            Disp_PSL_NFA (Get_PSL_NFA (Stmt));
          when others =>
             Error_Kind ("disp_psl_declaration", Decl);
       end case;
-      Put_Line (";");
    end Disp_Psl_Declaration;
 
    procedure Disp_PSL_NFA (N : PSL.Nodes.NFA)
@@ -3105,7 +3114,8 @@ package body Disp_Vhdl is
             Disp_For_Generate_Statement (Stmt);
          when Iir_Kind_Psl_Default_Clock =>
             Disp_Psl_Default_Clock (Stmt);
-         when Iir_Kind_Psl_Declaration =>
+         when Iir_Kind_Psl_Declaration
+           | Iir_Kind_Psl_Endpoint_Declaration =>
             Disp_Psl_Declaration (Stmt);
          when Iir_Kind_Psl_Assert_Statement =>
             Disp_Psl_Assert_Statement (Stmt);
diff --git a/src/vhdl/iirs.ads b/src/vhdl/iirs.ads
index fd13136cc..08b37b200 100644
--- a/src/vhdl/iirs.ads
+++ b/src/vhdl/iirs.ads
@@ -1658,6 +1658,14 @@ package Iirs is
    --
    --   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)
    --
    --   Get/Set_Use_Flag (Flag6)
diff --git a/src/vhdl/nodes_meta.adb b/src/vhdl/nodes_meta.adb
index 0b0df4d35..6e0de124a 100644
--- a/src/vhdl/nodes_meta.adb
+++ b/src/vhdl/nodes_meta.adb
@@ -2738,9 +2738,12 @@ package body Nodes_Meta is
       Field_Psl_Declaration,
       Field_PSL_Clock,
       Field_PSL_NFA,
+      Field_PSL_Nbr_States,
+      Field_PSL_EOS_Flag,
       Field_Visible_Flag,
       Field_Use_Flag,
       Field_Expr_Staticness,
+      Field_PSL_Clock_Sensitivity,
       Field_Chain,
       Field_Parent,
       Field_Type,
@@ -4152,170 +4155,170 @@ package body Nodes_Meta is
       Iir_Kind_Element_Declaration => 559,
       Iir_Kind_Non_Object_Alias_Declaration => 567,
       Iir_Kind_Psl_Declaration => 575,
-      Iir_Kind_Psl_Endpoint_Declaration => 585,
-      Iir_Kind_Terminal_Declaration => 591,
-      Iir_Kind_Free_Quantity_Declaration => 600,
-      Iir_Kind_Across_Quantity_Declaration => 612,
-      Iir_Kind_Through_Quantity_Declaration => 624,
-      Iir_Kind_Enumeration_Literal => 635,
-      Iir_Kind_Function_Declaration => 659,
-      Iir_Kind_Procedure_Declaration => 682,
-      Iir_Kind_Function_Body => 692,
-      Iir_Kind_Procedure_Body => 703,
-      Iir_Kind_Object_Alias_Declaration => 715,
-      Iir_Kind_File_Declaration => 730,
-      Iir_Kind_Guard_Signal_Declaration => 743,
-      Iir_Kind_Signal_Declaration => 760,
-      Iir_Kind_Variable_Declaration => 773,
-      Iir_Kind_Constant_Declaration => 787,
-      Iir_Kind_Iterator_Declaration => 799,
-      Iir_Kind_Interface_Constant_Declaration => 815,
-      Iir_Kind_Interface_Variable_Declaration => 831,
-      Iir_Kind_Interface_Signal_Declaration => 852,
-      Iir_Kind_Interface_File_Declaration => 868,
-      Iir_Kind_Interface_Package_Declaration => 877,
-      Iir_Kind_Identity_Operator => 881,
-      Iir_Kind_Negation_Operator => 885,
-      Iir_Kind_Absolute_Operator => 889,
-      Iir_Kind_Not_Operator => 893,
-      Iir_Kind_Condition_Operator => 897,
-      Iir_Kind_Reduction_And_Operator => 901,
-      Iir_Kind_Reduction_Or_Operator => 905,
-      Iir_Kind_Reduction_Nand_Operator => 909,
-      Iir_Kind_Reduction_Nor_Operator => 913,
-      Iir_Kind_Reduction_Xor_Operator => 917,
-      Iir_Kind_Reduction_Xnor_Operator => 921,
-      Iir_Kind_And_Operator => 926,
-      Iir_Kind_Or_Operator => 931,
-      Iir_Kind_Nand_Operator => 936,
-      Iir_Kind_Nor_Operator => 941,
-      Iir_Kind_Xor_Operator => 946,
-      Iir_Kind_Xnor_Operator => 951,
-      Iir_Kind_Equality_Operator => 956,
-      Iir_Kind_Inequality_Operator => 961,
-      Iir_Kind_Less_Than_Operator => 966,
-      Iir_Kind_Less_Than_Or_Equal_Operator => 971,
-      Iir_Kind_Greater_Than_Operator => 976,
-      Iir_Kind_Greater_Than_Or_Equal_Operator => 981,
-      Iir_Kind_Match_Equality_Operator => 986,
-      Iir_Kind_Match_Inequality_Operator => 991,
-      Iir_Kind_Match_Less_Than_Operator => 996,
-      Iir_Kind_Match_Less_Than_Or_Equal_Operator => 1001,
-      Iir_Kind_Match_Greater_Than_Operator => 1006,
-      Iir_Kind_Match_Greater_Than_Or_Equal_Operator => 1011,
-      Iir_Kind_Sll_Operator => 1016,
-      Iir_Kind_Sla_Operator => 1021,
-      Iir_Kind_Srl_Operator => 1026,
-      Iir_Kind_Sra_Operator => 1031,
-      Iir_Kind_Rol_Operator => 1036,
-      Iir_Kind_Ror_Operator => 1041,
-      Iir_Kind_Addition_Operator => 1046,
-      Iir_Kind_Substraction_Operator => 1051,
-      Iir_Kind_Concatenation_Operator => 1056,
-      Iir_Kind_Multiplication_Operator => 1061,
-      Iir_Kind_Division_Operator => 1066,
-      Iir_Kind_Modulus_Operator => 1071,
-      Iir_Kind_Remainder_Operator => 1076,
-      Iir_Kind_Exponentiation_Operator => 1081,
-      Iir_Kind_Function_Call => 1089,
-      Iir_Kind_Aggregate => 1095,
-      Iir_Kind_Parenthesis_Expression => 1098,
-      Iir_Kind_Qualified_Expression => 1102,
-      Iir_Kind_Type_Conversion => 1107,
-      Iir_Kind_Allocator_By_Expression => 1111,
-      Iir_Kind_Allocator_By_Subtype => 1117,
-      Iir_Kind_Selected_Element => 1123,
-      Iir_Kind_Dereference => 1128,
-      Iir_Kind_Implicit_Dereference => 1133,
-      Iir_Kind_Slice_Name => 1140,
-      Iir_Kind_Indexed_Name => 1146,
-      Iir_Kind_Psl_Expression => 1148,
-      Iir_Kind_Sensitized_Process_Statement => 1168,
-      Iir_Kind_Process_Statement => 1188,
-      Iir_Kind_Concurrent_Simple_Signal_Assignment => 1199,
-      Iir_Kind_Concurrent_Conditional_Signal_Assignment => 1210,
-      Iir_Kind_Concurrent_Selected_Signal_Assignment => 1222,
-      Iir_Kind_Concurrent_Assertion_Statement => 1230,
-      Iir_Kind_Psl_Default_Clock => 1234,
-      Iir_Kind_Psl_Assert_Statement => 1246,
-      Iir_Kind_Psl_Cover_Statement => 1258,
-      Iir_Kind_Concurrent_Procedure_Call_Statement => 1265,
-      Iir_Kind_Block_Statement => 1278,
-      Iir_Kind_If_Generate_Statement => 1288,
-      Iir_Kind_For_Generate_Statement => 1297,
-      Iir_Kind_Component_Instantiation_Statement => 1307,
-      Iir_Kind_Simple_Simultaneous_Statement => 1314,
-      Iir_Kind_Generate_Statement_Body => 1325,
-      Iir_Kind_If_Generate_Else_Clause => 1330,
-      Iir_Kind_Simple_Signal_Assignment_Statement => 1339,
-      Iir_Kind_Conditional_Signal_Assignment_Statement => 1348,
-      Iir_Kind_Null_Statement => 1352,
-      Iir_Kind_Assertion_Statement => 1359,
-      Iir_Kind_Report_Statement => 1365,
-      Iir_Kind_Wait_Statement => 1372,
-      Iir_Kind_Variable_Assignment_Statement => 1378,
-      Iir_Kind_Conditional_Variable_Assignment_Statement => 1384,
-      Iir_Kind_Return_Statement => 1390,
-      Iir_Kind_For_Loop_Statement => 1399,
-      Iir_Kind_While_Loop_Statement => 1407,
-      Iir_Kind_Next_Statement => 1413,
-      Iir_Kind_Exit_Statement => 1419,
-      Iir_Kind_Case_Statement => 1427,
-      Iir_Kind_Procedure_Call_Statement => 1433,
-      Iir_Kind_If_Statement => 1442,
-      Iir_Kind_Elsif => 1447,
-      Iir_Kind_Character_Literal => 1454,
-      Iir_Kind_Simple_Name => 1461,
-      Iir_Kind_Selected_Name => 1469,
-      Iir_Kind_Operator_Symbol => 1474,
-      Iir_Kind_Selected_By_All_Name => 1479,
-      Iir_Kind_Parenthesis_Name => 1483,
-      Iir_Kind_External_Constant_Name => 1492,
-      Iir_Kind_External_Signal_Name => 1501,
-      Iir_Kind_External_Variable_Name => 1510,
-      Iir_Kind_Package_Pathname => 1513,
-      Iir_Kind_Absolute_Pathname => 1514,
-      Iir_Kind_Relative_Pathname => 1515,
-      Iir_Kind_Pathname_Element => 1519,
-      Iir_Kind_Base_Attribute => 1521,
-      Iir_Kind_Left_Type_Attribute => 1526,
-      Iir_Kind_Right_Type_Attribute => 1531,
-      Iir_Kind_High_Type_Attribute => 1536,
-      Iir_Kind_Low_Type_Attribute => 1541,
-      Iir_Kind_Ascending_Type_Attribute => 1546,
-      Iir_Kind_Image_Attribute => 1552,
-      Iir_Kind_Value_Attribute => 1558,
-      Iir_Kind_Pos_Attribute => 1564,
-      Iir_Kind_Val_Attribute => 1570,
-      Iir_Kind_Succ_Attribute => 1576,
-      Iir_Kind_Pred_Attribute => 1582,
-      Iir_Kind_Leftof_Attribute => 1588,
-      Iir_Kind_Rightof_Attribute => 1594,
-      Iir_Kind_Delayed_Attribute => 1602,
-      Iir_Kind_Stable_Attribute => 1610,
-      Iir_Kind_Quiet_Attribute => 1618,
-      Iir_Kind_Transaction_Attribute => 1626,
-      Iir_Kind_Event_Attribute => 1630,
-      Iir_Kind_Active_Attribute => 1634,
-      Iir_Kind_Last_Event_Attribute => 1638,
-      Iir_Kind_Last_Active_Attribute => 1642,
-      Iir_Kind_Last_Value_Attribute => 1646,
-      Iir_Kind_Driving_Attribute => 1650,
-      Iir_Kind_Driving_Value_Attribute => 1654,
-      Iir_Kind_Behavior_Attribute => 1654,
-      Iir_Kind_Structure_Attribute => 1654,
-      Iir_Kind_Simple_Name_Attribute => 1661,
-      Iir_Kind_Instance_Name_Attribute => 1666,
-      Iir_Kind_Path_Name_Attribute => 1671,
-      Iir_Kind_Left_Array_Attribute => 1678,
-      Iir_Kind_Right_Array_Attribute => 1685,
-      Iir_Kind_High_Array_Attribute => 1692,
-      Iir_Kind_Low_Array_Attribute => 1699,
-      Iir_Kind_Length_Array_Attribute => 1706,
-      Iir_Kind_Ascending_Array_Attribute => 1713,
-      Iir_Kind_Range_Array_Attribute => 1720,
-      Iir_Kind_Reverse_Range_Array_Attribute => 1727,
-      Iir_Kind_Attribute_Name => 1735
+      Iir_Kind_Psl_Endpoint_Declaration => 588,
+      Iir_Kind_Terminal_Declaration => 594,
+      Iir_Kind_Free_Quantity_Declaration => 603,
+      Iir_Kind_Across_Quantity_Declaration => 615,
+      Iir_Kind_Through_Quantity_Declaration => 627,
+      Iir_Kind_Enumeration_Literal => 638,
+      Iir_Kind_Function_Declaration => 662,
+      Iir_Kind_Procedure_Declaration => 685,
+      Iir_Kind_Function_Body => 695,
+      Iir_Kind_Procedure_Body => 706,
+      Iir_Kind_Object_Alias_Declaration => 718,
+      Iir_Kind_File_Declaration => 733,
+      Iir_Kind_Guard_Signal_Declaration => 746,
+      Iir_Kind_Signal_Declaration => 763,
+      Iir_Kind_Variable_Declaration => 776,
+      Iir_Kind_Constant_Declaration => 790,
+      Iir_Kind_Iterator_Declaration => 802,
+      Iir_Kind_Interface_Constant_Declaration => 818,
+      Iir_Kind_Interface_Variable_Declaration => 834,
+      Iir_Kind_Interface_Signal_Declaration => 855,
+      Iir_Kind_Interface_File_Declaration => 871,
+      Iir_Kind_Interface_Package_Declaration => 880,
+      Iir_Kind_Identity_Operator => 884,
+      Iir_Kind_Negation_Operator => 888,
+      Iir_Kind_Absolute_Operator => 892,
+      Iir_Kind_Not_Operator => 896,
+      Iir_Kind_Condition_Operator => 900,
+      Iir_Kind_Reduction_And_Operator => 904,
+      Iir_Kind_Reduction_Or_Operator => 908,
+      Iir_Kind_Reduction_Nand_Operator => 912,
+      Iir_Kind_Reduction_Nor_Operator => 916,
+      Iir_Kind_Reduction_Xor_Operator => 920,
+      Iir_Kind_Reduction_Xnor_Operator => 924,
+      Iir_Kind_And_Operator => 929,
+      Iir_Kind_Or_Operator => 934,
+      Iir_Kind_Nand_Operator => 939,
+      Iir_Kind_Nor_Operator => 944,
+      Iir_Kind_Xor_Operator => 949,
+      Iir_Kind_Xnor_Operator => 954,
+      Iir_Kind_Equality_Operator => 959,
+      Iir_Kind_Inequality_Operator => 964,
+      Iir_Kind_Less_Than_Operator => 969,
+      Iir_Kind_Less_Than_Or_Equal_Operator => 974,
+      Iir_Kind_Greater_Than_Operator => 979,
+      Iir_Kind_Greater_Than_Or_Equal_Operator => 984,
+      Iir_Kind_Match_Equality_Operator => 989,
+      Iir_Kind_Match_Inequality_Operator => 994,
+      Iir_Kind_Match_Less_Than_Operator => 999,
+      Iir_Kind_Match_Less_Than_Or_Equal_Operator => 1004,
+      Iir_Kind_Match_Greater_Than_Operator => 1009,
+      Iir_Kind_Match_Greater_Than_Or_Equal_Operator => 1014,
+      Iir_Kind_Sll_Operator => 1019,
+      Iir_Kind_Sla_Operator => 1024,
+      Iir_Kind_Srl_Operator => 1029,
+      Iir_Kind_Sra_Operator => 1034,
+      Iir_Kind_Rol_Operator => 1039,
+      Iir_Kind_Ror_Operator => 1044,
+      Iir_Kind_Addition_Operator => 1049,
+      Iir_Kind_Substraction_Operator => 1054,
+      Iir_Kind_Concatenation_Operator => 1059,
+      Iir_Kind_Multiplication_Operator => 1064,
+      Iir_Kind_Division_Operator => 1069,
+      Iir_Kind_Modulus_Operator => 1074,
+      Iir_Kind_Remainder_Operator => 1079,
+      Iir_Kind_Exponentiation_Operator => 1084,
+      Iir_Kind_Function_Call => 1092,
+      Iir_Kind_Aggregate => 1098,
+      Iir_Kind_Parenthesis_Expression => 1101,
+      Iir_Kind_Qualified_Expression => 1105,
+      Iir_Kind_Type_Conversion => 1110,
+      Iir_Kind_Allocator_By_Expression => 1114,
+      Iir_Kind_Allocator_By_Subtype => 1120,
+      Iir_Kind_Selected_Element => 1126,
+      Iir_Kind_Dereference => 1131,
+      Iir_Kind_Implicit_Dereference => 1136,
+      Iir_Kind_Slice_Name => 1143,
+      Iir_Kind_Indexed_Name => 1149,
+      Iir_Kind_Psl_Expression => 1151,
+      Iir_Kind_Sensitized_Process_Statement => 1171,
+      Iir_Kind_Process_Statement => 1191,
+      Iir_Kind_Concurrent_Simple_Signal_Assignment => 1202,
+      Iir_Kind_Concurrent_Conditional_Signal_Assignment => 1213,
+      Iir_Kind_Concurrent_Selected_Signal_Assignment => 1225,
+      Iir_Kind_Concurrent_Assertion_Statement => 1233,
+      Iir_Kind_Psl_Default_Clock => 1237,
+      Iir_Kind_Psl_Assert_Statement => 1249,
+      Iir_Kind_Psl_Cover_Statement => 1261,
+      Iir_Kind_Concurrent_Procedure_Call_Statement => 1268,
+      Iir_Kind_Block_Statement => 1281,
+      Iir_Kind_If_Generate_Statement => 1291,
+      Iir_Kind_For_Generate_Statement => 1300,
+      Iir_Kind_Component_Instantiation_Statement => 1310,
+      Iir_Kind_Simple_Simultaneous_Statement => 1317,
+      Iir_Kind_Generate_Statement_Body => 1328,
+      Iir_Kind_If_Generate_Else_Clause => 1333,
+      Iir_Kind_Simple_Signal_Assignment_Statement => 1342,
+      Iir_Kind_Conditional_Signal_Assignment_Statement => 1351,
+      Iir_Kind_Null_Statement => 1355,
+      Iir_Kind_Assertion_Statement => 1362,
+      Iir_Kind_Report_Statement => 1368,
+      Iir_Kind_Wait_Statement => 1375,
+      Iir_Kind_Variable_Assignment_Statement => 1381,
+      Iir_Kind_Conditional_Variable_Assignment_Statement => 1387,
+      Iir_Kind_Return_Statement => 1393,
+      Iir_Kind_For_Loop_Statement => 1402,
+      Iir_Kind_While_Loop_Statement => 1410,
+      Iir_Kind_Next_Statement => 1416,
+      Iir_Kind_Exit_Statement => 1422,
+      Iir_Kind_Case_Statement => 1430,
+      Iir_Kind_Procedure_Call_Statement => 1436,
+      Iir_Kind_If_Statement => 1445,
+      Iir_Kind_Elsif => 1450,
+      Iir_Kind_Character_Literal => 1457,
+      Iir_Kind_Simple_Name => 1464,
+      Iir_Kind_Selected_Name => 1472,
+      Iir_Kind_Operator_Symbol => 1477,
+      Iir_Kind_Selected_By_All_Name => 1482,
+      Iir_Kind_Parenthesis_Name => 1486,
+      Iir_Kind_External_Constant_Name => 1495,
+      Iir_Kind_External_Signal_Name => 1504,
+      Iir_Kind_External_Variable_Name => 1513,
+      Iir_Kind_Package_Pathname => 1516,
+      Iir_Kind_Absolute_Pathname => 1517,
+      Iir_Kind_Relative_Pathname => 1518,
+      Iir_Kind_Pathname_Element => 1522,
+      Iir_Kind_Base_Attribute => 1524,
+      Iir_Kind_Left_Type_Attribute => 1529,
+      Iir_Kind_Right_Type_Attribute => 1534,
+      Iir_Kind_High_Type_Attribute => 1539,
+      Iir_Kind_Low_Type_Attribute => 1544,
+      Iir_Kind_Ascending_Type_Attribute => 1549,
+      Iir_Kind_Image_Attribute => 1555,
+      Iir_Kind_Value_Attribute => 1561,
+      Iir_Kind_Pos_Attribute => 1567,
+      Iir_Kind_Val_Attribute => 1573,
+      Iir_Kind_Succ_Attribute => 1579,
+      Iir_Kind_Pred_Attribute => 1585,
+      Iir_Kind_Leftof_Attribute => 1591,
+      Iir_Kind_Rightof_Attribute => 1597,
+      Iir_Kind_Delayed_Attribute => 1605,
+      Iir_Kind_Stable_Attribute => 1613,
+      Iir_Kind_Quiet_Attribute => 1621,
+      Iir_Kind_Transaction_Attribute => 1629,
+      Iir_Kind_Event_Attribute => 1633,
+      Iir_Kind_Active_Attribute => 1637,
+      Iir_Kind_Last_Event_Attribute => 1641,
+      Iir_Kind_Last_Active_Attribute => 1645,
+      Iir_Kind_Last_Value_Attribute => 1649,
+      Iir_Kind_Driving_Attribute => 1653,
+      Iir_Kind_Driving_Value_Attribute => 1657,
+      Iir_Kind_Behavior_Attribute => 1657,
+      Iir_Kind_Structure_Attribute => 1657,
+      Iir_Kind_Simple_Name_Attribute => 1664,
+      Iir_Kind_Instance_Name_Attribute => 1669,
+      Iir_Kind_Path_Name_Attribute => 1674,
+      Iir_Kind_Left_Array_Attribute => 1681,
+      Iir_Kind_Right_Array_Attribute => 1688,
+      Iir_Kind_High_Array_Attribute => 1695,
+      Iir_Kind_Low_Array_Attribute => 1702,
+      Iir_Kind_Length_Array_Attribute => 1709,
+      Iir_Kind_Ascending_Array_Attribute => 1716,
+      Iir_Kind_Range_Array_Attribute => 1723,
+      Iir_Kind_Reverse_Range_Array_Attribute => 1730,
+      Iir_Kind_Attribute_Name => 1738
      );
 
    function Get_Fields (K : Iir_Kind) return Fields_Array
@@ -9850,7 +9853,8 @@ package body Nodes_Meta is
    function Has_PSL_Nbr_States (K : Iir_Kind) return Boolean is
    begin
       case K is
-         when Iir_Kind_Psl_Assert_Statement
+         when Iir_Kind_Psl_Endpoint_Declaration
+           | Iir_Kind_Psl_Assert_Statement
            | Iir_Kind_Psl_Cover_Statement =>
             return True;
          when others =>
@@ -9861,7 +9865,8 @@ package body Nodes_Meta is
    function Has_PSL_Clock_Sensitivity (K : Iir_Kind) return Boolean is
    begin
       case K is
-         when Iir_Kind_Psl_Assert_Statement
+         when Iir_Kind_Psl_Endpoint_Declaration
+           | Iir_Kind_Psl_Assert_Statement
            | Iir_Kind_Psl_Cover_Statement =>
             return True;
          when others =>
@@ -9872,7 +9877,8 @@ package body Nodes_Meta is
    function Has_PSL_EOS_Flag (K : Iir_Kind) return Boolean is
    begin
       case K is
-         when Iir_Kind_Psl_Assert_Statement
+         when Iir_Kind_Psl_Endpoint_Declaration
+           | Iir_Kind_Psl_Assert_Statement
            | Iir_Kind_Psl_Cover_Statement =>
             return True;
          when others =>
diff --git a/src/vhdl/parse.adb b/src/vhdl/parse.adb
index 6acd718a5..bfe73eaec 100644
--- a/src/vhdl/parse.adb
+++ b/src/vhdl/parse.adb
@@ -6909,25 +6909,41 @@ package body Parse is
    function Parse_Psl_Declaration return Iir
    is
       Tok : constant Token_Type := Current_Token;
+      Loc : constant Location_Type := Get_Token_Location;
       Res : Iir;
+      Decl : PSL_Node;
+      Id : Name_Id;
    begin
-      Res := Create_Iir (Iir_Kind_Psl_Declaration);
-
       --  Skip 'property', 'sequence' or 'endpoint'.
       Scan;
 
       if Current_Token /= Tok_Identifier then
-         Error_Msg_Parse ("property name expected here");
+         Error_Msg_Parse ("declaration name expected here");
+         Id := Null_Identifier;
       else
-         Set_Identifier (Res, Current_Identifier);
+         Id := Current_Identifier;
       end if;
 
+      --  Parse PSL declaration.
       Scanner.Flag_Psl := True;
-      Set_Psl_Declaration (Res, Parse_Psl.Parse_Psl_Declaration (Tok));
+      Decl := Parse_Psl.Parse_Psl_Declaration (Tok);
       Expect (Tok_Semi_Colon);
       Scanner.Flag_Scan_In_Comment := False;
       Scanner.Flag_Psl := False;
 
+      if Tok = Tok_Psl_Endpoint
+        and then Parse_Psl.Is_Instantiated_Declaration (Decl)
+      then
+         --  Instantiated endpoint: make it visible from VHDL.
+         Res := Create_Iir (Iir_Kind_Psl_Endpoint_Declaration);
+      else
+         --  Otherwise, it will be visible only from PSL.
+         Res := Create_Iir (Iir_Kind_Psl_Declaration);
+      end if;
+      Set_Location (Res, Loc);
+      Set_Identifier (Res, Id);
+      Set_Psl_Declaration (Res, Decl);
+
       return Res;
    end Parse_Psl_Declaration;
 
diff --git a/src/vhdl/parse_psl.adb b/src/vhdl/parse_psl.adb
index a356043aa..4c682ae3f 100644
--- a/src/vhdl/parse_psl.adb
+++ b/src/vhdl/parse_psl.adb
@@ -289,6 +289,16 @@ package body Parse_Psl is
       case Current_Token is
          when Tok_Left_Curly =>
             Res := Parse_Braced_SERE;
+            if Current_Token = Tok_Arobase then
+               N := Create_Node_Loc (N_Clocked_SERE);
+               Set_SERE (N, Res);
+
+               --  Skip '@'
+               Scan;
+
+               Set_Boolean (N, Parse_Psl_Boolean);
+               Res := N;
+            end if;
          when Tok_Brack_Star =>
             return Parse_Maybe_Count (N_Star_Repeat_Seq, Null_Node);
          when Tok_Left_Paren =>
@@ -313,6 +323,8 @@ package body Parse_Psl is
             when Tok_Brack_Plus_Brack =>
                N := Create_Node_Loc (N_Plus_Repeat_Seq);
                Set_Sequence (N, Res);
+
+               --  Skip '[+]'
                Scan;
                Res := N;
             when Tok_Brack_Arrow =>
@@ -320,6 +332,8 @@ package body Parse_Psl is
             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
@@ -670,4 +684,9 @@ package body Parse_Psl is
       end case;
       return Res;
    end Parse_Psl_Declaration;
+
+   function Is_Instantiated_Declaration (N : PSL_Node) return Boolean is
+   begin
+      return Get_Parameter_List (N) = Null_Node;
+   end Is_Instantiated_Declaration;
 end Parse_Psl;
diff --git a/src/vhdl/parse_psl.ads b/src/vhdl/parse_psl.ads
index 160df668e..17989d8b3 100644
--- a/src/vhdl/parse_psl.ads
+++ b/src/vhdl/parse_psl.ads
@@ -24,4 +24,7 @@ package Parse_Psl is
    function Parse_Psl_Property return PSL_Node;
    function Parse_Psl_Boolean return PSL_Node;
    function Parse_Psl_Declaration (Tok : Token_Type) return PSL_Node;
+
+   --  True if endpoint declaration N is instantiated (ie has no parameters).
+   function Is_Instantiated_Declaration (N : PSL_Node) return Boolean;
 end Parse_Psl;
diff --git a/src/vhdl/sem_expr.adb b/src/vhdl/sem_expr.adb
index 684683d0c..415662a9f 100644
--- a/src/vhdl/sem_expr.adb
+++ b/src/vhdl/sem_expr.adb
@@ -429,6 +429,8 @@ package body Sem_Expr is
            | Iir_Kind_Type_Conversion
            | Iir_Kind_Function_Call =>
             return Expr;
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            return Expr;
          when Iir_Kind_Simple_Name
            | Iir_Kind_Parenthesis_Name
            | Iir_Kind_Attribute_Name
@@ -3894,6 +3896,8 @@ package body Sem_Expr is
                return;
             when Iir_Kinds_External_Name =>
                return;
+            when Iir_Kind_Psl_Endpoint_Declaration =>
+               return;
             when Iir_Kind_File_Declaration
               | Iir_Kind_Interface_File_Declaration =>
                --  LRM 4.3.2  Interface declarations
diff --git a/src/vhdl/sem_names.adb b/src/vhdl/sem_names.adb
index a65fd54ef..a4a6b44ca 100644
--- a/src/vhdl/sem_names.adb
+++ b/src/vhdl/sem_names.adb
@@ -1598,7 +1598,8 @@ package body Sem_Names is
             return Res;
          when Iir_Kind_Psl_Expression =>
             return Res;
-         when Iir_Kind_Psl_Declaration =>
+         when Iir_Kind_Psl_Declaration
+           | Iir_Kind_Psl_Endpoint_Declaration =>
             return Name;
          when Iir_Kind_Element_Declaration
            | Iir_Kind_Error =>
@@ -2512,7 +2513,8 @@ package body Sem_Names is
               (Disp_Node (Prefix) & " cannot be indexed or sliced", Name);
             Res := Null_Iir;
 
-         when Iir_Kind_Psl_Declaration =>
+         when Iir_Kind_Psl_Declaration
+           | Iir_Kind_Psl_Endpoint_Declaration =>
             Res := Sem_Psl.Sem_Psl_Name (Name);
 
          when Iir_Kinds_Library_Unit_Declaration =>
diff --git a/src/vhdl/sem_psl.adb b/src/vhdl/sem_psl.adb
index 280b0d90b..445b89d68 100644
--- a/src/vhdl/sem_psl.adb
+++ b/src/vhdl/sem_psl.adb
@@ -33,6 +33,8 @@ with Errorout; use Errorout;
 with Xrefs; use Xrefs;
 
 package body Sem_Psl is
+   procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out Node);
+
    --  Return TRUE iff Atype is a PSL boolean type.
    --  See PSL1.1 5.1.2  Boolean expressions
    function Is_Psl_Bool_Type (Atype : Iir) return Boolean
@@ -163,10 +165,6 @@ package body Sem_Psl is
                case Get_Kind (Decl) is
                   when N_Sequence_Declaration =>
                      Res := Create_Node (N_Sequence_Instance);
-                  when N_Endpoint_Declaration =>
-                     --  Endpoints are considered as boolean variables.
-                     Free_Node (N);
-                     return Convert_Bool (Name);
                   when N_Property_Declaration =>
                      Res := Create_Node (N_Property_Instance);
                   when N_Boolean_Parameter
@@ -257,6 +255,12 @@ package body Sem_Psl is
             Res := Sem_Sequence (Get_SERE (Seq));
             Set_SERE (Seq, Res);
             return Seq;
+         when N_Clocked_SERE =>
+            Res := Sem_Sequence (Get_SERE (Seq));
+            Set_SERE (Seq, Res);
+            Res := Sem_Boolean (Get_Boolean (Seq));
+            Set_Boolean (Seq, Res);
+            return Seq;
          when N_Concat_SERE
            | N_Fusion_SERE
            | N_Within_SERE
@@ -417,6 +421,9 @@ package body Sem_Psl is
          when N_Clock_Event =>
             Clk := Get_Boolean (Prop);
             Prop := Get_Property (Prop);
+         when N_Clocked_SERE =>
+            Clk := Get_Boolean (Prop);
+            Prop := Get_SERE (Prop);
          when N_Always
            | N_Never =>
             Child := Get_Property (Prop);
@@ -436,7 +443,7 @@ package body Sem_Psl is
    procedure Sem_Psl_Declaration (Stmt : Iir)
    is
       use Sem_Scopes;
-      Decl : Node;
+      Decl : constant Node := Get_Psl_Declaration (Stmt);
       Prop : Node;
       Clk : Node;
       Formal : Node;
@@ -445,8 +452,6 @@ package body Sem_Psl is
       Sem_Scopes.Add_Name (Stmt);
       Xref_Decl (Stmt);
 
-      Decl := Get_Psl_Declaration (Stmt);
-
       Open_Declarative_Region;
 
       --  Make formal parameters visible.
@@ -489,6 +494,33 @@ package body Sem_Psl is
       Close_Declarative_Region;
    end Sem_Psl_Declaration;
 
+   procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir)
+   is
+      use Sem_Scopes;
+      Decl : constant Node := Get_Psl_Declaration (Stmt);
+      Prop : Node;
+   begin
+      Sem_Scopes.Add_Name (Stmt);
+      Xref_Decl (Stmt);
+
+      pragma Assert (Get_Parameter_List (Decl) = Null_Node);
+      pragma Assert (Get_Kind (Decl) = N_Endpoint_Declaration);
+
+      Prop := Get_Sequence (Decl);
+      Prop := Sem_Sequence (Prop);
+      Sem_Psl_Directive_Clock (Stmt, Prop);
+      Set_Sequence (Decl, Prop);
+
+      PSL.Subsets.Check_Simple (Prop);
+
+      --  Endpoints are considered as an HDL declaration and must have a
+      --  type.
+      Set_Type (Stmt, Std_Package.Boolean_Type_Definition);
+      Set_Expr_Staticness (Stmt, None);
+
+      Set_Visible_Flag (Stmt, True);
+   end Sem_Psl_Endpoint_Declaration;
+
    function Rewrite_As_Boolean_Expression (Prop : Node) return Iir
    is
       function Rewrite_Dyadic_Operator
@@ -649,9 +681,9 @@ package body Sem_Psl is
 
    function Sem_Psl_Instance_Name (Name : Iir) return Iir
    is
-      Prefix : Iir;
-      Ent : Iir;
-      Decl : Node;
+      Prefix : constant Iir := Get_Prefix (Name);
+      Ent : constant Iir := Get_Named_Entity (Prefix);
+      Decl : constant Node := Get_Psl_Declaration (Ent);
       Formal : Node;
       Assoc : Iir;
       Res : Node;
@@ -661,10 +693,8 @@ package body Sem_Psl is
       Psl_Actual : Node;
       Res2 : Iir;
    begin
-      Prefix := Get_Prefix (Name);
-      Ent := Get_Named_Entity (Prefix);
-      pragma Assert (Get_Kind (Ent) = Iir_Kind_Psl_Declaration);
-      Decl := Get_Psl_Declaration (Ent);
+      pragma Assert (Get_Kind (Ent) = Iir_Kind_Psl_Declaration
+                       or Get_Kind (Ent) = Iir_Kind_Psl_Endpoint_Declaration);
       case Get_Kind (Decl) is
          when N_Property_Declaration =>
             Res := Create_Node (N_Property_Instance);
diff --git a/src/vhdl/sem_psl.ads b/src/vhdl/sem_psl.ads
index 482380303..6d2bf75ea 100644
--- a/src/vhdl/sem_psl.ads
+++ b/src/vhdl/sem_psl.ads
@@ -20,6 +20,7 @@ with Iirs; use Iirs;
 
 package Sem_Psl is
    procedure Sem_Psl_Declaration (Stmt : Iir);
+   procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir);
 
    --  May return a non-psl concurrent assertion statement.
    function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir;
diff --git a/src/vhdl/sem_stmts.adb b/src/vhdl/sem_stmts.adb
index 24d0f96e2..13fcc08d8 100644
--- a/src/vhdl/sem_stmts.adb
+++ b/src/vhdl/sem_stmts.adb
@@ -1913,6 +1913,8 @@ package body Sem_Stmts is
                  (El, Is_Passive);
             when Iir_Kind_Psl_Declaration =>
                Sem_Psl.Sem_Psl_Declaration (El);
+            when Iir_Kind_Psl_Endpoint_Declaration =>
+               Sem_Psl.Sem_Psl_Endpoint_Declaration (El);
             when Iir_Kind_Psl_Assert_Statement =>
                New_El := Sem_Psl.Sem_Psl_Assert_Statement (El);
             when Iir_Kind_Psl_Cover_Statement =>
@@ -1957,7 +1959,8 @@ package body Sem_Stmts is
       while Stmt /= Null_Iir loop
 
          case Get_Kind (Stmt) is
-            when Iir_Kind_Psl_Declaration =>
+            when Iir_Kind_Psl_Declaration
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                --  Special case for in-lined PSL declarations.
                null;
             when others =>
diff --git a/src/vhdl/translate/trans-chap7.adb b/src/vhdl/translate/trans-chap7.adb
index 2dfc6c57e..5c9fc35bc 100644
--- a/src/vhdl/translate/trans-chap7.adb
+++ b/src/vhdl/translate/trans-chap7.adb
@@ -4037,6 +4037,13 @@ package body Trans.Chap7 is
             | Iir_Kind_Selected_Name =>
             return Translate_Expression (Get_Named_Entity (Expr), Rtype);
 
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            declare
+               Info : constant Psl_Info_Acc := Get_Info (Expr);
+            begin
+               return New_Value (Get_Var (Info.Psl_Count_Var));
+            end;
+
          when others =>
             Error_Kind ("translate_expression", Expr);
       end case;
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index 395f3610a..8cfaf6a3c 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -315,8 +315,17 @@ package body Trans.Chap9 is
       New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type);
 
       --  Create the variables.
-      Info.Psl_Count_Var := Create_Var
-        (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type);
+      if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
+         --  FIXME: endpoint is a variable (and not a signal). This is required
+         --  to have the right value for the current cycle, but as a
+         --  consequence, this process must be evaluated before using the
+         --  endpoint.
+         Info.Psl_Count_Var := Create_Var
+           (Create_Var_Identifier ("ENDPOINT"), Std_Boolean_Type_Node);
+      else
+         Info.Psl_Count_Var := Create_Var
+           (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type);
+      end if;
 
       Info.Psl_Vect_Var := Create_Var
         (Create_Var_Identifier ("VECT"), Info.Psl_Vect_Type);
@@ -440,12 +449,18 @@ package body Trans.Chap9 is
       Start_Declare_Stmt;
       New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
       Init_Var (Var_I);
-      if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Statement then
-         New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
-                                               New_Obj_Value (Var_I)),
-                          New_Lit (Std_Boolean_True_Node));
-         Inc_Var (Var_I);
-      end if;
+      case Get_Kind (Stmt) is
+         when Iir_Kind_Psl_Cover_Statement
+           | Iir_Kind_Psl_Endpoint_Declaration =>
+            --  Sequences for cover or endpoints are detected on every cycle,
+            --  so the start state is always active.
+            New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
+                                                  New_Obj_Value (Var_I)),
+                             New_Lit (Std_Boolean_True_Node));
+            Inc_Var (Var_I);
+         when others =>
+            null;
+      end case;
       Start_Loop_Stmt (Label);
       Gen_Exit_When
         (Label,
@@ -512,28 +527,34 @@ package body Trans.Chap9 is
       S := Get_Final_State (NFA);
       S_Num := Get_State_Label (S);
       pragma Assert (S_Num = Get_PSL_Nbr_States (Stmt) - 1);
-      Start_If_Stmt
-        (S_Blk,
-         New_Value (New_Indexed_Element (New_Obj (Var_Nvec),
-                                         New_Lit (New_Index_Lit
-                                                    (Unsigned_64 (S_Num))))));
-      Open_Temp;
-      case Get_Kind (Stmt) is
-         when Iir_Kind_Psl_Assert_Statement =>
-            Chap8.Translate_Report
-              (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
-         when Iir_Kind_Psl_Cover_Statement =>
-            Chap8.Translate_Report
-              (Stmt, Ghdl_Psl_Cover, Severity_Level_Note);
-         when others =>
-            Error_Kind ("Translate_Psl_Directive_Statement", Stmt);
-      end case;
-      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var),
-                       New_Dyadic_Op (ON_Add_Ov,
-                                      New_Value (Get_Var (Info.Psl_Count_Var)),
-                                      New_Lit (Ghdl_Index_1)));
-      Close_Temp;
-      Finish_If_Stmt (S_Blk);
+      Cond := New_Value
+        (New_Indexed_Element (New_Obj (Var_Nvec),
+                              New_Lit (New_Index_Lit
+                                         (Unsigned_64 (S_Num)))));
+
+      if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
+         New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), Cond);
+      else
+         Start_If_Stmt (S_Blk, Cond);
+         Open_Temp;
+         case Get_Kind (Stmt) is
+            when Iir_Kind_Psl_Assert_Statement =>
+               Chap8.Translate_Report
+                 (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+            when Iir_Kind_Psl_Cover_Statement =>
+               Chap8.Translate_Report
+                 (Stmt, Ghdl_Psl_Cover, Severity_Level_Note);
+            when others =>
+               Error_Kind ("Translate_Psl_Directive_Statement", Stmt);
+         end case;
+         New_Assign_Stmt
+           (Get_Var (Info.Psl_Count_Var),
+            New_Dyadic_Op (ON_Add_Ov,
+                           New_Value (Get_Var (Info.Psl_Count_Var)),
+                           New_Lit (Ghdl_Index_1)));
+         Close_Temp;
+         Finish_If_Stmt (S_Blk);
+      end if;
 
       --  Assign state vector.
       Start_Declare_Stmt;
@@ -633,6 +654,9 @@ package body Trans.Chap9 is
             Pop_Local_Factory;
             Finish_Subprogram_Body;
 
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            Info.Psl_Proc_Final_Subprg := O_Dnode_Null;
+
          when others =>
             Error_Kind ("Translate_Psl_Directive_Statement(3)", Stmt);
       end case;
@@ -800,7 +824,8 @@ package body Trans.Chap9 is
             when Iir_Kind_Psl_Declaration =>
                null;
             when Iir_Kind_Psl_Assert_Statement
-               | Iir_Kind_Psl_Cover_Statement =>
+              | Iir_Kind_Psl_Cover_Statement
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                Translate_Psl_Directive_Declarations (El);
             when Iir_Kind_Component_Instantiation_Statement =>
                Translate_Component_Instantiation_Statement (El);
@@ -942,7 +967,8 @@ package body Trans.Chap9 is
             when Iir_Kind_Psl_Declaration =>
                null;
             when Iir_Kind_Psl_Assert_Statement
-               | Iir_Kind_Psl_Cover_Statement =>
+              | Iir_Kind_Psl_Cover_Statement
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                Translate_Psl_Directive_Statement (Stmt, Base_Info);
             when Iir_Kind_Component_Instantiation_Statement =>
                Chap4.Translate_Association_Subprograms
@@ -1334,6 +1360,7 @@ package body Trans.Chap9 is
       List   : Iir_List;
       Var_I  : O_Dnode;
       Label  : O_Snode;
+      Init   : O_Cnode;
    begin
       New_Debug_Line_Stmt (Get_Line_Number (Stmt));
 
@@ -1391,7 +1418,12 @@ package body Trans.Chap9 is
       Finish_Loop_Stmt (Label);
       Finish_Declare_Stmt;
 
-      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Ghdl_Index_0));
+      if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
+         Init := Std_Boolean_False_Node;
+      else
+         Init := Ghdl_Index_0;
+      end if;
+      New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Init));
    end Elab_Psl_Directive;
 
    procedure Elab_Implicit_Guard_Signal
@@ -2197,7 +2229,8 @@ package body Trans.Chap9 is
                null;
             when Iir_Kind_Psl_Default_Clock =>
                null;
-            when Iir_Kind_Psl_Declaration =>
+            when Iir_Kind_Psl_Declaration
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                null;
             when Iir_Kind_Psl_Assert_Statement
                | Iir_Kind_Psl_Cover_Statement =>
@@ -2260,7 +2293,8 @@ package body Trans.Chap9 is
             when Iir_Kind_Psl_Declaration =>
                null;
             when Iir_Kind_Psl_Assert_Statement
-              | Iir_Kind_Psl_Cover_Statement =>
+              | Iir_Kind_Psl_Cover_Statement
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                Elab_Psl_Directive (Stmt, Base_Info);
             when Iir_Kind_Component_Instantiation_Statement =>
                null;
diff --git a/src/vhdl/translate/trans-rtis.adb b/src/vhdl/translate/trans-rtis.adb
index ef26d17f3..8dd86b282 100644
--- a/src/vhdl/translate/trans-rtis.adb
+++ b/src/vhdl/translate/trans-rtis.adb
@@ -312,6 +312,9 @@ package body Trans.Rtis is
          New_Enum_Literal
            (Constr, Get_Identifier ("__ghdl_rtik_psl_cover"),
             Ghdl_Rtik_Psl_Cover);
+         New_Enum_Literal
+           (Constr, Get_Identifier ("__ghdl_rtik_psl_endpoint"),
+            Ghdl_Rtik_Psl_Endpoint);
 
          New_Enum_Literal (Constr, Get_Identifier ("__ghdl_rtik_error"),
                            Ghdl_Rtik_Error);
@@ -2008,6 +2011,8 @@ package body Trans.Rtis is
             Kind := Ghdl_Rtik_Psl_Cover;
          when Iir_Kind_Psl_Assert_Statement =>
             Kind := Ghdl_Rtik_Psl_Assert;
+         when Iir_Kind_Psl_Endpoint_Declaration =>
+            Kind := Ghdl_Rtik_Psl_Endpoint;
          when others =>
             Error_Kind ("rti.generate_psl_directive", Decl);
       end case;
@@ -2335,7 +2340,8 @@ package body Trans.Rtis is
             when Iir_Kind_Psl_Declaration =>
                null;
             when Iir_Kind_Psl_Assert_Statement
-              | Iir_Kind_Psl_Cover_Statement =>
+              | Iir_Kind_Psl_Cover_Statement
+              | Iir_Kind_Psl_Endpoint_Declaration =>
                Generate_Psl_Directive (Stmt);
             when others =>
                Error_Kind ("rti.generate_concurrent_statement_chain", Stmt);
@@ -2860,7 +2866,8 @@ package body Trans.Rtis is
             | Iir_Kind_Sensitized_Process_Statement =>
             Rti_Const := Node_Info.Process_Rti_Const;
          when Iir_Kind_Psl_Assert_Statement
-            | Iir_Kind_Psl_Cover_Statement =>
+           | Iir_Kind_Psl_Cover_Statement
+           | Iir_Kind_Psl_Endpoint_Declaration =>
             Rti_Const := Node_Info.Psl_Rti_Const;
          when others =>
             Error_Kind ("get_context_rti", Node);
@@ -2896,7 +2903,8 @@ package body Trans.Rtis is
             | Iir_Kind_Sensitized_Process_Statement =>
             Ref := Get_Instance_Ref (Node_Info.Process_Scope);
          when Iir_Kind_Psl_Assert_Statement
-            | Iir_Kind_Psl_Cover_Statement =>
+           | Iir_Kind_Psl_Cover_Statement
+           | Iir_Kind_Psl_Endpoint_Declaration =>
             Ref := Get_Instance_Ref (Node_Info.Psl_Scope);
          when others =>
             Error_Kind ("get_context_addr", Node);
diff --git a/src/vhdl/translate/trans-rtis.ads b/src/vhdl/translate/trans-rtis.ads
index c272bf7e9..a1b5b456b 100644
--- a/src/vhdl/translate/trans-rtis.ads
+++ b/src/vhdl/translate/trans-rtis.ads
@@ -68,6 +68,7 @@ package Trans.Rtis is
    Ghdl_Rtik_Attribute_Stable            : O_Cnode;
    Ghdl_Rtik_Psl_Assert                  : O_Cnode;
    Ghdl_Rtik_Psl_Cover                   : O_Cnode;
+   Ghdl_Rtik_Psl_Endpoint                : O_Cnode;
    Ghdl_Rtik_Error                       : O_Cnode;
 
    --  RTI types.