synth: generate cover for assertion precedent.

5 files changed, 103 insertions, 84 deletions

diff --git a/src/synth/netlists-builders.adb b/src/synth/netlists-builders.adb
index 74f43d434..7373ccc0a 100644
--- a/src/synth/netlists-builders.adb
+++ b/src/synth/netlists-builders.adb
@@ -471,6 +471,12 @@ package body Netlists.Builders is
          1, 0, 0);
       Set_Port_Desc (Ctxt.M_Cover, (0 => Create_Input ("cond", 1)),
                      Outputs);
+
+      Ctxt.M_Assert_Cover := New_User_Module
+        (Ctxt.Design, New_Sname_Artificial (Get_Identifier ("assert_cover")),
+         Id_Assert_Cover, 1, 0, 0);
+      Set_Port_Desc (Ctxt.M_Assert_Cover, (0 => Create_Input ("cond", 1)),
+                     Outputs);
    end Create_Assert_Assume_Cover;
 
    function Build_Builders (Design : Module) return Context_Acc
@@ -1368,37 +1374,40 @@ package body Netlists.Builders is
       end if;
    end Name_Or_Internal;
 
-   function Build_Assert (Ctxt : Context_Acc; Name : Sname; Cond : Net)
-                         return Instance
+   function Build_Formal
+     (Ctxt : Context_Acc; Gate : Module; Name : Sname; Cond : Net)
+     return Instance
    is
       Inst : Instance;
    begin
-      Inst := New_Instance (Ctxt.Parent, Ctxt.M_Assert,
+      Inst := New_Instance (Ctxt.Parent, Gate,
                             Name_Or_Internal (Name, Ctxt));
       Connect (Get_Input (Inst, 0), Cond);
       return Inst;
+   end Build_Formal;
+
+   function Build_Assert (Ctxt : Context_Acc; Name : Sname; Cond : Net)
+                         return Instance is
+   begin
+      return Build_Formal (Ctxt, Ctxt.M_Assert, Name, Cond);
    end Build_Assert;
 
    function Build_Assume (Ctxt : Context_Acc; Name : Sname; Cond : Net)
-                         return Instance
-   is
-      Inst : Instance;
+                         return Instance is
    begin
-      Inst := New_Instance (Ctxt.Parent, Ctxt.M_Assume,
-                            Name_Or_Internal (Name, Ctxt));
-      Connect (Get_Input (Inst, 0), Cond);
-      return Inst;
+      return Build_Formal (Ctxt, Ctxt.M_Assume, Name, Cond);
    end Build_Assume;
 
    function Build_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
-                         return Instance
-   is
-      Inst : Instance;
+                         return Instance is
    begin
-      Inst := New_Instance (Ctxt.Parent, Ctxt.M_Cover,
-                            Name_Or_Internal (Name, Ctxt));
-      Connect (Get_Input (Inst, 0), Cond);
-      return Inst;
+      return Build_Formal (Ctxt, Ctxt.M_Cover, Name, Cond);
    end Build_Cover;
 
+   function Build_Assert_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
+                         return Instance is
+   begin
+      return Build_Formal (Ctxt, Ctxt.M_Assert_Cover, Name, Cond);
+   end Build_Assert_Cover;
+
 end Netlists.Builders;
diff --git a/src/synth/netlists-builders.ads b/src/synth/netlists-builders.ads
index 4a76e5b52..2d177653b 100644
--- a/src/synth/netlists-builders.ads
+++ b/src/synth/netlists-builders.ads
@@ -168,6 +168,8 @@ package Netlists.Builders is
                          return Instance;
    function Build_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
                         return Instance;
+   function Build_Assert_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
+                         return Instance;
 
    --  A simple flip-flop.
    function Build_Dff (Ctxt : Context_Acc;
@@ -233,5 +235,6 @@ private
       M_Assert : Module;
       M_Assume : Module;
       M_Cover : Module;
+      M_Assert_Cover : Module;
    end record;
 end Netlists.Builders;
diff --git a/src/synth/netlists-disp_vhdl.adb b/src/synth/netlists-disp_vhdl.adb
index 1215d10e6..78f1efe0d 100644
--- a/src/synth/netlists-disp_vhdl.adb
+++ b/src/synth/netlists-disp_vhdl.adb
@@ -1051,6 +1051,10 @@ package body Netlists.Disp_Vhdl is
             Disp_Template
               ("  \l0: assert \i0 = '1' severity note; --  cover" & NL,
                Inst);
+         when Id_Assert_Cover =>
+            Disp_Template
+              ("  \l0: assert \i0 = '1' severity note; --  assert_cover" & NL,
+               Inst);
          when others =>
             Disp_Instance_Gate (Inst);
       end case;
diff --git a/src/synth/netlists-gates.ads b/src/synth/netlists-gates.ads
index e0cf9a6e1..ae6c2f58d 100644
--- a/src/synth/netlists-gates.ads
+++ b/src/synth/netlists-gates.ads
@@ -204,7 +204,11 @@ package Netlists.Gates is
    --  Input signal must always be true.
    Id_Assert : constant Module_Id := 81;
    Id_Assume : constant Module_Id := 82;
+
+   --  Input is true when a sequence is covered.
    Id_Cover : constant Module_Id := 83;
+   --  Use to cover the precedent of an assertion.
+   Id_Assert_Cover : constant Module_Id := 84;
 
    --  Constants are gates with only one constant output.  There are multiple
    --  kind of constant gates: for small width, the value is stored as a
diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb
index 732ed9a93..5977c978e 100644
--- a/src/synth/synth-stmts.adb
+++ b/src/synth/synth-stmts.adb
@@ -2276,16 +2276,16 @@ package body Synth.Stmts is
       return Res;
    end Synth_Psl_NFA;
 
-   function Synth_Psl_Sequence_Directive
-     (Syn_Inst : Synth_Instance_Acc; Stmt : Node) return Net
+   procedure Synth_Psl_Dff (Syn_Inst : Synth_Instance_Acc;
+                            Stmt : Node;
+                            Next_States : out Net)
    is
       use Netlists.Gates;
       Nbr_States : constant Int32 := Get_PSL_Nbr_States (Stmt);
+      States : Net;
       Init : Net;
       Clk : Net;
       Clk_Inst : Instance;
-      States : Net;
-      Next_States : Net;
    begin
       --  create init net, clock net
       pragma Assert (Nbr_States <= 32);
@@ -2296,7 +2296,8 @@ package body Synth.Stmts is
       Clk_Inst := Get_Net_Parent (Clk);
       if Get_Id (Clk_Inst) /= Id_Edge then
          Error_Msg_Synth (+Stmt, "clock is not an edge");
-         return No_Net;
+         Next_States := No_Net;
+         return;
       end if;
 
       Clk := Get_Input_Net (Clk_Inst, 0);
@@ -2309,24 +2310,44 @@ package body Synth.Stmts is
       Next_States :=
         Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States);
       Connect (Get_Input (Get_Net_Parent (States), 1), Next_States);
+   end Synth_Psl_Dff;
 
-      return Next_States;
-   end Synth_Psl_Sequence_Directive;
+   function Synth_Psl_Final
+     (Syn_Inst : Synth_Instance_Acc; Stmt : Node; Next_States : Net) return Net
+   is
+      use PSL.Types;
+      use PSL.NFAs;
+      NFA : constant PSL_NFA := Get_PSL_NFA (Stmt);
+   begin
+      return Build_Extract_Bit
+        (Get_Build (Syn_Inst), Next_States,
+         Uns32 (Get_State_Label (Get_Final_State (NFA))));
+   end Synth_Psl_Final;
+
+   function Synth_Psl_Not_Final
+     (Syn_Inst : Synth_Instance_Acc; Stmt : Node; Next_States : Net)
+     return Net is
+   begin
+      return Build_Monadic
+        (Get_Build (Syn_Inst), Netlists.Gates.Id_Not,
+         Synth_Psl_Final (Syn_Inst, Stmt, Next_States));
+   end Synth_Psl_Not_Final;
 
    procedure Synth_Psl_Restrict_Directive
      (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
    is
+      Next_States : Net;
       Res : Net;
       Inst : Instance;
    begin
       --  Build assume gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assume on States, then the first cycle is ignored).
-      Res := Synth_Psl_Sequence_Directive (Syn_Inst, Stmt);
-      if Res /= No_Net then
+      Synth_Psl_Dff (Syn_Inst, Stmt, Next_States);
+      if Next_States /= No_Net then
          --  The restriction holds as long as there is a 1 in the NFA state.
          Res := Build_Reduce (Build_Context,
-                              Netlists.Gates.Id_Red_Or, Res);
+                              Netlists.Gates.Id_Red_Or, Next_States);
          Inst := Build_Assume (Build_Context, Synth_Label (Stmt), Res);
          Set_Location (Inst, Get_Location (Stmt));
       end if;
@@ -2335,79 +2356,36 @@ package body Synth.Stmts is
    procedure Synth_Psl_Cover_Directive
      (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
    is
-      use PSL.NFAs;
+      Next_States : Net;
       Res : Net;
       Inst : Instance;
-      S_Num : Int32;
    begin
       --  Build cover gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assume on States, then the first cycle is ignored).
-      Res := Synth_Psl_Sequence_Directive (Syn_Inst, Stmt);
-      if Res /= No_Net then
+      Synth_Psl_Dff (Syn_Inst, Stmt, Next_States);
+      if Next_States /= No_Net then
          --  The sequence is covered as soon as the final state is reached.
-         S_Num := Get_State_Label (Get_Final_State (Get_PSL_NFA (Stmt)));
-         Res := Build_Extract_Bit (Get_Build (Syn_Inst), Res, Uns32 (S_Num));
+         Res := Synth_Psl_Final (Syn_Inst, Stmt, Next_States);
          Inst := Build_Cover (Build_Context, Synth_Label (Stmt), Res);
          Set_Location (Inst, Get_Location (Stmt));
       end if;
    end Synth_Psl_Cover_Directive;
 
-   function Synth_Psl_Property_Directive
-     (Syn_Inst : Synth_Instance_Acc; Stmt : Node) return Net
-   is
-      use PSL.Types;
-      use PSL.NFAs;
-      use Netlists.Gates;
-      NFA : constant PSL_NFA := Get_PSL_NFA (Stmt);
-      Nbr_States : constant Int32 := Get_PSL_Nbr_States (Stmt);
-      Init : Net;
-      Clk : Net;
-      Clk_Inst : Instance;
-      States : Net;
-      Next_States : Net;
-   begin
-      --  create init net, clock net
-      pragma Assert (Nbr_States <= 32);
-      Init := Build_Const_UB32 (Build_Context, 1, Uns32 (Nbr_States));
-      Clk := Synth_PSL_Expression (Syn_Inst, Get_PSL_Clock (Stmt));
-
-      --  Check the clock is an edge and extract it.
-      Clk_Inst := Get_Net_Parent (Clk);
-      if Get_Id (Clk_Inst) /= Id_Edge then
-         Error_Msg_Synth (+Stmt, "clock is not an edge");
-         return No_Net;
-      end if;
-
-      Clk := Get_Input_Net (Clk_Inst, 0);
-
-      --  build idff
-      States := Build_Idff (Build_Context, Clk, No_Net, Init);
-
-      --  create update nets
-      --  For each state: if set, evaluate all outgoing edges.
-      Next_States := Synth_Psl_NFA (Syn_Inst, NFA, Nbr_States, States);
-      Connect (Get_Input (Get_Net_Parent (States), 1), Next_States);
-
-      return Build_Monadic
-        (Build_Context, Netlists.Gates.Id_Not,
-         Build_Extract_Bit
-           (Build_Context, Next_States,
-            Uns32 (Get_State_Label (Get_Final_State (NFA)))));
-   end Synth_Psl_Property_Directive;
-
    procedure Synth_Psl_Assume_Directive
      (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
    is
-      Res : Net;
+      Next_States : Net;
       Inst : Instance;
    begin
       --  Build assume gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assume on States, then the first cycle is ignored).
-      Res := Synth_Psl_Property_Directive (Syn_Inst, Stmt);
-      if Res /= No_Net then
-         Inst := Build_Assume (Build_Context, Synth_Label (Stmt), Res);
+      Synth_Psl_Dff (Syn_Inst, Stmt, Next_States);
+      if Next_States /= No_Net then
+         Inst := Build_Assume
+           (Build_Context, Synth_Label (Stmt),
+            Synth_Psl_Not_Final (Syn_Inst, Stmt, Next_States));
          Set_Location (Inst, Get_Location (Stmt));
       end if;
    end Synth_Psl_Assume_Directive;
@@ -2415,16 +2393,37 @@ package body Synth.Stmts is
    procedure Synth_Psl_Assert_Directive
      (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
    is
-      Res : Net;
+      use PSL.Types;
+      use PSL.NFAs;
+      NFA : constant PSL_NFA := Get_PSL_NFA (Stmt);
+      Active : NFA_State;
+      Next_States : Net;
       Inst : Instance;
+      Lab : Sname;
    begin
       --  Build assert gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assert on States, then the first cycle is ignored).
-      Res := Synth_Psl_Property_Directive (Syn_Inst, Stmt);
-      if Res /= No_Net then
-         Inst := Build_Assert (Build_Context, Synth_Label (Stmt), Res);
+      Synth_Psl_Dff (Syn_Inst, Stmt, Next_States);
+      if Next_States /= No_Net then
+         Lab := Synth_Label (Stmt);
+
+         Inst := Build_Assert
+           (Build_Context, Lab,
+            Synth_Psl_Not_Final (Syn_Inst, Stmt, Next_States));
          Set_Location (Inst, Get_Location (Stmt));
+
+         Active := Get_Active_State (NFA);
+         if Active /= No_State then
+            if Lab /= No_Sname then
+               Lab := New_Sname (Lab, Std_Names.Name_Cover);
+            end if;
+            Inst := Build_Assert_Cover
+              (Get_Build (Syn_Inst), Lab,
+               Build_Extract_Bit (Get_Build (Syn_Inst), Next_States,
+                                  Uns32 (Get_State_Label (Active))));
+            Set_Location (Inst, Get_Location (Stmt));
+         end if;
       end if;
    end Synth_Psl_Assert_Directive;