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

5 files changed, 37 insertions, 12 deletions

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);