netlists: add assume gate.

5 files changed, 29 insertions, 3 deletions

diff --git a/src/synth/ghdlsynth_gates.h b/src/synth/ghdlsynth_gates.h
index 90872d312..b923652aa 100644
--- a/src/synth/ghdlsynth_gates.h
+++ b/src/synth/ghdlsynth_gates.h
@@ -54,6 +54,7 @@ enum Module_Id {
    Id_Dyn_Insert = 49,
    Id_Edge = 50,
    Id_Assert = 51,
+   Id_Assume = 52,
    Id_Const_UB32 = 56,
    Id_Const_SB32 = 57,
    Id_Const_UB64 = 58,
diff --git a/src/synth/netlists-builders.adb b/src/synth/netlists-builders.adb
index d0106b10b..089781aad 100644
--- a/src/synth/netlists-builders.adb
+++ b/src/synth/netlists-builders.adb
@@ -333,7 +333,7 @@ package body Netlists.Builders is
                      Outputs);
    end Create_Dff_Modules;
 
-   procedure Create_Assert (Ctxt : Context_Acc)
+   procedure Create_Assert_Assume (Ctxt : Context_Acc)
    is
       Outputs : Port_Desc_Array (1 .. 0);
    begin
@@ -342,7 +342,13 @@ package body Netlists.Builders is
          1, 0, 0);
       Set_Port_Desc (Ctxt.M_Assert, (0 => Create_Input ("cond", 1)),
                      Outputs);
-   end Create_Assert;
+
+      Ctxt.M_Assume := New_User_Module
+        (Ctxt.Design, New_Sname_Artificial (Name_Assume), Id_Assume,
+         1, 0, 0);
+      Set_Port_Desc (Ctxt.M_Assume, (0 => Create_Input ("cond", 1)),
+                     Outputs);
+   end Create_Assert_Assume;
 
    function Build_Builders (Design : Module) return Context_Acc
    is
@@ -408,13 +414,18 @@ package body Netlists.Builders is
       Create_Monadic_Module (Design, Res.M_Extend (Id_Sextend),
                              Get_Identifier ("sextend"), Id_Sextend);
 
+      Create_Monadic_Module (Design, Res.M_Reduce (Id_Red_Or),
+                             Get_Identifier ("red_or"), Id_Red_Or);
+      Create_Monadic_Module (Design, Res.M_Reduce (Id_Red_And),
+                             Get_Identifier ("red_and"), Id_Red_And);
+
       Create_Edge_Module (Res, Res.M_Edge, Name_Edge);
 
       Create_Mux_Modules (Res);
       Create_Objects_Module (Res);
       Create_Dff_Modules (Res);
 
-      Create_Assert (Res);
+      Create_Assert_Assume (Res);
 
       return Res;
    end Build_Builders;
@@ -864,4 +875,12 @@ package body Netlists.Builders is
       Connect (Get_Input (Inst, 0), Cond);
    end Build_Assert;
 
+   procedure Build_Assume (Ctxt : Context_Acc; Cond : Net)
+   is
+      Inst : Instance;
+   begin
+      Inst := New_Internal_Instance (Ctxt, Ctxt.M_Assume);
+      Connect (Get_Input (Inst, 0), Cond);
+   end Build_Assume;
+
 end Netlists.Builders;
diff --git a/src/synth/netlists-builders.ads b/src/synth/netlists-builders.ads
index 9f7567ecb..08b67789b 100644
--- a/src/synth/netlists-builders.ads
+++ b/src/synth/netlists-builders.ads
@@ -90,6 +90,7 @@ package Netlists.Builders is
                           return Net;
 
    procedure Build_Assert (Ctxt : Context_Acc; Cond : Net);
+   procedure Build_Assume (Ctxt : Context_Acc; Cond : Net);
 
    --  A simple flip-flop.
    function Build_Dff (Ctxt : Context_Acc;
@@ -137,5 +138,6 @@ private
       M_Dyn_Extract : Module;
       M_Dyn_Insert : Module;
       M_Assert : Module;
+      M_Assume : Module;
    end record;
 end Netlists.Builders;
diff --git a/src/synth/netlists-disp_vhdl.adb b/src/synth/netlists-disp_vhdl.adb
index 644ae0ce1..a7999ba0c 100644
--- a/src/synth/netlists-disp_vhdl.adb
+++ b/src/synth/netlists-disp_vhdl.adb
@@ -607,6 +607,9 @@ package body Netlists.Disp_Vhdl is
             end;
          when Id_Assert =>
             Disp_Template ("  assert \i0 = '1' severity error;" & NL, Inst);
+         when Id_Assume =>
+            Disp_Template
+              ("  assert \i0 = '1' severity warning; --  assume" & 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 b150f158d..6e196f38d 100644
--- a/src/synth/netlists-gates.ads
+++ b/src/synth/netlists-gates.ads
@@ -137,6 +137,7 @@ package Netlists.Gates is
 
    --  Input signal must always be true.
    Id_Assert : constant Module_Id := 51;
+   Id_Assume : constant Module_Id := 52;
 
    --  Constants are gates with only one constant output.  There are multiple
    --  kind of constant gates: for small width, the value is stored as a