synth: add support for sequential assertions. Fix #1273

6 files changed, 312 insertions, 58 deletions

diff --git a/src/synth/netlists-cleanup.adb b/src/synth/netlists-cleanup.adb
index 24889cd6c..c24a89031 100644
--- a/src/synth/netlists-cleanup.adb
+++ b/src/synth/netlists-cleanup.adb
@@ -126,9 +126,10 @@ package body Netlists.Cleanup is
 
          case Get_Id (Inst) is
             when Id_Output
-              | Id_Ioutput
-              | Id_Port
-              | Id_Nop =>
+              |  Id_Ioutput
+              |  Id_Port
+              |  Id_Enable
+              |  Id_Nop =>
                declare
                   Inp : Input;
                   In_Drv : Net;
diff --git a/src/synth/netlists-inference.adb b/src/synth/netlists-inference.adb
index 9079a260d..7016f1f57 100644
--- a/src/synth/netlists-inference.adb
+++ b/src/synth/netlists-inference.adb
@@ -880,4 +880,155 @@ package body Netlists.Inference is
 
       return Res;
    end Infere;
+
+   --  INST is a mux2 of a condition chain.
+   --  Return the input that is not 0.  Could be either a mux2 or a const.
+   function Find_Condition_Chain_Next (Inst : Instance) return Instance
+   is
+      Mux_In0, Mux_In1 : Net;
+      In0_Inst, In1_Inst : Instance;
+   begin
+      Mux_In0 := Get_Input_Net (Inst, 1);
+      In0_Inst := Get_Net_Parent (Mux_In0);
+
+      Mux_In1 := Get_Input_Net (Inst, 2);
+      In1_Inst := Get_Net_Parent (Mux_In1);
+
+      if Get_Id (In0_Inst) /= Id_Const_UB32 then
+         --  The other input must be const 0.
+         pragma Assert (Get_Id (In1_Inst) = Id_Const_UB32
+                          and then Get_Param_Uns32 (In1_Inst, 0) = 0);
+         return In0_Inst;
+      else
+         --  Either both are const, or the other input must be const 0.
+         if Get_Id (In1_Inst) = Id_Const_UB32 then
+            --  Both are const.  Return the const 1.
+            if Get_Param_Uns32 (In1_Inst, 0) = 0 then
+               pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 1);
+               return In0_Inst;
+            else
+               pragma Assert (Get_Param_Uns32 (In1_Inst, 0) = 1);
+               pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 0);
+               return In1_Inst;
+            end if;
+         end if;
+
+         pragma Assert (Get_Param_Uns32 (In0_Inst, 0) = 0);
+         return In1_Inst;
+      end if;
+   end Find_Condition_Chain_Next;
+
+   --  VAL is a chain of mux2 that define the conditions to enable assertions.
+   function Infere_Assert (Ctxt : Context_Acc;
+                           Val : Net;
+                           En_Gate : Net;
+                           Stmt : Synth.Source.Syn_Src) return Net
+   is
+      Loc : constant Location_Type := Synth.Source."+" (Stmt);
+      Inst : Instance;
+      First_Inst, Last_Inst : Instance;
+      Clk, En : Net;
+      Areset : Net;
+      Zero : Net;
+   begin
+      --  Extract clock (if any) from VAL.  Return VAL is no clock.
+      First_Inst := Get_Net_Parent (Val);
+      Inst := First_Inst;
+      loop
+         if Get_Id (Inst) /= Id_Mux2 then
+            pragma Assert (Get_Id (Inst) = Id_Const_UB32);
+            return Val;
+         end if;
+         Extract_Clock (Ctxt, Get_Input_Net (Inst, 0), Clk, En);
+         exit when Clk /= No_Net;
+
+         --  No clock.  Try the father.
+         Inst := Find_Condition_Chain_Next (Inst);
+      end loop;
+
+      --  Extract enable and asynchronous reset (if any).
+      Last_Inst := Inst;
+      Areset := No_Net;
+      while Last_Inst /= Inst loop
+         declare
+            Cond : Net;
+            Next_Inst : Instance;
+         begin
+            Cond := Get_Input_Net (Inst, 0);
+
+            --  Find the next mux.
+            Next_Inst := Find_Condition_Chain_Next (Inst);
+
+            --  If the next mux is in0, negate COND.
+            if Next_Inst = Get_Net_Parent (Get_Input_Net (Inst, 1)) then
+               Cond := Build_Monadic (Ctxt, Id_Not, Cond);
+               Synth.Source.Set_Location (Cond, Stmt);
+            end if;
+
+            --  'And' COND to Areset.
+            Areset := Build2_And (Ctxt, Areset, Cond, Loc);
+
+            Inst := Next_Inst;
+         end;
+      end loop;
+
+      --  Same for LAST_INST, but check it is on in1.
+      declare
+         Next_Inst : Instance;
+      begin
+         Next_Inst := Find_Condition_Chain_Next (Last_Inst);
+         if Next_Inst /= Get_Net_Parent (Get_Input_Net (Inst, 2)) then
+            Error_Msg_Synth
+              (+Last_Inst, "assertion checked on else branch of an edge");
+            return Val;
+         end if;
+
+         En := Build2_And (Ctxt, En, Get_Output (Next_Inst, 0), Loc);
+         Zero := Get_Input_Net (Inst, 1);
+      end;
+
+      --  Build an idff/iadff for each condition of the assertions.
+      --  The caller will connect the returned value (En) to the enable gate.
+      declare
+         En_Inp : Input;
+         Assert_Inp : Input;
+         N : Net;
+         Dff : Net;
+      begin
+         En_Inp := Get_First_Sink (En_Gate);
+         pragma Assert (En_Inp /= No_Input);
+         while En_Inp /= No_Input loop
+            --  The Enable gate is connected to an implication.
+            Inst := Get_Input_Parent (En_Inp);
+            pragma Assert (Get_Id (Inst) = Id_Not);
+            N := Get_Output (Inst, 0);
+            pragma Assert (Has_One_Connection (N));
+            Inst := Get_Input_Parent (Get_First_Sink (N));
+            pragma Assert (Get_Id (Inst) = Id_Or);
+
+            N := Get_Output (Inst, 0);
+            pragma Assert (Has_One_Connection (N));
+            Inst := Get_Input_Parent (Get_First_Sink (N));
+
+            pragma Assert (Get_Id (Inst) = Id_Assert);
+
+            Assert_Inp := Get_Input (Inst, 0);
+            Disconnect (Assert_Inp);
+
+            if Areset = No_Net then
+               Dff := Build_Idff (Ctxt, Clk, N, Zero);
+            else
+               Dff := Build_Iadff (Ctxt, Clk, N, Areset, Zero, Zero);
+            end if;
+            Set_Location (Dff, Loc);
+
+            Connect (Assert_Inp, Dff);
+
+            En_Inp := Get_Next_Sink (En_Inp);
+         end loop;
+      end;
+
+      return En;
+   end Infere_Assert;
+
 end Netlists.Inference;
diff --git a/src/synth/netlists-inference.ads b/src/synth/netlists-inference.ads
index 291b135bd..91ae6228b 100644
--- a/src/synth/netlists-inference.ads
+++ b/src/synth/netlists-inference.ads
@@ -41,4 +41,10 @@ package Netlists.Inference is
                     Prev_Val : Net;
                     Stmt : Synth.Source.Syn_Src;
                     Last_Use : Boolean) return Net;
+
+   --  Called when there is an assignment to a enable gate.
+   function Infere_Assert (Ctxt : Context_Acc;
+                           Val : Net;
+                           En_Gate : Net;
+                           Stmt : Synth.Source.Syn_Src) return Net;
 end Netlists.Inference;
diff --git a/src/synth/synth-environment.adb b/src/synth/synth-environment.adb
index 59b3938f5..4e789ef05 100644
--- a/src/synth/synth-environment.adb
+++ b/src/synth/synth-environment.adb
@@ -77,37 +77,6 @@ package body Synth.Environment is
       Wire_Rec.Kind := Wire_None;
    end Free_Wire;
 
-   procedure Mark (M : out Wire_Id) is
-   begin
-      M := Wire_Id_Table.Last;
-   end Mark;
-
-   procedure Release (M : in out Wire_Id) is
-   begin
-      --  Check all wires to be released are free.
-      for I in M + 1 .. Wire_Id_Table.Last loop
-         declare
-            Wire_Rec : Wire_Id_Record renames Wire_Id_Table.Table (I);
-         begin
-            if Wire_Rec.Kind /= Wire_None then
-               raise Internal_Error;
-            end if;
-         end;
-      end loop;
-
-      --  Release.
-      Wire_Id_Table.Set_Last (M);
-
-      M := No_Wire_Id;
-   end Release;
-
-   procedure All_Released is
-   begin
-      if Wire_Id_Table.Last /= No_Wire_Id then
-         raise Internal_Error;
-      end if;
-   end All_Released;
-
    procedure Set_Wire_Gate (Wid : Wire_Id; Gate : Net) is
    begin
       --  Cannot override a gate.
@@ -203,9 +172,61 @@ package body Synth.Environment is
    begin
       Phis_Table.Append ((First => No_Seq_Assign,
                           Last => No_Seq_Assign,
-                          Nbr => 0));
+                          Nbr => 0,
+                          En => No_Wire_Id));
    end Push_Phi;
 
+   procedure Mark (M : out Wire_Id) is
+   begin
+      M := Wire_Id_Table.Last;
+   end Mark;
+
+   procedure Release (M : in out Wire_Id)
+   is
+      Last : Wire_Id;
+   begin
+      --  Check all wires to be released are free.
+      Last := M;
+      for I in M + 1 .. Wire_Id_Table.Last loop
+         declare
+            Wire_Rec : Wire_Id_Record renames Wire_Id_Table.Table (I);
+            Asgn : Seq_Assign;
+         begin
+            case Wire_Rec.Kind is
+               when Wire_None =>
+                  null;
+               when Wire_Enable =>
+                  --  Keep.  This renames the wire, but the only references
+                  --  must be in the wire.
+                  Last := Last + 1;
+                  if Last /= I then
+                     --  Renames.
+                     Asgn := Wire_Rec.Cur_Assign;
+                     while Asgn /= No_Seq_Assign loop
+                        Assign_Table.Table (Asgn).Id := Last;
+                        Asgn := Get_Assign_Prev (Asgn);
+                     end loop;
+                     Wire_Id_Table.Table (Last) := Wire_Rec;
+                  end if;
+               when others =>
+                  raise Internal_Error;
+            end case;
+         end;
+      end loop;
+
+      --  Release.
+      Wire_Id_Table.Set_Last (Last);
+
+      M := No_Wire_Id;
+   end Release;
+
+   procedure All_Released is
+   begin
+      if Wire_Id_Table.Last /= No_Wire_Id then
+         raise Internal_Error;
+      end if;
+   end All_Released;
+
    --  Concatenate when possible partial assignments of HEAD.
    procedure Merge_Partial_Assignments
      (Ctxt : Context_Acc; Head : Seq_Assign_Value)
@@ -291,7 +312,10 @@ package body Synth.Environment is
       Wid : Wire_Id;
    begin
       Asgn := Phi.First;
-      Phi := (First => No_Seq_Assign, Last => No_Seq_Assign, Nbr => 0);
+      Phi := (First => No_Seq_Assign,
+              Last => No_Seq_Assign,
+              Nbr => 0,
+              En => No_Wire_Id);
       while Asgn /= No_Seq_Assign loop
          pragma Assert (Assign_Table.Table (Asgn).Phi = Current_Phi);
          Next_Asgn := Get_Assign_Chain (Asgn);
@@ -382,6 +406,11 @@ package body Synth.Environment is
                begin
                   if Synth.Flags.Flag_Debug_Noinference then
                      Res := Pa.Value;
+                  elsif Wire_Rec.Kind = Wire_Enable then
+                     --  Possibly infere a idff/iadff.
+                     pragma Assert (Pa.Offset = 0);
+                     Res := Inference.Infere_Assert
+                       (Ctxt, Pa.Value, Outport, Stmt);
                   else
                      --  Note: lifetime is currently based on the kind of the
                      --   wire (variable -> not reused beyond this process).
@@ -407,6 +436,7 @@ package body Synth.Environment is
       Asgn : Seq_Assign;
    begin
       Pop_Phi (Phi);
+      pragma Assert (Phis_Table.Last = No_Phi_Id);
 
       --  It is possible that the same value is assigned to different targets.
       --  Example:
@@ -939,9 +969,10 @@ package body Synth.Environment is
       W : constant Width := Get_Width (Wid_Rec.Gate);
    begin
       case Wid_Rec.Kind is
-         when Wire_Signal | Wire_Output | Wire_Inout | Wire_Variable =>
+         when Wire_Signal | Wire_Output | Wire_Inout
+           | Wire_Variable =>
             null;
-         when Wire_Input | Wire_None =>
+         when Wire_Input | Wire_Enable | Wire_None =>
             raise Internal_Error;
       end case;
 
@@ -981,7 +1012,8 @@ package body Synth.Environment is
             else
                return Get_Assign_Value (Ctxt, Wire_Rec.Cur_Assign);
             end if;
-         when Wire_Signal | Wire_Output | Wire_Inout | Wire_Input =>
+         when Wire_Signal | Wire_Output | Wire_Inout | Wire_Input
+           | Wire_Enable =>
             --  For signals, always read the previous value.
             return Wire_Rec.Gate;
          when Wire_None =>
@@ -1513,13 +1545,7 @@ package body Synth.Environment is
       end loop;
    end Merge_Phis;
 
-   procedure Phi_Append_Assign (Asgn : Seq_Assign)
-   is
-      pragma Assert (Asgn /= No_Seq_Assign);
-      Asgn_Rec : Seq_Assign_Record renames Assign_Table.Table (Asgn);
-      pragma Assert (Asgn_Rec.Phi = Current_Phi);
-      pragma Assert (Asgn_Rec.Chain = No_Seq_Assign);
-      P : Phi_Type renames Phis_Table.Table (Phis_Table.Last);
+   procedure Phi_Append_Assign (P : in out Phi_Type; Asgn : Seq_Assign) is
    begin
       --  Chain assignment in the current sequence.
       if P.First = No_Seq_Assign then
@@ -1531,6 +1557,64 @@ package body Synth.Environment is
       P.Nbr := P.Nbr + 1;
    end Phi_Append_Assign;
 
+   procedure Phi_Append_Assign (Asgn : Seq_Assign)
+   is
+      pragma Assert (Asgn /= No_Seq_Assign);
+      Asgn_Rec : Seq_Assign_Record renames Assign_Table.Table (Asgn);
+      pragma Assert (Asgn_Rec.Phi = Current_Phi);
+      pragma Assert (Asgn_Rec.Chain = No_Seq_Assign);
+   begin
+      Phi_Append_Assign (Phis_Table.Table (Phis_Table.Last), Asgn);
+   end Phi_Append_Assign;
+
+   function Phi_Enable (Ctxt : Builders.Context_Acc; Loc : Source.Syn_Src)
+                       return Net
+   is
+      Last : constant Phi_Id := Phis_Table.Last;
+      Wid : Wire_Id;
+      N : Net;
+      Asgn : Seq_Assign;
+   begin
+      if Last = No_Phi_Id then
+         --  Can be called only when a phi is created.
+         raise Internal_Error;
+      end if;
+      if Last = No_Phi_Id + 1 then
+         --  That's the first phi, which is always enabled.
+         return No_Net;
+      end if;
+
+      --  Cached value.
+      Wid := Phis_Table.Table (Last).En;
+      if Wid = No_Wire_Id then
+         Wid := Alloc_Wire (Wire_Enable, Loc);
+         Phis_Table.Table (Last).En := Wid;
+
+         --  Create the Enable gate.
+         N := Build_Enable (Ctxt);
+         Set_Location (N, Loc);
+         Set_Wire_Gate (Wid, N);
+
+         --  Initialize to '0'.
+         --  This is really cheating, as it is like assigning in the first
+         --  phi.
+         Assign_Table.Append ((Phi => No_Phi_Id + 1,
+                               Id => Wid,
+                               Prev => No_Seq_Assign,
+                               Chain => No_Seq_Assign,
+                               Val => (Is_Static => True, Val => Bit0)));
+         Asgn := Assign_Table.Last;
+         Wire_Id_Table.Table (Wid).Cur_Assign := Asgn;
+         Phi_Append_Assign (Phis_Table.Table (No_Phi_Id + 1), Asgn);
+
+         --  Assign to '1'.
+         Phi_Assign_Static (Wid, Bit1);
+         return N;
+      else
+         return Get_Current_Value (Ctxt, Wid);
+      end if;
+   end Phi_Enable;
+
    --  Check consistency:
    --  - ordered.
    --  - no overlaps.
@@ -1753,7 +1837,8 @@ package body Synth.Environment is
       Phi_Assign (Ctxt, Dest, Pasgn);
    end Phi_Assign_Net;
 
-   procedure Phi_Assign_Static (Dest : Wire_Id; Val : Memtyp) is
+   procedure Phi_Assign_Static (Dest : Wire_Id; Val : Memtyp)
+   is
       Wire_Rec : Wire_Id_Record renames Wire_Id_Table.Table (Dest);
       pragma Assert (Wire_Rec.Kind /= Wire_None);
       Cur_Asgn : constant Seq_Assign := Wire_Rec.Cur_Assign;
@@ -1820,7 +1905,8 @@ begin
 
    Phis_Table.Append ((First => No_Seq_Assign,
                        Last => No_Seq_Assign,
-                       Nbr => 0));
+                       Nbr => 0,
+                       En => No_Wire_Id));
    pragma Assert (Phis_Table.Last = No_Phi_Id);
 
    Conc_Assign_Table.Append ((Next => No_Conc_Assign,
diff --git a/src/synth/synth-environment.ads b/src/synth/synth-environment.ads
index 5d066bf43..37ab29414 100644
--- a/src/synth/synth-environment.ads
+++ b/src/synth/synth-environment.ads
@@ -61,7 +61,9 @@ package Synth.Environment is
    type Wire_Kind is
      (
       Wire_None,
-      Wire_Signal, Wire_Variable,
+      Wire_Variable,
+      Wire_Enable,
+      Wire_Signal,
       Wire_Input, Wire_Output, Wire_Inout
      );
 
@@ -145,6 +147,13 @@ package Synth.Environment is
                          T, F : Phi_Type;
                          Stmt : Source.Syn_Src);
 
+   --  Create or get (if already created) a net that is true iff the current
+   --  phi is selected.  Used to enable sequential assertions.
+   --  Because a wire is created, inference will run on it and therefore
+   --  a dff is created if needed.
+   function Phi_Enable (Ctxt : Builders.Context_Acc; Loc : Source.Syn_Src)
+                       return Net;
+
    --  Lower level part.
    --  Currently public to handle case statements.
 
@@ -348,6 +357,8 @@ private
       Last : Seq_Assign;
       --  Number of assignments.
       Nbr : Uns32;
+      --  Enable wire created for this phi.
+      En : Wire_Id;
    end record;
 
    package Phis_Table is new Tables
diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb
index a9f39babf..10261bfa6 100644
--- a/src/synth/synth-stmts.adb
+++ b/src/synth/synth-stmts.adb
@@ -2700,10 +2700,10 @@ package body Synth.Stmts is
    procedure Synth_Dynamic_Assertion_Statement (C : Seq_Context; Stmt : Node)
    is
       Ctxt : constant Context_Acc := Get_Build (C.Inst);
-      En : constant Net := No_Net;
       Loc : constant Location_Type := Get_Location (Stmt);
       Cond : Valtyp;
       N : Net;
+      En : Net;
       Inst : Instance;
    begin
       Cond := Synth_Expression
@@ -2712,15 +2712,14 @@ package body Synth.Stmts is
          Set_Error (C.Inst);
          return;
       end if;
-      if Boolean'(False) then
-         N := Get_Net (Ctxt, Cond);
-         if En /= No_Net then
-            --  Build: En -> Cond
-            N := Build2_Imp (Ctxt, En, N, Loc);
-         end if;
-         Inst := Build_Assert (Ctxt, Synth_Label (Stmt), N);
-         Set_Location (Inst, Loc);
+      N := Get_Net (Ctxt, Cond);
+      En := Phi_Enable (Ctxt, Stmt);
+      if En /= No_Net then
+         --  Build: En -> Cond
+         N := Build2_Imp (Ctxt, En, N, Loc);
       end if;
+      Inst := Build_Assert (Ctxt, Synth_Label (Stmt), N);
+      Set_Location (Inst, Loc);
    end Synth_Dynamic_Assertion_Statement;
 
    procedure Synth_Sequential_Statements