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

6 files changed, 48 insertions, 20 deletions

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