synth: handle PSL async_abort and sync_abort. For #1654

3 files changed, 44 insertions, 10 deletions

diff --git a/src/synth/netlists-builders.adb b/src/synth/netlists-builders.adb
index f396123e6..56069f1b4 100644
--- a/src/synth/netlists-builders.adb
+++ b/src/synth/netlists-builders.adb
@@ -537,10 +537,10 @@ package body Netlists.Builders is
          Id_Iadff, 5, 1, 0);
       Outputs := (0 => Create_Output ("q"));
       Set_Ports_Desc (Ctxt.M_Iadff, (0 => Create_Input ("clk", 1),
-                                    1 => Create_Input ("d"),
-                                    2 => Create_Input ("rst"),
-                                    3 => Create_Input ("rst_val"),
-                                    4 => Create_Input ("init")),
+                                     1 => Create_Input ("d"),
+                                     2 => Create_Input ("rst"),
+                                     3 => Create_Input ("rst_val"),
+                                     4 => Create_Input ("init")),
                       Outputs);
 
       Ctxt.M_Mdff := New_User_Module
@@ -1524,7 +1524,7 @@ package body Netlists.Builders is
                          D : Net;
                          Rst : Net; Rst_Val : Net; Init : Net) return Net
    is
-      Wd : constant Width := Get_Width (D);
+      Wd : constant Width := Get_Width (Init);
       pragma Assert (Get_Width (Clk) = 1);
       Inst : Instance;
       O : Net;
@@ -1533,7 +1533,9 @@ package body Netlists.Builders is
       O := Get_Output (Inst, 0);
       Set_Width (O, Wd);
       Connect (Get_Input (Inst, 0), Clk);
-      Connect (Get_Input (Inst, 1), D);
+      if D /= No_Net then
+         Connect (Get_Input (Inst, 1), D);
+      end if;
       Connect (Get_Input (Inst, 2), Rst);
       Connect (Get_Input (Inst, 3), Rst_Val);
       Connect (Get_Input (Inst, 4), Init);
diff --git a/src/synth/netlists-builders.ads b/src/synth/netlists-builders.ads
index 86a95851f..4cec3fc72 100644
--- a/src/synth/netlists-builders.ads
+++ b/src/synth/netlists-builders.ads
@@ -196,9 +196,9 @@ package Netlists.Builders is
                         Clk : Net;
                         D : Net; Rst : Net; Rst_Val : Net) return Net;
    function Build_Iadff (Ctxt : Context_Acc;
-                        Clk : Net;
-                        D : Net; Rst : Net; Rst_Val : Net;
-                                            Init : Net) return Net;
+                         Clk : Net;
+                         D : Net; Rst : Net; Rst_Val : Net;
+                                             Init : Net) return Net;
 
    function Build_Mdff (Ctxt : Context_Acc;
                         Clk : Net;
diff --git a/src/synth/synth-vhdl_stmts.adb b/src/synth/synth-vhdl_stmts.adb
index ddf579656..9710efb4b 100644
--- a/src/synth/synth-vhdl_stmts.adb
+++ b/src/synth/synth-vhdl_stmts.adb
@@ -37,6 +37,8 @@ with Vhdl.Evaluation;
 with Vhdl.Ieee.Std_Logic_1164;
 
 with PSL.Types;
+with PSL.Nodes;
+with PSL.Subsets;
 with PSL.NFAs;
 
 with Synth.Memtype; use Synth.Memtype;
@@ -3305,8 +3307,10 @@ package body Synth.Vhdl_Stmts is
    is
       Ctxt : constant Context_Acc := Get_Build (Syn_Inst);
       Nbr_States : constant Int32 := Get_PSL_Nbr_States (Stmt);
+      Has_Async_Abort : Boolean;
       States : Net;
       Init : Net;
+      Rst  : Net;
       Clk : Net;
       Clk_Inst : Instance;
    begin
@@ -3323,14 +3327,42 @@ package body Synth.Vhdl_Stmts is
          return;
       end if;
 
+      Rst := No_Net;
+      Has_Async_Abort := False;
+      if Get_Kind (Stmt) in Iir_Kinds_Psl_Property_Directive
+        and then Get_PSL_Abort_Flag (Stmt)
+      then
+         declare
+            use PSL.Types;
+            use PSL.Subsets;
+            use PSL.Nodes;
+            Abort_Prop : constant PSL_Node := Get_Psl_Property (Stmt);
+         begin
+            Rst := Synth_PSL_Expression (Syn_Inst, Get_Boolean (Abort_Prop));
+            Has_Async_Abort := Is_Async_Abort (Abort_Prop);
+         end;
+      end if;
+
       --  build idff
-      States := Build_Idff (Ctxt, Clk, No_Net, Init);
+      if Rst /= No_Net and then Has_Async_Abort then
+         --  In case of async_abort.
+         States := Build_Iadff (Ctxt, Clk, No_Net, Rst, Init, Init);
+      else
+         States := Build_Idff (Ctxt, Clk, No_Net, Init);
+      end if;
       Set_Location (States, Stmt);
 
       --  create update nets
       --  For each state: if set, evaluate all outgoing edges.
       Next_States :=
         Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States, Stmt);
+
+      --  Handle sync_abort.
+      if Rst /= No_Net and then not Has_Async_Abort then
+         Next_States := Build_Mux2 (Ctxt, Rst, Next_States, Init);
+         Set_Location (Next_States, Stmt);
+      end if;
+
       Connect (Get_Input (Get_Net_Parent (States), 1), Next_States);
    end Synth_Psl_Dff;