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 ++++
 src/vhdl/vhdl-canon.adb    |  7 +++++++
 3 files changed, 37 insertions(+)

(limited to 'src')

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;
diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb
index bddcc228f..f7778db00 100644
--- a/src/vhdl/vhdl-canon.adb
+++ b/src/vhdl/vhdl-canon.adb
@@ -1795,6 +1795,13 @@ package body Vhdl.Canon is
 
       --  Generate the NFA.
       Fa := PSL.Build.Build_SERE_FA (Seq);
+
+      --  IEEE1850-2005 PSL 7.1.6
+      --  cover {r} is semantically equivalent to cover {[*]; r}.  That is,
+      --  there is an implicit [*] starting the sequence.
+      if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Directive then
+         PSL.NFAs.Utils.Set_Init_Loop (Fa);
+      end if;
       Set_PSL_NFA (Stmt, Fa);
 
       Canon_Psl_Clocked_NFA (Stmt);
-- 
cgit v1.2.3