psl: cover directive works on a sequence, not on a property.

20 files changed, 307 insertions, 86 deletions

diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb
index 661d758bf..7a047b6de 100644
--- a/src/psl/psl-build.adb
+++ b/src/psl/psl-build.adb
@@ -29,8 +29,6 @@ with PSL.Prints;
 with PSL.NFAs; use PSL.NFAs;
 
 package body PSL.Build is
-   function Build_SERE_FA (N : Node) return NFA;
-
    package Intersection is
       function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA;
    end Intersection;
diff --git a/src/psl/psl-build.ads b/src/psl/psl-build.ads
index c8e15ee22..dcfadb96a 100644
--- a/src/psl/psl-build.ads
+++ b/src/psl/psl-build.ads
@@ -21,5 +21,6 @@ with PSL.Nodes; use PSL.Nodes;
 package PSL.Build is
    Optimize_Final : Boolean := True;
 
+   function Build_SERE_FA (N : Node) return NFA;
    function Build_FA (N : Node) return NFA;
 end PSL.Build;
diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb
index 19d7c3959..dd0755570 100644
--- a/src/psl/psl-prints.adb
+++ b/src/psl/psl-prints.adb
@@ -67,7 +67,9 @@ package body PSL.Prints is
            | N_True
            | N_False
            | N_EOS
-           | N_HDL_Expr =>
+           | N_HDL_Expr
+           | N_Property_Instance
+           | N_Sequence_Instance =>
             return Prio_HDL;
          when N_Or_Bool =>
             return Prio_Seq_Or;
@@ -184,8 +186,6 @@ package body PSL.Prints is
       end if;
    end Print_Expr;
 
-   procedure Print_Sequence (Seq : Node; Parent_Prio : Priority);
-
    procedure Print_Count (N : Node) is
       B : Node;
    begin
@@ -222,7 +222,7 @@ package body PSL.Prints is
       Put ("]");
    end Print_Repeat_Sequence;
 
-   procedure Print_Sequence (Seq : Node; Parent_Prio : Priority)
+   procedure Print_Sequence (Seq : Node; Parent_Prio : Priority := Prio_Lowest)
    is
       Prio : constant Priority := Get_Priority (Seq);
       Add_Paren : constant Boolean := Prio < Parent_Prio
@@ -260,6 +260,8 @@ package body PSL.Prints is
          when N_Booleans
            | N_Name_Decl =>
             Print_Expr (Seq);
+         when N_Sequence_Instance =>
+            Put (Image (Get_Identifier (Get_Declaration (Seq))));
          when others =>
             Error_Kind ("print_sequence", Seq);
       end case;
@@ -387,6 +389,10 @@ package body PSL.Prints is
             Print_Expr (Prop);
          when N_Sequences =>
             Print_Sequence (Prop, Parent_Prio);
+         when N_Property_Instance =>
+            Put (Image (Get_Identifier (Get_Declaration (Prop))));
+         when N_EOS =>
+            Put ("EOS");
          when others =>
             Error_Kind ("print_property", Prop);
       end case;
diff --git a/src/psl/psl-prints.ads b/src/psl/psl-prints.ads
index 920ca5939..d49a5e093 100644
--- a/src/psl/psl-prints.ads
+++ b/src/psl/psl-prints.ads
@@ -21,8 +21,10 @@ with PSL.Priorities; use PSL.Priorities;
 
 package PSL.Prints is
    procedure Print_Unit (Unit : Node);
-   procedure Print_Property (Prop : Node;
-                             Parent_Prio : Priority := Prio_Lowest);
+   procedure Print_Sequence
+     (Seq : Node; Parent_Prio : Priority := Prio_Lowest);
+   procedure Print_Property
+     (Prop : Node; Parent_Prio : Priority := Prio_Lowest);
    procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest);
 
    --  Procedure to display HDL_Expr nodes.
diff --git a/src/vhdl/canon.adb b/src/vhdl/canon.adb
index c498ba55c..bf4536088 100644
--- a/src/vhdl/canon.adb
+++ b/src/vhdl/canon.adb
@@ -1636,6 +1636,31 @@ package body Canon is
       return False;
    end Psl_Need_Finalizer;
 
+   procedure Canon_Psl_Directive (Stmt : Iir)
+   is
+      use PSL.Nodes;
+      Fa : PSL_NFA;
+      Num : Natural;
+      List : Iir_List;
+   begin
+      Fa := Get_PSL_NFA (Stmt);
+
+      PSL.NFAs.Labelize_States (Fa, Num);
+      Set_PSL_Nbr_States (Stmt, Int32 (Num));
+
+      Set_PSL_EOS_Flag (Stmt, Psl_Need_Finalizer (Fa));
+
+      List := Create_Iir_List;
+      Canon_PSL.Canon_Extract_Sensitivity (Get_PSL_Clock (Stmt), List);
+      Set_PSL_Clock_Sensitivity (Stmt, List);
+
+      if Canon_Flag_Expressions then
+         Canon_PSL_Expression (Get_PSL_Clock (Stmt));
+         Canon_Expression (Get_Severity_Expression (Stmt));
+         Canon_Expression (Get_Report_Expression (Stmt));
+      end if;
+   end Canon_Psl_Directive;
+
    procedure Canon_Concurrent_Stmts (Top : Iir_Design_Unit; Parent : Iir)
    is
       --  Current element in the chain of concurrent statements.
@@ -1897,37 +1922,38 @@ package body Canon is
                Canon_Generate_Statement_Body
                  (Top, Get_Generate_Statement_Body (El));
 
-            when Iir_Kind_Psl_Assert_Statement
-              | Iir_Kind_Psl_Cover_Statement =>
+            when Iir_Kind_Psl_Assert_Statement =>
                declare
                   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);
                   Set_Psl_Property (El, Prop);
+
                   --  Generate the NFA.
                   Fa := PSL.Build.Build_FA (Prop);
                   Set_PSL_NFA (El, Fa);
 
-                  PSL.NFAs.Labelize_States (Fa, Num);
-                  Set_PSL_Nbr_States (El, Int32 (Num));
+                  Canon_Psl_Directive (El);
+               end;
 
-                  Set_PSL_EOS_Flag (El, Psl_Need_Finalizer (Fa));
+            when Iir_Kind_Psl_Cover_Statement =>
+               declare
+                  use PSL.Nodes;
+                  Seq : PSL_Node;
+                  Fa : PSL_NFA;
+               begin
+                  Seq := Get_Psl_Sequence (El);
+                  Seq := PSL.Rewrites.Rewrite_SERE (Seq);
+                  Set_Psl_Sequence (El, Seq);
 
-                  List := Create_Iir_List;
-                  Canon_PSL.Canon_Extract_Sensitivity
-                    (Get_PSL_Clock (El), List);
-                  Set_PSL_Clock_Sensitivity (El, List);
+                  --  Generate the NFA.
+                  Fa := PSL.Build.Build_SERE_FA (Seq);
+                  Set_PSL_NFA (El, Fa);
 
-                  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;
+                  Canon_Psl_Directive (El);
                end;
 
             when Iir_Kind_Psl_Default_Clock =>
diff --git a/src/vhdl/disp_vhdl.adb b/src/vhdl/disp_vhdl.adb
index 9872ff802..4cccdf576 100644
--- a/src/vhdl/disp_vhdl.adb
+++ b/src/vhdl/disp_vhdl.adb
@@ -2835,6 +2835,12 @@ package body Disp_Vhdl is
       PSL.Prints.Print_Property (Expr);
    end Disp_Psl_Expression;
 
+   procedure Disp_Psl_Sequence (Expr : PSL_Node) is
+   begin
+      PSL.Prints.HDL_Expr_Printer := Disp_PSL_HDL_Expr'Access;
+      PSL.Prints.Print_Sequence (Expr);
+   end Disp_Psl_Sequence;
+
    procedure Disp_Block_Header (Header : Iir_Block_Header; Indent: Count)
    is
       Chain : Iir;
@@ -2979,6 +2985,29 @@ package body Disp_Vhdl is
       Put_Line (";");
    end Disp_Psl_Default_Clock;
 
+   procedure Disp_Psl_Declaration (Stmt : Iir)
+   is
+      use PSL.Nodes;
+      Decl : constant PSL_Node := Get_Psl_Declaration (Stmt);
+   begin
+      Put ("--psl ");
+      case Get_Kind (Decl) is
+         when N_Property_Declaration =>
+            Put ("property ");
+            Disp_Ident (Get_Identifier (Decl));
+            Put (" is ");
+            Disp_Psl_Expression (Get_Property (Decl));
+         when N_Sequence_Declaration =>
+            Put ("sequence ");
+            Disp_Ident (Get_Identifier (Decl));
+            Put (" is ");
+            Disp_Psl_Sequence (Get_Sequence (Decl));
+         when others =>
+            Error_Kind ("disp_psl_declaration", Decl);
+      end case;
+      Put_Line (";");
+   end Disp_Psl_Declaration;
+
    procedure Disp_PSL_NFA (N : PSL.Nodes.NFA)
    is
       use PSL.NFAs;
@@ -2994,6 +3023,12 @@ package body Disp_Vhdl is
       E : NFA_Edge;
    begin
       if N /= No_NFA then
+         Put ("-- start: ");
+         Disp_State (Get_Start_State (N));
+         Put (", final: ");
+         Disp_State (Get_Final_State (N));
+         New_Line;
+
          S := Get_First_State (N);
          while S /= No_State loop
             E := Get_First_Src_Edge (S);
@@ -3027,7 +3062,7 @@ package body Disp_Vhdl is
       Put ("--psl ");
       Disp_Label (Stmt);
       Put ("cover ");
-      Disp_Psl_Expression (Get_Psl_Property (Stmt));
+      Disp_Psl_Sequence (Get_Psl_Sequence (Stmt));
       Put_Line (";");
       Disp_PSL_NFA (Get_PSL_NFA (Stmt));
    end Disp_Psl_Cover_Statement;
@@ -3070,6 +3105,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 =>
+            Disp_Psl_Declaration (Stmt);
          when Iir_Kind_Psl_Assert_Statement =>
             Disp_Psl_Assert_Statement (Stmt);
          when Iir_Kind_Psl_Cover_Statement =>
@@ -3340,6 +3377,8 @@ package body Disp_Vhdl is
            | Iir_Kind_Indexed_Name
            | Iir_Kind_Slice_Name =>
             Disp_Expression (An_Iir);
+         when Iir_Kind_Psl_Cover_Statement =>
+            Disp_Psl_Cover_Statement (An_Iir);
          when others =>
             Error_Kind ("disp", An_Iir);
       end case;
diff --git a/src/vhdl/disp_vhdl.ads b/src/vhdl/disp_vhdl.ads
index 880290efd..9f04129bc 100644
--- a/src/vhdl/disp_vhdl.ads
+++ b/src/vhdl/disp_vhdl.ads
@@ -24,6 +24,8 @@ package Disp_Vhdl is
    -- the node.
    procedure Disp_Vhdl (An_Iir: Iir);
 
+   procedure Disp_PSL_NFA (N : PSL_NFA);
+
    procedure Disp_Expression (Expr: Iir);
    --  Display an expression.
 
diff --git a/src/vhdl/iirs.adb b/src/vhdl/iirs.adb
index 00614233c..3b9f32b86 100644
--- a/src/vhdl/iirs.adb
+++ b/src/vhdl/iirs.adb
@@ -5229,6 +5229,22 @@ package body Iirs is
       Set_Field1 (Decl, PSL_Node_To_Iir (Prop));
    end Set_Psl_Property;
 
+   function Get_Psl_Sequence (Decl : Iir) return PSL_Node is
+   begin
+      pragma Assert (Decl /= Null_Iir);
+      pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)),
+                     "no field Psl_Sequence");
+      return Iir_To_PSL_Node (Get_Field1 (Decl));
+   end Get_Psl_Sequence;
+
+   procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node) is
+   begin
+      pragma Assert (Decl /= Null_Iir);
+      pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)),
+                     "no field Psl_Sequence");
+      Set_Field1 (Decl, PSL_Node_To_Iir (Prop));
+   end Set_Psl_Sequence;
+
    function Get_Psl_Declaration (Decl : Iir) return PSL_Node is
    begin
       pragma Assert (Decl /= Null_Iir);
diff --git a/src/vhdl/iirs.ads b/src/vhdl/iirs.ads
index 1272e7723..a1fe93ced 100644
--- a/src/vhdl/iirs.ads
+++ b/src/vhdl/iirs.ads
@@ -2506,8 +2506,12 @@ package Iirs is
    --
    --   Get/Set_Parent (Field0)
    --
+   -- Only for Iir_Kind_Psl_Assert_Statement:
    --   Get/Set_Psl_Property (Field1)
    --
+   -- Only for Iir_Kind_Psl_Cover_Statement:
+   --   Get/Set_Psl_Sequence (Field1)
+   --
    --   Get/Set_Chain (Field2)
    --
    --   Get/Set_Label (Field3)
@@ -6646,6 +6650,10 @@ package Iirs is
    procedure Set_Psl_Property (Decl : Iir; Prop : PSL_Node);
 
    --  Field: Field1 (uc)
+   function Get_Psl_Sequence (Decl : Iir) return PSL_Node;
+   procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node);
+
+   --  Field: Field1 (uc)
    function Get_Psl_Declaration (Decl : Iir) return PSL_Node;
    procedure Set_Psl_Declaration (Decl : Iir; Prop : PSL_Node);
 
diff --git a/src/vhdl/nodes_meta.adb b/src/vhdl/nodes_meta.adb
index d5a3c62a0..b868751f5 100644
--- a/src/vhdl/nodes_meta.adb
+++ b/src/vhdl/nodes_meta.adb
@@ -312,6 +312,7 @@ package body Nodes_Meta is
       Field_Suspend_Flag => Type_Boolean,
       Field_Is_Ref => Type_Boolean,
       Field_Psl_Property => Type_PSL_Node,
+      Field_Psl_Sequence => Type_PSL_Node,
       Field_Psl_Declaration => Type_PSL_Node,
       Field_Psl_Expression => Type_PSL_Node,
       Field_Psl_Boolean => Type_PSL_Node,
@@ -916,6 +917,8 @@ package body Nodes_Meta is
             return "is_ref";
          when Field_Psl_Property =>
             return "psl_property";
+         when Field_Psl_Sequence =>
+            return "psl_sequence";
          when Field_Psl_Declaration =>
             return "psl_declaration";
          when Field_Psl_Expression =>
@@ -2038,6 +2041,8 @@ package body Nodes_Meta is
             return Attr_None;
          when Field_Psl_Property =>
             return Attr_None;
+         when Field_Psl_Sequence =>
+            return Attr_None;
          when Field_Psl_Declaration =>
             return Attr_None;
          when Field_Psl_Expression =>
@@ -3473,7 +3478,7 @@ package body Nodes_Meta is
       Field_Report_Expression,
       Field_Parent,
       --  Iir_Kind_Psl_Cover_Statement
-      Field_Psl_Property,
+      Field_Psl_Sequence,
       Field_Label,
       Field_PSL_Clock,
       Field_PSL_NFA,
@@ -5960,6 +5965,8 @@ package body Nodes_Meta is
       case F is
          when Field_Psl_Property =>
             return Get_Psl_Property (N);
+         when Field_Psl_Sequence =>
+            return Get_Psl_Sequence (N);
          when Field_Psl_Declaration =>
             return Get_Psl_Declaration (N);
          when Field_Psl_Expression =>
@@ -5980,6 +5987,8 @@ package body Nodes_Meta is
       case F is
          when Field_Psl_Property =>
             Set_Psl_Property (N, V);
+         when Field_Psl_Sequence =>
+            Set_Psl_Sequence (N, V);
          when Field_Psl_Declaration =>
             Set_Psl_Declaration (N, V);
          when Field_Psl_Expression =>
@@ -9762,15 +9771,14 @@ package body Nodes_Meta is
 
    function Has_Psl_Property (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;
+      return K = Iir_Kind_Psl_Assert_Statement;
    end Has_Psl_Property;
 
+   function Has_Psl_Sequence (K : Iir_Kind) return Boolean is
+   begin
+      return K = Iir_Kind_Psl_Cover_Statement;
+   end Has_Psl_Sequence;
+
    function Has_Psl_Declaration (K : Iir_Kind) return Boolean is
    begin
       return K = Iir_Kind_Psl_Declaration;
diff --git a/src/vhdl/nodes_meta.ads b/src/vhdl/nodes_meta.ads
index d4ae3a060..19b5930a6 100644
--- a/src/vhdl/nodes_meta.ads
+++ b/src/vhdl/nodes_meta.ads
@@ -352,6 +352,7 @@ package Nodes_Meta is
       Field_Suspend_Flag,
       Field_Is_Ref,
       Field_Psl_Property,
+      Field_Psl_Sequence,
       Field_Psl_Declaration,
       Field_Psl_Expression,
       Field_Psl_Boolean,
@@ -842,6 +843,7 @@ package Nodes_Meta is
    function Has_Suspend_Flag (K : Iir_Kind) return Boolean;
    function Has_Is_Ref (K : Iir_Kind) return Boolean;
    function Has_Psl_Property (K : Iir_Kind) return Boolean;
+   function Has_Psl_Sequence (K : Iir_Kind) return Boolean;
    function Has_Psl_Declaration (K : Iir_Kind) return Boolean;
    function Has_Psl_Expression (K : Iir_Kind) return Boolean;
    function Has_Psl_Boolean (K : Iir_Kind) return Boolean;
diff --git a/src/vhdl/parse.adb b/src/vhdl/parse.adb
index ccbf98617..012a54264 100644
--- a/src/vhdl/parse.adb
+++ b/src/vhdl/parse.adb
@@ -6917,18 +6917,31 @@ package body Parse is
       return Res;
    end Parse_Psl_Declaration;
 
+   --  Parse end of PSL assert/cover statement.
+   procedure Parse_Psl_Assert_Report_Severity (Stmt : Iir) is
+   begin
+      if Current_Token = Tok_Report then
+         --  Skip 'report'
+         Scan;
+
+         Set_Report_Expression (Stmt, Parse_Expression);
+      end if;
+
+      if Current_Token = Tok_Severity then
+         --  Skip 'severity'
+         Scan;
+
+         Set_Severity_Expression (Stmt, Parse_Expression);
+      end if;
+
+      Expect (Tok_Semi_Colon);
+   end Parse_Psl_Assert_Report_Severity;
+
    function Parse_Psl_Assert_Statement return Iir
    is
       Res : Iir;
    begin
-      case Current_Token is
-         when Tok_Assert =>
-            Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
-         when Tok_Psl_Cover =>
-            Res := Create_Iir (Iir_Kind_Psl_Cover_Statement);
-         when others =>
-            raise Internal_Error;
-      end case;
+      Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
 
       --  Skip 'assert'
       Scan;
@@ -6938,24 +6951,31 @@ package body Parse is
       --  No more PSL tokens after the property.
       Scanner.Flag_Psl := False;
 
-      if Current_Token = Tok_Report then
-         --  Skip 'report'
-         Scan;
+      Parse_Psl_Assert_Report_Severity (Res);
 
-         Set_Report_Expression (Res, Parse_Expression);
-      end if;
+      Scanner.Flag_Scan_In_Comment := False;
+      return Res;
+   end Parse_Psl_Assert_Statement;
 
-      if Current_Token = Tok_Severity then
-         --  Skip 'severity'
-         Scan;
+   function Parse_Psl_Cover_Statement return Iir
+   is
+      Res : Iir;
+   begin
+      Res := Create_Iir (Iir_Kind_Psl_Cover_Statement);
 
-         Set_Severity_Expression (Res, Parse_Expression);
-      end if;
+      --  Skip 'cover'
+      Scan;
+
+      Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence);
+
+      --  No more PSL tokens after the property.
+      Scanner.Flag_Psl := False;
+
+      Parse_Psl_Assert_Report_Severity (Res);
 
-      Expect (Tok_Semi_Colon);
       Scanner.Flag_Scan_In_Comment := False;
       return Res;
-   end Parse_Psl_Assert_Statement;
+   end Parse_Psl_Cover_Statement;
 
    procedure Parse_Concurrent_Statements (Parent : Iir)
    is
@@ -7103,7 +7123,7 @@ package body Parse is
                Stmt := Parse_Psl_Declaration;
             when Tok_Psl_Cover =>
                Postponed_Not_Allowed;
-               Stmt := Parse_Psl_Assert_Statement;
+               Stmt := Parse_Psl_Cover_Statement;
             when others =>
                --  FIXME: improve message:
                --  instead of 'unexpected token 'signal' in conc stmt list'
diff --git a/src/vhdl/parse_psl.adb b/src/vhdl/parse_psl.adb
index 506218ade..a356043aa 100644
--- a/src/vhdl/parse_psl.adb
+++ b/src/vhdl/parse_psl.adb
@@ -77,17 +77,18 @@ package body Parse_Psl is
 
    function Vhdl_To_Psl (N : Iirs.Iir) return Node
    is
+      use Iirs;
       Res : Node;
    begin
       Res := Create_Node_Loc (N_HDL_Expr);
-      Set_Location (Res, Iirs.Get_Location (N));
-      Set_HDL_Node (Res, Int32 (N));
+      if N /= Null_Iir then
+         Set_Location (Res, Get_Location (N));
+         Set_HDL_Node (Res, Int32 (N));
+      end if;
       return Res;
    end Vhdl_To_Psl;
 
    function Parse_FL_Property (Prio : Priority) return Node;
-   function Parse_Sequence return Node;
-
    function Parse_Parenthesis_Boolean return Node;
    function Parse_Boolean (Parent_Prio : Priority) return Node;
 
@@ -161,7 +162,7 @@ package body Parse_Psl is
       Kind : Nkind;
       Op_Prio : Priority;
    begin
-      Left := Parse_Sequence; --  FIXME: allow boolean;
+      Left := Parse_Psl_Sequence; --  FIXME: allow boolean;
       loop
          case Current_Token is
             when Tok_Semi_Colon =>
@@ -282,7 +283,7 @@ package body Parse_Psl is
       end if;
    end Parse_Bracket_Number;
 
-   function Parse_Sequence return Node is
+   function Parse_Psl_Sequence return Node is
       Res, N : Node;
    begin
       case Current_Token is
@@ -331,7 +332,7 @@ package body Parse_Psl is
                return Res;
          end case;
       end loop;
-   end Parse_Sequence;
+   end Parse_Psl_Sequence;
 
    --  precond:  '('
    --  postcond: next token
@@ -430,7 +431,7 @@ package body Parse_Psl is
          when Tok_Left_Paren =>
             return Parse_Parenthesis_FL_Property;
          when Tok_Left_Curly =>
-            Res := Parse_Sequence;
+            Res := Parse_Psl_Sequence;
             if Get_Kind (Res) = N_Braced_SERE
               and then Current_Token = Tok_Left_Paren
             then
@@ -442,7 +443,7 @@ package body Parse_Psl is
                Res := Tmp;
             end if;
          when others =>
-            Res := Parse_Sequence;
+            Res := Parse_Psl_Sequence;
       end case;
       return Res;
    end Parse_FL_Property_1;
@@ -663,7 +664,7 @@ package body Parse_Psl is
             Set_Property (Res, Parse_Psl_Property);
          when N_Sequence_Declaration
            | N_Endpoint_Declaration =>
-            Set_Sequence (Res, Parse_Sequence);
+            Set_Sequence (Res, Parse_Psl_Sequence);
          when others =>
             raise Internal_Error;
       end case;
diff --git a/src/vhdl/parse_psl.ads b/src/vhdl/parse_psl.ads
index 62869feb8..160df668e 100644
--- a/src/vhdl/parse_psl.ads
+++ b/src/vhdl/parse_psl.ads
@@ -20,6 +20,7 @@ with Types; use Types;
 with Tokens; use Tokens;
 
 package Parse_Psl is
+   function Parse_Psl_Sequence return PSL_Node;
    function Parse_Psl_Property return PSL_Node;
    function Parse_Psl_Boolean return PSL_Node;
    function Parse_Psl_Declaration (Tok : Token_Type) return PSL_Node;
diff --git a/src/vhdl/sem_psl.adb b/src/vhdl/sem_psl.adb
index 503842ce1..98e258359 100644
--- a/src/vhdl/sem_psl.adb
+++ b/src/vhdl/sem_psl.adb
@@ -150,11 +150,7 @@ package body Sem_Psl is
          Expr := Finish_Sem_Name (Expr);
          Set_HDL_Node (N, Expr);
 
-         if Get_Kind (Expr) in Iir_Kinds_Denoting_Name then
-            Name := Get_Named_Entity (Expr);
-         else
-            Name := Expr;
-         end if;
+         Name := Strip_Denoting_Name (Expr);
 
          case Get_Kind (Name) is
             when Iir_Kind_Error =>
@@ -290,7 +286,20 @@ package body Sem_Psl is
            | N_Not_Bool =>
             return Sem_Boolean (Seq);
          when N_HDL_Expr =>
-            return Sem_Hdl_Expr (Seq);
+            Res := Sem_Hdl_Expr (Seq);
+            case Get_Kind (Res) is
+               when N_Sequence_Instance
+                 | N_Endpoint_Instance
+                 | N_Boolean_Parameter
+                 | N_Booleans =>
+                  null;
+               when N_Property_Instance =>
+                  Error_Msg_Sem
+                    ("property instance not allowed in PSL sequence", Res);
+               when others =>
+                  Error_Kind ("psl.sem_sequence.hdl", Res);
+            end case;
+            return Res;
          when others =>
             Error_Kind ("psl.sem_sequence", Seq);
       end case;
@@ -553,14 +562,30 @@ package body Sem_Psl is
       end case;
    end Is_Boolean_Assertion;
 
+   procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out Node)
+   is
+      Clk : Node;
+   begin
+      Extract_Clock (Prop, Clk);
+      if Clk = Null_Node then
+         if Current_Psl_Default_Clock = Null_Iir then
+            Error_Msg_Sem ("no clock for PSL directive", Stmt);
+            Clk := Null_Node;
+         else
+            Clk := Get_Psl_Boolean (Current_Psl_Default_Clock);
+         end if;
+      end if;
+      Set_PSL_Clock (Stmt, Clk);
+   end Sem_Psl_Directive_Clock;
+
    function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir
    is
       Prop : Node;
-      Clk : Node;
       Res : Iir;
    begin
       --  Sem report and severity expressions.
       Sem_Report_Statement (Stmt);
+
       Prop := Get_Psl_Property (Stmt);
       Prop := Sem_Property (Prop, True);
       Set_Psl_Property (Stmt, Prop);
@@ -576,16 +601,7 @@ package body Sem_Psl is
       end if;
 
       --  Properties must be clocked.
-      Extract_Clock (Prop, Clk);
-      if Clk = Null_Node then
-         if Current_Psl_Default_Clock = Null_Iir then
-            Error_Msg_Sem ("no clock for PSL assert", Stmt);
-            Clk := Null_Node;
-         else
-            Clk := Get_Psl_Boolean (Current_Psl_Default_Clock);
-         end if;
-      end if;
-      Set_PSL_Clock (Stmt, Clk);
+      Sem_Psl_Directive_Clock (Stmt, Prop);
       Set_Psl_Property (Stmt, Prop);
 
       --  Check simple subset restrictions.
@@ -594,6 +610,24 @@ package body Sem_Psl is
       return Stmt;
    end Sem_Psl_Assert_Statement;
 
+   procedure Sem_Psl_Cover_Statement (Stmt : Iir)
+   is
+      Seq : Node;
+   begin
+      --  Sem report and severity expressions.
+      Sem_Report_Statement (Stmt);
+
+      Seq := Get_Psl_Sequence (Stmt);
+      Seq := Sem_Sequence (Seq);
+
+      --  Properties must be clocked.
+      Sem_Psl_Directive_Clock (Stmt, Seq);
+      Set_Psl_Sequence (Stmt, Seq);
+
+      --  Check simple subset restrictions.
+      PSL.Subsets.Check_Simple (Seq);
+   end Sem_Psl_Cover_Statement;
+
    procedure Sem_Psl_Default_Clock (Stmt : Iir)
    is
       Expr : Node;
diff --git a/src/vhdl/sem_psl.ads b/src/vhdl/sem_psl.ads
index 25663a244..482380303 100644
--- a/src/vhdl/sem_psl.ads
+++ b/src/vhdl/sem_psl.ads
@@ -20,7 +20,11 @@ with Iirs; use Iirs;
 
 package Sem_Psl is
    procedure Sem_Psl_Declaration (Stmt : Iir);
+
+   --  May return a non-psl concurrent assertion statement.
    function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir;
+
+   procedure Sem_Psl_Cover_Statement (Stmt : Iir);
    procedure Sem_Psl_Default_Clock (Stmt : Iir);
    function Sem_Psl_Name (Name : Iir) return Iir;
 end Sem_Psl;
diff --git a/src/vhdl/sem_stmts.adb b/src/vhdl/sem_stmts.adb
index 5e04cb494..24d0f96e2 100644
--- a/src/vhdl/sem_stmts.adb
+++ b/src/vhdl/sem_stmts.adb
@@ -1913,9 +1913,10 @@ package body Sem_Stmts is
                  (El, Is_Passive);
             when Iir_Kind_Psl_Declaration =>
                Sem_Psl.Sem_Psl_Declaration (El);
-            when Iir_Kind_Psl_Assert_Statement
-              | Iir_Kind_Psl_Cover_Statement =>
+            when Iir_Kind_Psl_Assert_Statement =>
                New_El := Sem_Psl.Sem_Psl_Assert_Statement (El);
+            when Iir_Kind_Psl_Cover_Statement =>
+               Sem_Psl.Sem_Psl_Cover_Statement (El);
             when Iir_Kind_Psl_Default_Clock =>
                Sem_Psl.Sem_Psl_Default_Clock (El);
             when Iir_Kind_Simple_Simultaneous_Statement =>
diff --git a/src/vhdl/simulate/debugger.adb b/src/vhdl/simulate/debugger.adb
index bbb16e231..47846394a 100644
--- a/src/vhdl/simulate/debugger.adb
+++ b/src/vhdl/simulate/debugger.adb
@@ -1298,6 +1298,42 @@ package body Debugger is
       return Walk_Continue;
    end Cb_Disp_File;
 
+   procedure Info_PSL_Proc (Line : String)
+   is
+      pragma Unreferenced (Line);
+   begin
+      if PSL_Table.Last < PSL_Table.First then
+         Put_Line ("no PSL directive");
+         return;
+      end if;
+
+      for I in PSL_Table.First .. PSL_Table.Last loop
+         declare
+            E : PSL_Entry renames PSL_Table.Table (I);
+         begin
+            Disp_Instance_Name (E.Instance);
+            Put ('.');
+            Put (Name_Table.Image (Get_Identifier (E.Stmt)));
+            New_Line;
+            Disp_Vhdl.Disp_PSL_NFA (Get_PSL_NFA (E.Stmt));
+            Put ("    01234567890123456789012345678901234567890123456789");
+            for I in E.States'Range loop
+               if I mod 50 = 0 then
+                  New_Line;
+                  Put (Int32'Image (I / 10));
+                  Put (": ");
+               end if;
+               if E.States (I) then
+                  Put ('*');
+               else
+                  Put ('.');
+               end if;
+            end loop;
+            New_Line;
+         end;
+      end loop;
+   end Info_PSL_Proc;
+
    procedure Info_Stats_Proc (Line : String) is
       P : Natural := Line'First;
       E : Natural;
@@ -1324,7 +1360,8 @@ package body Debugger is
       end if;
    end Info_Stats_Proc;
 
-   procedure Info_Files_Proc (Line : String) is
+   procedure Info_Files_Proc (Line : String)
+   is
       pragma Unreferenced (Line);
       Status : Walk_Status;
    begin
@@ -1706,10 +1743,16 @@ package body Debugger is
       end loop;
    end Cont_Proc;
 
+   Menu_Info_Psl : aliased Menu_Entry :=
+     (Kind => Menu_Command,
+      Name => new String'("psl"),
+      Next => null,
+      Proc => Info_PSL_Proc'Access);
+
    Menu_Info_Stats : aliased Menu_Entry :=
      (Kind => Menu_Command,
       Name => new String'("stats"),
-      Next => null,
+      Next => Menu_Info_Psl'Access,
       Proc => Info_Stats_Proc'Access);
 
    Menu_Info_Tree : aliased Menu_Entry :=
diff --git a/src/vhdl/simulate/simulation.adb b/src/vhdl/simulate/simulation.adb
index b02d47dd2..c33997b7d 100644
--- a/src/vhdl/simulate/simulation.adb
+++ b/src/vhdl/simulate/simulation.adb
@@ -1112,6 +1112,9 @@ package body Simulation is
       Release (Marker, Expr_Pool);
       if V then
          Nvec := (others => False);
+         if Get_Kind (E.Stmt) = Iir_Kind_Psl_Cover_Statement then
+            Nvec (0) := True;
+         end if;
 
          --  For each state: if set, evaluate all outgoing edges.
          NFA := Get_PSL_NFA (E.Stmt);
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index b2138cd06..36a8ec471 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -450,6 +450,12 @@ 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;
       Start_Loop_Stmt (Label);
       Gen_Exit_When
         (Label,
@@ -1372,7 +1378,7 @@ package body Trans.Chap9 is
       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 (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);