simul: handle PSL aborts

3 files changed, 71 insertions, 0 deletions

diff --git a/src/simul/simul-vhdl_elab.adb b/src/simul/simul-vhdl_elab.adb
index 03bd3f863..0ff4d2446 100644
--- a/src/simul/simul-vhdl_elab.adb
+++ b/src/simul/simul-vhdl_elab.adb
@@ -21,6 +21,11 @@ with Areapools;
 with Vhdl.Errors; use Vhdl.Errors;
 with Vhdl.Utils; use Vhdl.Utils;
 with Vhdl.Canon;
+with Vhdl.Canon_PSL;
+
+with PSL.Nodes;
+with PSL.Subsets;
+with PSL.Types;
 
 with Synth.Vhdl_Stmts;
 with Synth.Vhdl_Decls;
@@ -621,6 +626,23 @@ package body Simul.Vhdl_Elab is
             | Iir_Kind_Psl_Cover_Directive =>
             List := Get_PSL_Clock_Sensitivity (Proc);
             Gather_Sensitivity (Inst, Proc_Idx, List);
+            if Get_Kind (Proc) in Iir_Kinds_Psl_Property_Directive
+              and then Get_PSL_Abort_Flag (Proc)
+            then
+               declare
+                  use PSL.Types;
+                  use PSL.Nodes;
+                  Prop : constant PSL_Node := Get_Psl_Property (Proc);
+               begin
+                  if PSL.Subsets.Is_Async_Abort (Prop) then
+                     List := Create_Iir_List;
+                     Vhdl.Canon_PSL.Canon_Extract_Sensitivity
+                       (Get_Boolean (Prop), List);
+                     Gather_Sensitivity (Inst, Proc_Idx, List);
+                     Destroy_Iir_List (List);
+                  end if;
+               end;
+            end if;
             return;
          when Iir_Kind_Concurrent_Break_Statement =>
             List := Get_Sensitivity_List (Proc);
diff --git a/src/simul/simul-vhdl_simul.adb b/src/simul/simul-vhdl_simul.adb
index cc68914ea..14f50fad7 100644
--- a/src/simul/simul-vhdl_simul.adb
+++ b/src/simul/simul-vhdl_simul.adb
@@ -35,6 +35,7 @@ with PSL.Nodes;
 with PSL.NFAs;
 with PSL.NFAs.Utils;
 with PSL.Errors;
+with PSL.Subsets;
 
 with Elab.Debugger;
 with Elab.Vhdl_Objtypes; use Elab.Vhdl_Objtypes;
@@ -2028,11 +2029,34 @@ package body Simul.Vhdl_Simul is
       end case;
    end Execute_Psl_Expr;
 
+   --  Execute the boolean condition of PROP.
+   function Execute_Psl_Abort_Condition (Inst : Synth_Instance_Acc;
+                                         Prop : PSL_Node) return Boolean
+   is
+      Marker : Mark_Type;
+      V : Boolean;
+   begin
+      Mark_Expr_Pool (Marker);
+      V := Execute_Psl_Expr (Inst, PSL.Nodes.Get_Boolean (Prop), False);
+      Release_Expr_Pool (Marker);
+      return V;
+   end Execute_Psl_Abort_Condition;
+
+   procedure Reset_PSL_State (E : Process_State_Acc) is
+   begin
+      E.States.all := (others => False);
+      E.States (0) := True;
+   end Reset_PSL_State;
+
    procedure PSL_Process_Executer (Self : Grt.Processes.Instance_Acc)
    is
       use PSL.NFAs;
 
       E : constant Process_State_Acc := To_Process_State_Acc (Self);
+      Has_Abort : constant Boolean :=
+        Get_Kind (E.Proc) in Iir_Kinds_Psl_Property_Directive
+        and then Get_PSL_Abort_Flag (E.Proc);
+      Prop : PSL_Node;
       Nvec : Boolean_Vector (E.States.all'Range);
       Marker : Mark_Type;
       V : Boolean;
@@ -2052,10 +2076,31 @@ package body Simul.Vhdl_Simul is
       Instance_Pool := Process_Pool'Access;
 --      Current_Process := No_Process;
 
+      if Has_Abort then
+         Prop := Get_Psl_Property (E.Proc);
+         if PSL.Subsets.Is_Async_Abort (Prop) then
+            if Execute_Psl_Abort_Condition (E.Instance, Prop) then
+               Reset_PSL_State (E);
+
+               Instance_Pool := null;
+               return;
+            end if;
+         end if;
+      end if;
+
       Mark_Expr_Pool (Marker);
       V := Execute_Psl_Expr (E.Instance, Get_PSL_Clock (E.Proc), False);
       Release_Expr_Pool (Marker);
       if V then
+         if Has_Abort and then not PSL.Subsets.Is_Async_Abort (Prop) then
+            if Execute_Psl_Abort_Condition (E.Instance, Prop) then
+               Reset_PSL_State (E);
+
+               Instance_Pool := null;
+               return;
+            end if;
+         end if;
+
          Nvec := (others => False);
          case Get_Kind (E.Proc) is
             when Iir_Kind_Psl_Cover_Directive
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index 469dc6c20..7dcec16a3 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -389,9 +389,13 @@ package body Trans.Chap9 is
    begin
       Start_Declare_Stmt;
       New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
+
+      --  Set true to the first state.
       New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
                                             New_Lit (Ghdl_Index_0)),
                        New_Lit (Std_Boolean_True_Node));
+
+      --  Set flase to the other states.
       New_Assign_Stmt (New_Obj (Var_I), New_Lit (Ghdl_Index_1));
       Start_Loop_Stmt (Label);
       Gen_Exit_When