From 847de3fbeb301f60b00d59524c14cf74f562c268 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Tue, 15 Oct 2019 20:39:54 +0200
Subject: vhdl: Add the implicit [*] at start of PSL cover sequence.

---
 src/psl/psl-nfas-utils.adb | 26 ++++++++++++++++++++++++++
 src/psl/psl-nfas-utils.ads |  4 ++++
 2 files changed, 30 insertions(+)

(limited to 'src/psl')

diff --git a/src/psl/psl-nfas-utils.adb b/src/psl/psl-nfas-utils.adb
index 16c0ac6d5..a773b0702 100644
--- a/src/psl/psl-nfas-utils.adb
+++ b/src/psl/psl-nfas-utils.adb
@@ -347,4 +347,30 @@ package body PSL.NFAs.Utils is
       end case;
    end Has_EOS;
 
+   procedure Set_Init_Loop (N : NFA)
+   is
+      Start : constant NFA_State := Get_Start_State (N);
+      E : NFA_Edge;
+      Expr : Node;
+   begin
+      --  Look for existing edge.
+      E := Get_First_Src_Edge (Start);
+      while E /= No_Edge loop
+         if Get_Edge_Dest (E) = Start then
+            Expr := Get_Edge_Expr (E);
+            if Get_Kind (Expr) = N_True then
+               return;
+            end if;
+            Expr := Create_Node (N_True);
+            Set_Edge_Expr (E, Expr);
+            return;
+         end if;
+         E := Get_Next_Src_Edge (E);
+      end loop;
+
+      --  No existing edge.  Create one.
+      Expr := Create_Node (N_True);
+      Add_Edge (Start, Start, Expr);
+   end Set_Init_Loop;
+
 end PSL.NFAs.Utils;
diff --git a/src/psl/psl-nfas-utils.ads b/src/psl/psl-nfas-utils.ads
index f30f665a8..3f11ee880 100644
--- a/src/psl/psl-nfas-utils.ads
+++ b/src/psl/psl-nfas-utils.ads
@@ -33,6 +33,10 @@ package PSL.NFAs.Utils is
    --  N must be a boolean expression.
    function Has_EOS (N : Node) return Boolean;
 
+   --  Ensure there is an edge from init state to itself, for the implicit
+   --  [*] of cover directive.
+   procedure Set_Init_Loop (N : NFA);
+
    --  Raise Program_Error if N is not internally coherent.
    procedure Check_NFA (N : NFA);
 end PSL.NFAs.Utils;
-- 
cgit v1.2.3