Add support for PSL assumptions, used in formal verification (#880)

* vhdl: make the parser understand PSL assume

* assume does not actually have report according to the spec. Just a property.

* add SPL assume to semantic analysis

* canonicalise PSL assume

* add assume to annotations

* add PSL assume to simulation code

* statement -> directive

* add assume to translation files

* update ticked24 testcase

* correctly parse assume

* add assume testcase

* refactor chunk of duplicated code

23 files changed, 293 insertions, 141 deletions

diff --git a/src/vhdl/simulate/simul-elaboration.adb b/src/vhdl/simulate/simul-elaboration.adb
index 61048392b..f165662c2 100644
--- a/src/vhdl/simulate/simul-elaboration.adb
+++ b/src/vhdl/simulate/simul-elaboration.adb
@@ -1897,7 +1897,8 @@ package body Simul.Elaboration is
                null;
 
             when Iir_Kind_Psl_Cover_Directive
-              | Iir_Kind_Psl_Assert_Statement
+              | Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Endpoint_Declaration =>
                Elaborate_Psl_Directive (Instance, Stmt);
 
diff --git a/src/vhdl/simulate/simul-simulation-main.adb b/src/vhdl/simulate/simul-simulation-main.adb
index 5af8acb55..d6c6ba0ff 100644
--- a/src/vhdl/simulate/simul-simulation-main.adb
+++ b/src/vhdl/simulate/simul-simulation-main.adb
@@ -477,12 +477,18 @@ package body Simul.Simulation.Main is
          S_Num := Get_State_Label (S);
          pragma Assert (S_Num = Get_PSL_Nbr_States (E.Stmt) - 1);
          case Get_Kind (E.Stmt) is
-            when Iir_Kind_Psl_Assert_Statement =>
+            when Iir_Kind_Psl_Assume_Directive =>
                if Nvec (S_Num) then
                   Execute_Failed_Assertion
                     (E.Instance, "psl assertion", E.Stmt,
                      "assertion violation", 2);
                end if;
+            when Iir_Kind_Psl_Assume_Directive =>
+               if Nvec (S_Num) then
+                  Execute_Failed_Assertion
+                    (E.Instance, "psl assumption", E.Stmt,
+                     "assumption violation", 2);
+               end if;
             when Iir_Kind_Psl_Cover_Directive =>
                if Nvec (S_Num) then
                   if Get_Report_Expression (E.Stmt) /= Null_Iir then
@@ -563,7 +569,8 @@ package body Simul.Simulation.Main is
               (E.Instance, Get_PSL_Clock_Sensitivity (E.Stmt));
 
             case Get_Kind (E.Stmt) is
-               when Iir_Kind_Psl_Assert_Statement =>
+               when Iir_Kind_Psl_Assert_Directive
+                  | Iir_Kind_Psl_Assume_Directive =>
                   if Get_PSL_EOS_Flag (E.Stmt) then
                      Grt.Processes.Ghdl_Finalize_Register
                        (To_Instance_Acc (E'Address),
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index b70a673a5..7a2033624 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -644,9 +644,12 @@ package body Trans.Chap9 is
          Start_If_Stmt (S_Blk, Cond);
          Open_Temp;
          case Get_Kind (Stmt) is
-            when Iir_Kind_Psl_Assert_Statement =>
+            when Iir_Kind_Psl_Assert_Directive =>
                Chap8.Translate_Report
                  (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+            when Iir_Kind_Psl_Assume_Directive =>
+               Chap8.Translate_Report
+                 (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error);
             when Iir_Kind_Psl_Cover_Directive =>
                if Get_Report_Expression (Stmt) /= Null_Iir then
                   Start_Association (Assocs, Report_Proc);
@@ -697,7 +700,8 @@ package body Trans.Chap9 is
 
       --  The finalizer.
       case Get_Kind (Stmt) is
-         when Iir_Kind_Psl_Assert_Statement =>
+         when Iir_Kind_Psl_Assert_Directive
+            | Iir_Kind_Psl_Assume_Directive =>
             if Get_PSL_EOS_Flag (Stmt) then
                Create_Psl_Final_Proc (Stmt, Base, Instance);
 
@@ -724,8 +728,13 @@ package body Trans.Chap9 is
                        (ON_And, Cond,
                         Translate_Psl_Expr (Get_Edge_Expr (E), True));
                      Start_If_Stmt (E_Blk, Cond);
-                     Chap8.Translate_Report
-                       (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+                     if Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive then
+                        Chap8.Translate_Report
+                          (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+                     else
+                        Chap8.Translate_Report
+                          (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error);
+                     end if;
                      New_Return_Stmt;
                      Finish_If_Stmt (E_Blk);
 
@@ -974,7 +983,8 @@ package body Trans.Chap9 is
                null;
             when Iir_Kind_Psl_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement
+            when Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Cover_Directive
               | Iir_Kind_Psl_Endpoint_Declaration =>
                Translate_Psl_Directive_Declarations (El);
@@ -1122,7 +1132,8 @@ package body Trans.Chap9 is
                null;
             when Iir_Kind_Psl_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement
+            when Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Cover_Directive
               | Iir_Kind_Psl_Endpoint_Declaration =>
                Translate_Psl_Directive_Statement (Stmt, Base_Info);
@@ -2721,7 +2732,8 @@ package body Trans.Chap9 is
             when Iir_Kind_Psl_Declaration
               | Iir_Kind_Psl_Endpoint_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement
+            when Iir_Kind_Psl_Assert_Directive
+               | Iir_Kind_Psl_Assume_Directive
                | Iir_Kind_Psl_Cover_Directive =>
                null;
             when Iir_Kind_Component_Instantiation_Statement =>
@@ -2783,7 +2795,8 @@ package body Trans.Chap9 is
                null;
             when Iir_Kind_Psl_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement
+            when Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Cover_Directive
               | Iir_Kind_Psl_Endpoint_Declaration =>
                Elab_Psl_Directive (Stmt, Base_Info);
diff --git a/src/vhdl/translate/trans-rtis.adb b/src/vhdl/translate/trans-rtis.adb
index 96aacb8b0..e618aeb9b 100644
--- a/src/vhdl/translate/trans-rtis.adb
+++ b/src/vhdl/translate/trans-rtis.adb
@@ -322,6 +322,9 @@ package body Trans.Rtis is
            (Constr, Get_Identifier ("__ghdl_rtik_psl_assert"),
             Ghdl_Rtik_Psl_Assert);
          New_Enum_Literal
+           (Constr, Get_Identifier ("__ghdl_rtik_psl_assume"),
+            Ghdl_Rtik_Psl_Assume);
+         New_Enum_Literal
            (Constr, Get_Identifier ("__ghdl_rtik_psl_cover"),
             Ghdl_Rtik_Psl_Cover);
          New_Enum_Literal
@@ -2042,8 +2045,10 @@ package body Trans.Rtis is
       case Get_Kind (Decl) is
          when Iir_Kind_Psl_Cover_Directive =>
             Kind := Ghdl_Rtik_Psl_Cover;
-         when Iir_Kind_Psl_Assert_Statement =>
+         when Iir_Kind_Psl_Assert_Directive =>
             Kind := Ghdl_Rtik_Psl_Assert;
+         when Iir_Kind_Psl_Assume_Directive =>
+            Kind := Ghdl_Rtik_Psl_Assume;
          when Iir_Kind_Psl_Endpoint_Declaration =>
             Kind := Ghdl_Rtik_Psl_Endpoint;
          when others =>
@@ -2422,7 +2427,8 @@ package body Trans.Rtis is
                null;
             when Iir_Kind_Psl_Declaration =>
                null;
-            when Iir_Kind_Psl_Assert_Statement
+            when Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Cover_Directive
               | Iir_Kind_Psl_Endpoint_Declaration =>
                Generate_Psl_Directive (Stmt);
@@ -2994,7 +3000,8 @@ package body Trans.Rtis is
          when Iir_Kind_Process_Statement
             | Iir_Kind_Sensitized_Process_Statement =>
             return Node_Info.Process_Rti_Const;
-         when Iir_Kind_Psl_Assert_Statement
+         when Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Endpoint_Declaration =>
             return Node_Info.Psl_Rti_Const;
@@ -3035,7 +3042,8 @@ package body Trans.Rtis is
          when Iir_Kind_Process_Statement
             | Iir_Kind_Sensitized_Process_Statement =>
             Ref := Get_Instance_Ref (Node_Info.Process_Scope);
-         when Iir_Kind_Psl_Assert_Statement
+         when Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Endpoint_Declaration =>
             Ref := Get_Instance_Ref (Node_Info.Psl_Scope);
diff --git a/src/vhdl/translate/trans-rtis.ads b/src/vhdl/translate/trans-rtis.ads
index e3c8c188e..1e4dd36ef 100644
--- a/src/vhdl/translate/trans-rtis.ads
+++ b/src/vhdl/translate/trans-rtis.ads
@@ -70,6 +70,7 @@ package Trans.Rtis is
    Ghdl_Rtik_Attribute_Quiet             : O_Cnode;
    Ghdl_Rtik_Attribute_Stable            : O_Cnode;
    Ghdl_Rtik_Psl_Assert                  : O_Cnode;
+   Ghdl_Rtik_Psl_Assume                  : O_Cnode;
    Ghdl_Rtik_Psl_Cover                   : O_Cnode;
    Ghdl_Rtik_Psl_Endpoint                : O_Cnode;
    Ghdl_Rtik_Error                       : O_Cnode;
diff --git a/src/vhdl/translate/trans_decls.ads b/src/vhdl/translate/trans_decls.ads
index 38d3be7e7..d76b1b896 100644
--- a/src/vhdl/translate/trans_decls.ads
+++ b/src/vhdl/translate/trans_decls.ads
@@ -25,6 +25,7 @@ package Trans_Decls is
 
    Ghdl_Check_Stack_Allocation : O_Dnode;
 
+   Ghdl_Psl_Assume_Failed : O_Dnode;
    Ghdl_Psl_Cover : O_Dnode;
    Ghdl_Psl_Cover_Failed : O_Dnode;
    --  Procedure for report statement.
diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb
index de83ba132..863acd37d 100644
--- a/src/vhdl/translate/translation.adb
+++ b/src/vhdl/translate/translation.adb
@@ -1077,6 +1077,8 @@ package body Translation is
            ("__ghdl_ieee_assert_failed", Ghdl_Ieee_Assert_Failed);
          Create_Report_Subprg ("__ghdl_psl_assert_failed",
                                Ghdl_Psl_Assert_Failed);
+         Create_Report_Subprg ("__ghdl_psl_assume_failed",
+                               Ghdl_Psl_Assume_Failed);
          Create_Report_Subprg ("__ghdl_psl_cover", Ghdl_Psl_Cover);
          Create_Report_Subprg ("__ghdl_psl_cover_failed",
                                Ghdl_Psl_Cover_Failed);
diff --git a/src/vhdl/vhdl-annotations.adb b/src/vhdl/vhdl-annotations.adb
index cb44f98f0..7e2d19a58 100644
--- a/src/vhdl/vhdl-annotations.adb
+++ b/src/vhdl/vhdl-annotations.adb
@@ -1083,7 +1083,8 @@ package body Vhdl.Annotations is
                null;
 
             when Iir_Kind_Psl_Cover_Directive
-              | Iir_Kind_Psl_Assert_Statement
+              | Iir_Kind_Psl_Assert_Directive
+              | Iir_Kind_Psl_Assume_Directive
               | Iir_Kind_Psl_Restrict_Directive =>
                null;
             when Iir_Kind_Psl_Endpoint_Declaration =>
diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb
index 4dbb03c4c..6dd40560b 100644
--- a/src/vhdl/vhdl-canon.adb
+++ b/src/vhdl/vhdl-canon.adb
@@ -2125,7 +2125,8 @@ package body Vhdl.Canon is
                     (Top, Get_Generate_Statement_Body (El));
                end;
 
-            when Iir_Kind_Psl_Assert_Statement =>
+            when Iir_Kind_Psl_Assert_Directive
+               | Iir_Kind_Psl_Assume_Directive=>
                declare
                   Prop : PSL_Node;
                   Fa : PSL_NFA;
diff --git a/src/vhdl/vhdl-elocations.adb b/src/vhdl/vhdl-elocations.adb
index c4dd2f1b6..6965457d6 100644
--- a/src/vhdl/vhdl-elocations.adb
+++ b/src/vhdl/vhdl-elocations.adb
@@ -342,7 +342,8 @@ package body Vhdl.Elocations is
            | Iir_Kind_Psl_Expression
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Case_Generate_Statement
diff --git a/src/vhdl/vhdl-elocations.ads b/src/vhdl/vhdl-elocations.ads
index 286ba751c..84be78e93 100644
--- a/src/vhdl/vhdl-elocations.ads
+++ b/src/vhdl/vhdl-elocations.ads
@@ -404,7 +404,8 @@ package Vhdl.Elocations is
 
    -- Iir_Kind_Psl_Default_Clock (None)
 
-   -- Iir_Kind_Psl_Assert_Statement (None)
+   -- Iir_Kind_Psl_Assert_Directive (None)
+   -- Iir_Kind_Psl_Assume_Directive (None)
    -- Iir_Kind_Psl_Cover_Directive (None)
    -- Iir_Kind_Psl_Restrict_Directive (None)
 
diff --git a/src/vhdl/vhdl-errors.adb b/src/vhdl/vhdl-errors.adb
index 57be65311..ada8258af 100644
--- a/src/vhdl/vhdl-errors.adb
+++ b/src/vhdl/vhdl-errors.adb
@@ -687,8 +687,10 @@ package body Vhdl.Errors is
               (Node, "concurrent selected signal assignment");
          when Iir_Kind_Concurrent_Assertion_Statement =>
             return Disp_Label (Node, "concurrent assertion");
-         when Iir_Kind_Psl_Assert_Statement =>
+         when Iir_Kind_Psl_Assert_Directive =>
             return Disp_Label (Node, "PSL assertion");
+         when Iir_Kind_Psl_Assume_Directive =>
+            return Disp_Label (Node, "PSL assumption");
          when Iir_Kind_Psl_Cover_Directive =>
             return Disp_Label (Node, "PSL cover");
          when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-nodes.adb b/src/vhdl/vhdl-nodes.adb
index dfb9629af..780f13b5b 100644
--- a/src/vhdl/vhdl-nodes.adb
+++ b/src/vhdl/vhdl-nodes.adb
@@ -1235,7 +1235,8 @@ package body Vhdl.Nodes is
            | Iir_Kind_Concurrent_Simple_Signal_Assignment
            | Iir_Kind_Concurrent_Conditional_Signal_Assignment
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
diff --git a/src/vhdl/vhdl-nodes.ads b/src/vhdl/vhdl-nodes.ads
index a884f7b9d..58dce712a 100644
--- a/src/vhdl/vhdl-nodes.ads
+++ b/src/vhdl/vhdl-nodes.ads
@@ -2902,12 +2902,16 @@ package Vhdl.Nodes is
    --   Get/Set_Label (Field3)
    --   Get/Set_Identifier (Alias Field3)
 
-   -- Iir_Kind_Psl_Assert_Statement (Medium)
+   -- Iir_Kind_Psl_Assert_Directive (Medium)
+   -- Iir_Kind_Psl_Assume_Directive (Medium)
    -- Iir_Kind_Psl_Cover_Directive (Medium)
    --
    --   Get/Set_Parent (Field0)
    --
-   -- Only for Iir_Kind_Psl_Assert_Statement:
+   -- Only for Iir_Kind_Psl_Assert_Directive:
+   --   Get/Set_Psl_Property (Field1)
+   --
+   -- Only for Iir_Kind_Psl_Assume_Directive:
    --   Get/Set_Psl_Property (Field1)
    --
    -- Only for Iir_Kind_Psl_Cover_Directive:
@@ -4377,7 +4381,8 @@ package Vhdl.Nodes is
       Iir_Kind_Concurrent_Selected_Signal_Assignment,
       Iir_Kind_Concurrent_Assertion_Statement,
       Iir_Kind_Concurrent_Procedure_Call_Statement,
-      Iir_Kind_Psl_Assert_Statement,
+      Iir_Kind_Psl_Assert_Directive,
+      Iir_Kind_Psl_Assume_Directive,
       Iir_Kind_Psl_Cover_Directive,
       Iir_Kind_Psl_Restrict_Directive,
       Iir_Kind_Block_Statement,
@@ -5569,7 +5574,8 @@ package Vhdl.Nodes is
    --Iir_Kind_Concurrent_Selected_Signal_Assignment
    --Iir_Kind_Concurrent_Assertion_Statement
    --Iir_Kind_Concurrent_Procedure_Call_Statement
-   --Iir_Kind_Psl_Assert_Statement
+   --Iir_Kind_Psl_Assert_Directive
+   --Iir_Kind_Psl_Assume_Directive
    --Iir_Kind_Psl_Cover_Directive
    --Iir_Kind_Psl_Restrict_Directive
    --Iir_Kind_Block_Statement
@@ -5587,7 +5593,8 @@ package Vhdl.Nodes is
    --Iir_Kind_Concurrent_Selected_Signal_Assignment
    --Iir_Kind_Concurrent_Assertion_Statement
    --Iir_Kind_Concurrent_Procedure_Call_Statement
-   --Iir_Kind_Psl_Assert_Statement
+   --Iir_Kind_Psl_Assert_Directive
+   --Iir_Kind_Psl_Assume_Directive
    --Iir_Kind_Psl_Cover_Directive
      Iir_Kind_Psl_Restrict_Directive;
 
diff --git a/src/vhdl/vhdl-nodes_meta.adb b/src/vhdl/vhdl-nodes_meta.adb
index 2e3512028..4b4c6b632 100644
--- a/src/vhdl/vhdl-nodes_meta.adb
+++ b/src/vhdl/vhdl-nodes_meta.adb
@@ -1388,8 +1388,10 @@ package body Vhdl.Nodes_Meta is
             return "concurrent_assertion_statement";
          when Iir_Kind_Concurrent_Procedure_Call_Statement =>
             return "concurrent_procedure_call_statement";
-         when Iir_Kind_Psl_Assert_Statement =>
+         when Iir_Kind_Psl_Assert_Directive =>
             return "psl_assert_statement";
+         when Iir_Kind_Psl_Assume_Directive =>
+            return "psl_assume_statement";
          when Iir_Kind_Psl_Cover_Directive =>
             return "psl_cover_directive";
          when Iir_Kind_Psl_Restrict_Directive =>
@@ -3795,7 +3797,21 @@ package body Vhdl.Nodes_Meta is
       Field_Parent,
       Field_Procedure_Call,
       Field_Chain,
-      --  Iir_Kind_Psl_Assert_Statement
+      --  Iir_Kind_Psl_Assert_Directive
+      Field_Psl_Property,
+      Field_Label,
+      Field_PSL_Clock,
+      Field_PSL_NFA,
+      Field_PSL_Nbr_States,
+      Field_PSL_EOS_Flag,
+      Field_Postponed_Flag,
+      Field_Visible_Flag,
+      Field_Parent,
+      Field_Chain,
+      Field_Severity_Expression,
+      Field_Report_Expression,
+      Field_PSL_Clock_Sensitivity,
+      --  Iir_Kind_Psl_Assume_Directive
       Field_Psl_Property,
       Field_Label,
       Field_PSL_Clock,
@@ -4640,91 +4656,92 @@ package body Vhdl.Nodes_Meta is
       Iir_Kind_Concurrent_Selected_Signal_Assignment => 1370,
       Iir_Kind_Concurrent_Assertion_Statement => 1378,
       Iir_Kind_Concurrent_Procedure_Call_Statement => 1385,
-      Iir_Kind_Psl_Assert_Statement => 1398,
-      Iir_Kind_Psl_Cover_Directive => 1411,
-      Iir_Kind_Psl_Restrict_Directive => 1422,
-      Iir_Kind_Block_Statement => 1436,
-      Iir_Kind_If_Generate_Statement => 1447,
-      Iir_Kind_Case_Generate_Statement => 1456,
-      Iir_Kind_For_Generate_Statement => 1465,
-      Iir_Kind_Component_Instantiation_Statement => 1476,
-      Iir_Kind_Psl_Default_Clock => 1480,
-      Iir_Kind_Simple_Simultaneous_Statement => 1487,
-      Iir_Kind_Generate_Statement_Body => 1498,
-      Iir_Kind_If_Generate_Else_Clause => 1504,
-      Iir_Kind_Simple_Signal_Assignment_Statement => 1514,
-      Iir_Kind_Conditional_Signal_Assignment_Statement => 1524,
-      Iir_Kind_Selected_Waveform_Assignment_Statement => 1535,
-      Iir_Kind_Null_Statement => 1539,
-      Iir_Kind_Assertion_Statement => 1546,
-      Iir_Kind_Report_Statement => 1552,
-      Iir_Kind_Wait_Statement => 1560,
-      Iir_Kind_Variable_Assignment_Statement => 1567,
-      Iir_Kind_Conditional_Variable_Assignment_Statement => 1574,
-      Iir_Kind_Return_Statement => 1580,
-      Iir_Kind_For_Loop_Statement => 1589,
-      Iir_Kind_While_Loop_Statement => 1598,
-      Iir_Kind_Next_Statement => 1605,
-      Iir_Kind_Exit_Statement => 1612,
-      Iir_Kind_Case_Statement => 1620,
-      Iir_Kind_Procedure_Call_Statement => 1626,
-      Iir_Kind_If_Statement => 1636,
-      Iir_Kind_Elsif => 1642,
-      Iir_Kind_Character_Literal => 1650,
-      Iir_Kind_Simple_Name => 1658,
-      Iir_Kind_Selected_Name => 1667,
-      Iir_Kind_Operator_Symbol => 1673,
-      Iir_Kind_Reference_Name => 1677,
-      Iir_Kind_External_Constant_Name => 1685,
-      Iir_Kind_External_Signal_Name => 1693,
-      Iir_Kind_External_Variable_Name => 1702,
-      Iir_Kind_Selected_By_All_Name => 1708,
-      Iir_Kind_Parenthesis_Name => 1713,
-      Iir_Kind_Package_Pathname => 1717,
-      Iir_Kind_Absolute_Pathname => 1718,
-      Iir_Kind_Relative_Pathname => 1719,
-      Iir_Kind_Pathname_Element => 1724,
-      Iir_Kind_Base_Attribute => 1726,
-      Iir_Kind_Subtype_Attribute => 1731,
-      Iir_Kind_Element_Attribute => 1736,
-      Iir_Kind_Left_Type_Attribute => 1741,
-      Iir_Kind_Right_Type_Attribute => 1746,
-      Iir_Kind_High_Type_Attribute => 1751,
-      Iir_Kind_Low_Type_Attribute => 1756,
-      Iir_Kind_Ascending_Type_Attribute => 1761,
-      Iir_Kind_Image_Attribute => 1767,
-      Iir_Kind_Value_Attribute => 1773,
-      Iir_Kind_Pos_Attribute => 1779,
-      Iir_Kind_Val_Attribute => 1785,
-      Iir_Kind_Succ_Attribute => 1791,
-      Iir_Kind_Pred_Attribute => 1797,
-      Iir_Kind_Leftof_Attribute => 1803,
-      Iir_Kind_Rightof_Attribute => 1809,
-      Iir_Kind_Delayed_Attribute => 1818,
-      Iir_Kind_Stable_Attribute => 1827,
-      Iir_Kind_Quiet_Attribute => 1836,
-      Iir_Kind_Transaction_Attribute => 1845,
-      Iir_Kind_Event_Attribute => 1849,
-      Iir_Kind_Active_Attribute => 1853,
-      Iir_Kind_Last_Event_Attribute => 1857,
-      Iir_Kind_Last_Active_Attribute => 1861,
-      Iir_Kind_Last_Value_Attribute => 1865,
-      Iir_Kind_Driving_Attribute => 1869,
-      Iir_Kind_Driving_Value_Attribute => 1873,
-      Iir_Kind_Behavior_Attribute => 1873,
-      Iir_Kind_Structure_Attribute => 1873,
-      Iir_Kind_Simple_Name_Attribute => 1880,
-      Iir_Kind_Instance_Name_Attribute => 1885,
-      Iir_Kind_Path_Name_Attribute => 1890,
-      Iir_Kind_Left_Array_Attribute => 1897,
-      Iir_Kind_Right_Array_Attribute => 1904,
-      Iir_Kind_High_Array_Attribute => 1911,
-      Iir_Kind_Low_Array_Attribute => 1918,
-      Iir_Kind_Length_Array_Attribute => 1925,
-      Iir_Kind_Ascending_Array_Attribute => 1932,
-      Iir_Kind_Range_Array_Attribute => 1939,
-      Iir_Kind_Reverse_Range_Array_Attribute => 1946,
-      Iir_Kind_Attribute_Name => 1955
+      Iir_Kind_Psl_Assert_Directive => 1398,
+      Iir_Kind_Psl_Assume_Directive => 1411,
+      Iir_Kind_Psl_Cover_Directive => 1424,
+      Iir_Kind_Psl_Restrict_Directive => 1435,
+      Iir_Kind_Block_Statement => 1449,
+      Iir_Kind_If_Generate_Statement => 1460,
+      Iir_Kind_Case_Generate_Statement => 1469,
+      Iir_Kind_For_Generate_Statement => 1478,
+      Iir_Kind_Component_Instantiation_Statement => 1489,
+      Iir_Kind_Psl_Default_Clock => 1493,
+      Iir_Kind_Simple_Simultaneous_Statement => 1500,
+      Iir_Kind_Generate_Statement_Body => 1511,
+      Iir_Kind_If_Generate_Else_Clause => 1517,
+      Iir_Kind_Simple_Signal_Assignment_Statement => 1527,
+      Iir_Kind_Conditional_Signal_Assignment_Statement => 1537,
+      Iir_Kind_Selected_Waveform_Assignment_Statement => 1548,
+      Iir_Kind_Null_Statement => 1552,
+      Iir_Kind_Assertion_Statement => 1559,
+      Iir_Kind_Report_Statement => 1565,
+      Iir_Kind_Wait_Statement => 1573,
+      Iir_Kind_Variable_Assignment_Statement => 1580,
+      Iir_Kind_Conditional_Variable_Assignment_Statement => 1587,
+      Iir_Kind_Return_Statement => 1593,
+      Iir_Kind_For_Loop_Statement => 1602,
+      Iir_Kind_While_Loop_Statement => 1611,
+      Iir_Kind_Next_Statement => 1618,
+      Iir_Kind_Exit_Statement => 1625,
+      Iir_Kind_Case_Statement => 1633,
+      Iir_Kind_Procedure_Call_Statement => 1639,
+      Iir_Kind_If_Statement => 1649,
+      Iir_Kind_Elsif => 1655,
+      Iir_Kind_Character_Literal => 1663,
+      Iir_Kind_Simple_Name => 1671,
+      Iir_Kind_Selected_Name => 1680,
+      Iir_Kind_Operator_Symbol => 1686,
+      Iir_Kind_Reference_Name => 1690,
+      Iir_Kind_External_Constant_Name => 1698,
+      Iir_Kind_External_Signal_Name => 1706,
+      Iir_Kind_External_Variable_Name => 1715,
+      Iir_Kind_Selected_By_All_Name => 1721,
+      Iir_Kind_Parenthesis_Name => 1726,
+      Iir_Kind_Package_Pathname => 1730,
+      Iir_Kind_Absolute_Pathname => 1731,
+      Iir_Kind_Relative_Pathname => 1732,
+      Iir_Kind_Pathname_Element => 1737,
+      Iir_Kind_Base_Attribute => 1739,
+      Iir_Kind_Subtype_Attribute => 1744,
+      Iir_Kind_Element_Attribute => 1749,
+      Iir_Kind_Left_Type_Attribute => 1754,
+      Iir_Kind_Right_Type_Attribute => 1759,
+      Iir_Kind_High_Type_Attribute => 1764,
+      Iir_Kind_Low_Type_Attribute => 1769,
+      Iir_Kind_Ascending_Type_Attribute => 1774,
+      Iir_Kind_Image_Attribute => 1780,
+      Iir_Kind_Value_Attribute => 1786,
+      Iir_Kind_Pos_Attribute => 1792,
+      Iir_Kind_Val_Attribute => 1798,
+      Iir_Kind_Succ_Attribute => 1804,
+      Iir_Kind_Pred_Attribute => 1810,
+      Iir_Kind_Leftof_Attribute => 1816,
+      Iir_Kind_Rightof_Attribute => 1822,
+      Iir_Kind_Delayed_Attribute => 1831,
+      Iir_Kind_Stable_Attribute => 1840,
+      Iir_Kind_Quiet_Attribute => 1849,
+      Iir_Kind_Transaction_Attribute => 1858,
+      Iir_Kind_Event_Attribute => 1862,
+      Iir_Kind_Active_Attribute => 1866,
+      Iir_Kind_Last_Event_Attribute => 1870,
+      Iir_Kind_Last_Active_Attribute => 1874,
+      Iir_Kind_Last_Value_Attribute => 1878,
+      Iir_Kind_Driving_Attribute => 1882,
+      Iir_Kind_Driving_Value_Attribute => 1886,
+      Iir_Kind_Behavior_Attribute => 1886,
+      Iir_Kind_Structure_Attribute => 1886,
+      Iir_Kind_Simple_Name_Attribute => 1893,
+      Iir_Kind_Instance_Name_Attribute => 1898,
+      Iir_Kind_Path_Name_Attribute => 1903,
+      Iir_Kind_Left_Array_Attribute => 1910,
+      Iir_Kind_Right_Array_Attribute => 1917,
+      Iir_Kind_High_Array_Attribute => 1924,
+      Iir_Kind_Low_Array_Attribute => 1931,
+      Iir_Kind_Length_Array_Attribute => 1938,
+      Iir_Kind_Ascending_Array_Attribute => 1945,
+      Iir_Kind_Range_Array_Attribute => 1952,
+      Iir_Kind_Reverse_Range_Array_Attribute => 1959,
+      Iir_Kind_Attribute_Name => 1968
      );
 
    function Get_Fields_First (K : Iir_Kind) return Fields_Index is
@@ -7393,7 +7410,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
@@ -8172,7 +8190,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
@@ -8223,7 +8242,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
@@ -8309,7 +8329,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
@@ -8777,7 +8798,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
@@ -9035,7 +9057,8 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Concurrent_Assertion_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Assertion_Statement
            | Iir_Kind_Report_Statement =>
@@ -9049,7 +9072,8 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Concurrent_Assertion_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Assertion_Statement
            | Iir_Kind_Report_Statement =>
@@ -9393,7 +9417,8 @@ package body Vhdl.Nodes_Meta is
            | Iir_Kind_Concurrent_Selected_Signal_Assignment
            | Iir_Kind_Concurrent_Assertion_Statement
            | Iir_Kind_Concurrent_Procedure_Call_Statement
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive
            | Iir_Kind_Block_Statement
@@ -10759,7 +10784,13 @@ package body Vhdl.Nodes_Meta is
 
    function Has_Psl_Property (K : Iir_Kind) return Boolean is
    begin
-      return K = Iir_Kind_Psl_Assert_Statement;
+      case K is
+         when Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive =>
+            return True;
+         when others =>
+            return False;
+      end case;
    end Has_Psl_Property;
 
    function Has_Psl_Sequence (K : Iir_Kind) return Boolean is
@@ -10799,7 +10830,8 @@ package body Vhdl.Nodes_Meta is
       case K is
          when Iir_Kind_Psl_Declaration
            | Iir_Kind_Psl_Endpoint_Declaration
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
@@ -10813,7 +10845,8 @@ package body Vhdl.Nodes_Meta is
       case K is
          when Iir_Kind_Psl_Declaration
            | Iir_Kind_Psl_Endpoint_Declaration
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
@@ -10826,7 +10859,8 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Psl_Endpoint_Declaration
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
@@ -10839,7 +10873,8 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Psl_Endpoint_Declaration
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
@@ -10852,7 +10887,8 @@ package body Vhdl.Nodes_Meta is
    begin
       case K is
          when Iir_Kind_Psl_Endpoint_Declaration
-           | Iir_Kind_Psl_Assert_Statement
+           | Iir_Kind_Psl_Assert_Directive
+           | Iir_Kind_Psl_Assume_Directive
            | Iir_Kind_Psl_Cover_Directive
            | Iir_Kind_Psl_Restrict_Directive =>
             return True;
diff --git a/src/vhdl/vhdl-parse.adb b/src/vhdl/vhdl-parse.adb
index e182821ae..491d14b85 100644
--- a/src/vhdl/vhdl-parse.adb
+++ b/src/vhdl/vhdl-parse.adb
@@ -8586,11 +8586,11 @@ package body Vhdl.Parse is
       Expect_Scan (Tok_Semi_Colon);
    end Parse_Psl_Assert_Report_Severity;
 
-   function Parse_Psl_Assert_Statement return Iir
+   function Parse_Psl_Assert_Directive return Iir
    is
       Res : Iir;
    begin
-      Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
+      Res := Create_Iir (Iir_Kind_Psl_Assert_Directive);
 
       --  Accept PSL tokens
       if Flags.Vhdl_Std >= Vhdl_08 then
@@ -8605,7 +8605,26 @@ package body Vhdl.Parse is
       Parse_Psl_Assert_Report_Severity (Res);
 
       return Res;
-   end Parse_Psl_Assert_Statement;
+   end Parse_Psl_Assert_Directive;
+
+   function Parse_Psl_Assume_Directive return Iir
+   is
+      Res : Iir;
+   begin
+      Res := Create_Iir (Iir_Kind_Psl_Assume_Directive);
+
+      --  Skip 'assume'
+      Scan;
+
+      Set_Psl_Property (Res, Parse_Psl.Parse_Psl_Property);
+
+      Vhdl.Scanner.Flag_Psl := False;
+      Vhdl.Scanner.Flag_Scan_In_Comment := False;
+
+      Expect_Scan (Tok_Semi_Colon);
+
+      return Res;
+   end Parse_Psl_Assume_Directive;
 
    function Parse_Psl_Cover_Directive return Iir
    is
@@ -8758,7 +8777,7 @@ package body Vhdl.Parse is
                if Vhdl_Std >= Vhdl_08
                  or else (Flag_Psl_Comment and then Flag_Scan_In_Comment)
                then
-                  Stmt := Parse_Psl_Assert_Statement;
+                  Stmt := Parse_Psl_Assert_Directive;
                else
                   Stmt := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement);
                   Parse_Assertion (Stmt);
@@ -8804,6 +8823,9 @@ package body Vhdl.Parse is
                Postponed_Not_Allowed;
                Label_Not_Allowed;
                Stmt := Parse_Psl_Declaration;
+            when Tok_Psl_Assume =>
+               Postponed_Not_Allowed;
+               Stmt := Parse_Psl_Assume_Directive;
             when Tok_Psl_Cover =>
                Postponed_Not_Allowed;
                Stmt := Parse_Psl_Cover_Directive;
diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb
index 16f9e0e37..7c87b3df5 100644
--- a/src/vhdl/vhdl-prints.adb
+++ b/src/vhdl/vhdl-prints.adb
@@ -3893,7 +3893,7 @@ package body Vhdl.Prints is
       end if;
    end Disp_PSL_NFA;
 
-   procedure Disp_Psl_Assert_Statement
+   procedure Disp_Psl_Assert_Directive
      (Ctxt : in out Ctxt_Class; Stmt : Iir) is
    begin
       Start_Hbox (Ctxt);
@@ -3909,7 +3909,25 @@ package body Vhdl.Prints is
       Disp_Token (Ctxt, Tok_Semi_Colon);
       Close_Hbox (Ctxt);
       Disp_PSL_NFA (Get_PSL_NFA (Stmt));
-   end Disp_Psl_Assert_Statement;
+   end Disp_Psl_Assert_Directive;
+
+   procedure Disp_Psl_Assume_Directive
+     (Ctxt : in out Ctxt_Class; Stmt : Iir) is
+   begin
+      Start_Hbox (Ctxt);
+      if Vhdl_Std < Vhdl_08 then
+         OOB.Put ("--psl ");
+      end if;
+      Disp_Label (Ctxt, Stmt);
+      Disp_Postponed (Ctxt, Stmt);
+      Disp_Token (Ctxt, Tok_Psl_Assume);
+      Disp_Psl_Expression (Ctxt, Get_Psl_Property (Stmt));
+      Disp_Report_Expression (Ctxt, Stmt);
+      Disp_Severity_Expression (Ctxt, Stmt);
+      Disp_Token (Ctxt, Tok_Semi_Colon);
+      Close_Hbox (Ctxt);
+      Disp_PSL_NFA (Get_PSL_NFA (Stmt));
+   end Disp_Psl_Assume_Directive;
 
    procedure Disp_Psl_Cover_Directive
      (Ctxt : in out Ctxt_Class; Stmt : Iir) is
@@ -3984,8 +4002,10 @@ package body Vhdl.Prints is
          when Iir_Kind_Psl_Declaration
            | Iir_Kind_Psl_Endpoint_Declaration =>
             Disp_Psl_Declaration (Ctxt, Stmt);
-         when Iir_Kind_Psl_Assert_Statement =>
-            Disp_Psl_Assert_Statement (Ctxt, Stmt);
+         when Iir_Kind_Psl_Assert_Directive =>
+            Disp_Psl_Assert_Directive (Ctxt, Stmt);
+         when Iir_Kind_Psl_Assume_Directive =>
+            Disp_Psl_Assume_Directive (Ctxt, Stmt);
          when Iir_Kind_Psl_Cover_Directive =>
             Disp_Psl_Cover_Directive (Ctxt, Stmt);
          when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-scanner.adb b/src/vhdl/vhdl-scanner.adb
index 740617ba4..2f08ffbab 100644
--- a/src/vhdl/vhdl-scanner.adb
+++ b/src/vhdl/vhdl-scanner.adb
@@ -1307,6 +1307,8 @@ package body Vhdl.Scanner is
                Current_Token := Tok_Psl_Property;
             when Std_Names.Name_Endpoint =>
                Current_Token := Tok_Psl_Endpoint;
+            when Std_Names.Name_Assume =>
+               Current_Token := Tok_Psl_Assume;
             when Std_Names.Name_Cover =>
                Current_Token := Tok_Psl_Cover;
             when Std_Names.Name_Default =>
diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb
index b4e949aac..671c59c27 100644
--- a/src/vhdl/vhdl-sem_psl.adb
+++ b/src/vhdl/vhdl-sem_psl.adb
@@ -695,12 +695,12 @@ package body Vhdl.Sem_Psl is
       Set_PSL_Clock (Stmt, Clk);
    end Sem_Psl_Directive_Clock;
 
-   function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir
+   function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir
    is
       Prop : PSL_Node;
       Res : Iir;
    begin
-      pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Statement);
+      pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive);
 
       --  Sem report and severity expressions.
       Sem_Report_Statement (Stmt);
@@ -730,7 +730,26 @@ package body Vhdl.Sem_Psl is
       PSL.Subsets.Check_Simple (Prop);
 
       return Stmt;
-   end Sem_Psl_Assert_Statement;
+   end Sem_Psl_Assert_Directive;
+
+   procedure Sem_Psl_Assume_Directive (Stmt : Iir)
+   is
+      Prop : PSL_Node;
+   begin
+      --  Sem report and severity expressions.
+      Sem_Report_Statement (Stmt);
+
+      Prop := Get_Psl_Property (Stmt);
+      Prop := Sem_Property (Prop, True);
+      Set_Psl_Property (Stmt, Prop);
+
+      --  Properties must be clocked.
+      Sem_Psl_Directive_Clock (Stmt, Prop);
+      Set_Psl_Property (Stmt, Prop);
+
+      --  Check simple subset restrictions.
+      PSL.Subsets.Check_Simple (Prop);
+   end Sem_Psl_Assume_Directive;
 
    procedure Sem_Psl_Cover_Directive (Stmt : Iir)
    is
diff --git a/src/vhdl/vhdl-sem_psl.ads b/src/vhdl/vhdl-sem_psl.ads
index 433555b20..1cd02796e 100644
--- a/src/vhdl/vhdl-sem_psl.ads
+++ b/src/vhdl/vhdl-sem_psl.ads
@@ -23,8 +23,9 @@ package Vhdl.Sem_Psl is
    procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir);
 
    --  May return a non-psl concurrent assertion statement.
-   function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir;
+   function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir;
 
+   procedure Sem_Psl_Assume_Directive (Stmt : Iir);
    procedure Sem_Psl_Cover_Directive (Stmt : Iir);
    procedure Sem_Psl_Restrict_Directive (Stmt : Iir);
    procedure Sem_Psl_Default_Clock (Stmt : Iir);
diff --git a/src/vhdl/vhdl-sem_stmts.adb b/src/vhdl/vhdl-sem_stmts.adb
index 4b8c5880c..545a543c7 100644
--- a/src/vhdl/vhdl-sem_stmts.adb
+++ b/src/vhdl/vhdl-sem_stmts.adb
@@ -2020,8 +2020,10 @@ package body Vhdl.Sem_Stmts is
                Sem_Psl.Sem_Psl_Declaration (El);
             when Iir_Kind_Psl_Endpoint_Declaration =>
                Sem_Psl.Sem_Psl_Endpoint_Declaration (El);
-            when Iir_Kind_Psl_Assert_Statement =>
-               New_El := Sem_Psl.Sem_Psl_Assert_Statement (El);
+            when Iir_Kind_Psl_Assert_Directive =>
+               New_El := Sem_Psl.Sem_Psl_Assert_Directive (El);
+            when Iir_Kind_Psl_Assume_Directive =>
+               Sem_Psl.Sem_Psl_Assume_Directive (El);
             when Iir_Kind_Psl_Cover_Directive =>
                Sem_Psl.Sem_Psl_Cover_Directive (El);
             when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-tokens.adb b/src/vhdl/vhdl-tokens.adb
index 8ad0e4081..1f17c5092 100644
--- a/src/vhdl/vhdl-tokens.adb
+++ b/src/vhdl/vhdl-tokens.adb
@@ -422,6 +422,8 @@ package body Vhdl.Tokens is
             return "sequence";
          when Tok_Psl_Endpoint =>
             return "endpoint";
+         when Tok_Psl_Assume =>
+            return "assume";
          when Tok_Psl_Cover =>
             return "cover";
          when Tok_Psl_Restrict =>
diff --git a/src/vhdl/vhdl-tokens.ads b/src/vhdl/vhdl-tokens.ads
index e8daf0bce..f8e2dd14e 100644
--- a/src/vhdl/vhdl-tokens.ads
+++ b/src/vhdl/vhdl-tokens.ads
@@ -261,6 +261,7 @@ package Vhdl.Tokens is
       Tok_Psl_Property,
       Tok_Psl_Sequence,
       Tok_Psl_Endpoint,
+      Tok_Psl_Assume,
       Tok_Psl_Cover,
       Tok_Psl_Restrict,
       Tok_Psl_Restrict_Guarantee,