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

4 files changed, 15 insertions, 8 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.