netlists: add formal input gates.

3 files changed, 44 insertions, 0 deletions

diff --git a/src/synth/netlists-builders.adb b/src/synth/netlists-builders.adb
index 7f0a58bde..0d88ec7ce 100644
--- a/src/synth/netlists-builders.adb
+++ b/src/synth/netlists-builders.adb
@@ -479,6 +479,19 @@ package body Netlists.Builders is
                      Outputs);
    end Create_Assert_Assume_Cover;
 
+   procedure Create_Formal_Input
+     (Ctxt : Context_Acc; Id : Formal_Module_Id; Name : Name_Id)
+   is
+      Outputs : Port_Desc_Array (0 .. 0);
+      Res : Module;
+   begin
+      Res := New_User_Module
+        (Ctxt.Design, New_Sname_Artificial (Name), Id, 0, 1, 0);
+      Ctxt.M_Formal_Input (Id) := Res;
+      Outputs := (0 => Create_Output ("o"));
+      Set_Port_Desc (Res, Port_Desc_Array'(1 .. 0 => <>), Outputs);
+   end Create_Formal_Input;
+
    function Build_Builders (Design : Module) return Context_Acc
    is
       Res : Context_Acc;
@@ -493,6 +506,7 @@ package body Netlists.Builders is
                           M_Concat => (others => No_Module),
                           M_Truncate | M_Extend => (others => No_Module),
                           M_Reduce => (others => No_Module),
+                          M_Formal_Input => (others => No_Module),
                           others => No_Module);
 
       Create_Dyadic_Module (Design, Res.M_Dyadic (Id_And), Name_And, Id_And);
@@ -602,6 +616,11 @@ package body Netlists.Builders is
 
       Create_Assert_Assume_Cover (Res);
 
+      Create_Formal_Input (Res, Id_Allconst, Name_Allconst);
+      Create_Formal_Input (Res, Id_Anyconst, Name_Anyconst);
+      Create_Formal_Input (Res, Id_Allseq, Name_Allseq);
+      Create_Formal_Input (Res, Id_Anyseq, Name_Anyseq);
+
       return Res;
    end Build_Builders;
 
@@ -1446,4 +1465,17 @@ package body Netlists.Builders is
       return Build_Formal (Ctxt, Ctxt.M_Assert_Cover, Name, Cond);
    end Build_Assert_Cover;
 
+   function Build_Formal_Input
+     (Ctxt : Context_Acc; Id : Formal_Module_Id; W : Width) return Net
+   is
+      Inst : Instance;
+      O : Net;
+   begin
+      Inst := New_Instance (Ctxt.Parent, Ctxt.M_Formal_Input (Id),
+                            New_Internal_Name (Ctxt));
+      O := Get_Output (Inst, 0);
+      Set_Width (O, W);
+      return O;
+   end Build_Formal_Input;
+
 end Netlists.Builders;
diff --git a/src/synth/netlists-builders.ads b/src/synth/netlists-builders.ads
index 63619a306..1b42b52ab 100644
--- a/src/synth/netlists-builders.ads
+++ b/src/synth/netlists-builders.ads
@@ -175,6 +175,9 @@ package Netlists.Builders is
    function Build_Assert_Cover (Ctxt : Context_Acc; Name : Sname; Cond : Net)
                          return Instance;
 
+   function Build_Formal_Input
+     (Ctxt : Context_Acc; Id : Formal_Module_Id; W : Width) return Net;
+
    --  A simple flip-flop.
    function Build_Dff (Ctxt : Context_Acc;
                        Clk : Net;
@@ -240,5 +243,6 @@ private
       M_Assume : Module;
       M_Cover : Module;
       M_Assert_Cover : Module;
+      M_Formal_Input : Module_Arr (Formal_Module_Id);
    end record;
 end Netlists.Builders;
diff --git a/src/synth/netlists-gates.ads b/src/synth/netlists-gates.ads
index ae6c2f58d..69546f479 100644
--- a/src/synth/netlists-gates.ads
+++ b/src/synth/netlists-gates.ads
@@ -210,6 +210,14 @@ package Netlists.Gates is
    --  Use to cover the precedent of an assertion.
    Id_Assert_Cover : constant Module_Id := 84;
 
+   --  Formal gates.
+   Id_Allconst : constant Module_Id := 90;
+   Id_Anyconst : constant Module_Id := 91;
+   Id_Allseq : constant Module_Id := 92;
+   Id_Anyseq : constant Module_Id := 93;
+
+   subtype Formal_Module_Id is Module_Id range Id_Allconst .. Id_Anyseq;
+
    --  Constants are gates with only one constant output.  There are multiple
    --  kind of constant gates: for small width, the value is stored as a
    --  parameter, possibly signed or unsigned extended.