synth: Add support for PSL cover directive (#930)

* synth: Add support for PSL cover directive

* testsuite/synth: Add tests for PSL cover directives

6 files changed, 49 insertions, 3 deletions

diff --git a/src/synth/ghdlsynth_gates.h b/src/synth/ghdlsynth_gates.h
index bb8f6a4af..43fc416b0 100644
--- a/src/synth/ghdlsynth_gates.h
+++ b/src/synth/ghdlsynth_gates.h
@@ -58,6 +58,7 @@ enum Module_Id {
    Id_Edge = 71,
    Id_Assert = 72,
    Id_Assume = 73,
+   Id_Cover = 74,
    Id_Const_UB32 = 96,
    Id_Const_SB32 = 97,
    Id_Const_UL32 = 98,
diff --git a/src/synth/netlists-builders.adb b/src/synth/netlists-builders.adb
index 4b3ddae4f..14e0827d4 100644
--- a/src/synth/netlists-builders.adb
+++ b/src/synth/netlists-builders.adb
@@ -363,7 +363,7 @@ package body Netlists.Builders is
                      Outputs);
    end Create_Dff_Modules;
 
-   procedure Create_Assert_Assume (Ctxt : Context_Acc)
+   procedure Create_Assert_Assume_Cover (Ctxt : Context_Acc)
    is
       Outputs : Port_Desc_Array (1 .. 0);
    begin
@@ -378,7 +378,13 @@ package body Netlists.Builders is
          1, 0, 0);
       Set_Port_Desc (Ctxt.M_Assume, (0 => Create_Input ("cond", 1)),
                      Outputs);
-   end Create_Assert_Assume;
+
+      Ctxt.M_Cover := New_User_Module
+        (Ctxt.Design, New_Sname_Artificial (Name_Cover), Id_Cover,
+         1, 0, 0);
+      Set_Port_Desc (Ctxt.M_Cover, (0 => Create_Input ("cond", 1)),
+                     Outputs);
+   end Create_Assert_Assume_Cover;
 
    function Build_Builders (Design : Module) return Context_Acc
    is
@@ -479,7 +485,7 @@ package body Netlists.Builders is
       Create_Objects_Module (Res);
       Create_Dff_Modules (Res);
 
-      Create_Assert_Assume (Res);
+      Create_Assert_Assume_Cover (Res);
 
       return Res;
    end Build_Builders;
@@ -1146,4 +1152,15 @@ package body Netlists.Builders is
       return Inst;
    end Build_Assume;
 
+   function Build_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
+                         return Instance
+   is
+      Inst : Instance;
+   begin
+      Inst := New_Instance (Ctxt.Parent, Ctxt.M_Cover,
+                            Name_Or_Internal (Name, Ctxt));
+      Connect (Get_Input (Inst, 0), Cond);
+      return Inst;
+   end Build_Cover;
+
 end Netlists.Builders;
diff --git a/src/synth/netlists-builders.ads b/src/synth/netlists-builders.ads
index 7cf9a3058..8395c6292 100644
--- a/src/synth/netlists-builders.ads
+++ b/src/synth/netlists-builders.ads
@@ -147,6 +147,8 @@ package Netlists.Builders is
                          return Instance;
    function Build_Assume (Ctxt : Context_Acc; Name : Sname; Cond : Net)
                          return Instance;
+   function Build_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
+                        return Instance;
 
    --  A simple flip-flop.
    function Build_Dff (Ctxt : Context_Acc;
@@ -204,5 +206,6 @@ private
       M_Dyn_Insert : Module;
       M_Assert : Module;
       M_Assume : Module;
+      M_Cover : Module;
    end record;
 end Netlists.Builders;
diff --git a/src/synth/netlists-disp_vhdl.adb b/src/synth/netlists-disp_vhdl.adb
index ef9db9b30..632966645 100644
--- a/src/synth/netlists-disp_vhdl.adb
+++ b/src/synth/netlists-disp_vhdl.adb
@@ -743,6 +743,10 @@ package body Netlists.Disp_Vhdl is
             Disp_Template
               ("  \l0: assert \i0 = '1' severity warning; --  assume" & NL,
                Inst);
+         when Id_Cover =>
+            Disp_Template
+              ("  \l0: assert \i0 = '1' severity note; --  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 b33da9778..7f3012063 100644
--- a/src/synth/netlists-gates.ads
+++ b/src/synth/netlists-gates.ads
@@ -148,6 +148,7 @@ package Netlists.Gates is
    --  Input signal must always be true.
    Id_Assert : constant Module_Id := 72;
    Id_Assume : constant Module_Id := 73;
+   Id_Cover : constant Module_Id := 74;
 
    --  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 2abfc6bf9..03f6d06e9 100644
--- a/src/synth/synth-stmts.adb
+++ b/src/synth/synth-stmts.adb
@@ -1722,6 +1722,22 @@ package body Synth.Stmts is
       end if;
    end Synth_Psl_Restrict_Directive;
 
+   procedure Synth_Psl_Cover_Directive
+     (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
+   is
+      Res : Net;
+      Inst : Instance;
+   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
+         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
@@ -1949,6 +1965,8 @@ package body Synth.Stmts is
                Synth_Psl_Restrict_Directive (Syn_Inst, Stmt);
             when Iir_Kind_Psl_Assume_Directive =>
                Synth_Psl_Assume_Directive (Syn_Inst, Stmt);
+            when Iir_Kind_Psl_Cover_Directive =>
+               Synth_Psl_Cover_Directive (Syn_Inst, Stmt);
             when Iir_Kind_Psl_Assert_Directive =>
                Synth_Psl_Assert_Directive (Syn_Inst, Stmt);
             when Iir_Kind_Concurrent_Assertion_Statement =>
@@ -1975,6 +1993,8 @@ package body Synth.Stmts is
                Synth_Psl_Assert_Directive (Syn_Inst, Item);
             when Iir_Kind_Psl_Assume_Directive =>
                Synth_Psl_Assume_Directive (Syn_Inst, Item);
+            when Iir_Kind_Psl_Cover_Directive =>
+               Synth_Psl_Cover_Directive (Syn_Inst, Item);
             when others =>
                Error_Kind ("synth_verification_unit", Item);
          end case;