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, 38 insertions, 0 deletions

diff --git a/src/grt/grt-disp_rti.adb b/src/grt/grt-disp_rti.adb
index b3b595668..b908a3c3b 100644
--- a/src/grt/grt-disp_rti.adb
+++ b/src/grt/grt-disp_rti.adb
@@ -470,6 +470,8 @@ package body Grt.Disp_Rti is
 
          when Ghdl_Rtik_Psl_Assert =>
             Put ("ghdl_rtik_psl_assert");
+         when Ghdl_Rtik_Psl_Assume =>
+            Put ("ghdl_rtik_psl_assume");
          when Ghdl_Rtik_Psl_Cover =>
             Put ("ghdl_rtik_psl_cover");
          when Ghdl_Rtik_Psl_Endpoint =>
@@ -1310,6 +1312,7 @@ package body Grt.Disp_Rti is
             Disp_Type_Protected
               (To_Ghdl_Rtin_Type_Scalar_Acc (Rti), Ctxt, Indent);
          when Ghdl_Rtik_Psl_Cover
+           | Ghdl_Rtik_Psl_Assume
            | Ghdl_Rtik_Psl_Assert =>
             Disp_Psl_Directive (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent);
          when Ghdl_Rtik_Psl_Endpoint =>
diff --git a/src/grt/grt-lib.adb b/src/grt/grt-lib.adb
index 26491a7ad..149f218eb 100644
--- a/src/grt/grt-lib.adb
+++ b/src/grt/grt-lib.adb
@@ -116,6 +116,12 @@ package body Grt.Lib is
       Do_Report ("psl assertion", Str, "Assertion violation", Severity, Loc);
    end Ghdl_Psl_Assert_Failed;
 
+   procedure Ghdl_Psl_Assume_Failed
+     (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is
+   begin
+      Do_Report ("psl assumption", Str, "Assumption violation", Severity, Loc);
+   end Ghdl_Psl_Assume_Failed;
+
    procedure Ghdl_Psl_Cover
      (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is
    begin
diff --git a/src/grt/grt-lib.ads b/src/grt/grt-lib.ads
index 167ea98e5..1f5e020d4 100644
--- a/src/grt/grt-lib.ads
+++ b/src/grt/grt-lib.ads
@@ -40,6 +40,11 @@ package Grt.Lib is
       Severity : Integer;
       Loc : Ghdl_Location_Ptr);
 
+   procedure Ghdl_Psl_Assume_Failed
+     (Str : Std_String_Ptr;
+      Severity : Integer;
+      Loc : Ghdl_Location_Ptr);
+
    --  Called when a sequence is covered (in a cover directive)
    procedure Ghdl_Psl_Cover
      (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr);
@@ -116,6 +121,7 @@ private
 
    pragma Export (C, Ghdl_Assert_Failed, "__ghdl_assert_failed");
    pragma Export (C, Ghdl_Ieee_Assert_Failed, "__ghdl_ieee_assert_failed");
+   pragma Export (C, Ghdl_Psl_Assume_Failed, "__ghdl_psl_assume_failed");
    pragma Export (C, Ghdl_Psl_Assert_Failed, "__ghdl_psl_assert_failed");
    pragma Export (C, Ghdl_Psl_Cover, "__ghdl_psl_cover");
    pragma Export (C, Ghdl_Psl_Cover_Failed, "__ghdl_psl_cover_failed");
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
index cf603a097..1fd3ad94f 100644
--- a/src/grt/grt-psl.adb
+++ b/src/grt/grt-psl.adb
@@ -40,6 +40,8 @@ package body Grt.Psl is
    Is_First : Boolean := True;
    Nbr_Assert_Failed : Ghdl_U32 := 0;
    Nbr_Assert_Passed : Ghdl_U32 := 0;
+   Nbr_Assume_Failed : Ghdl_U32 := 0;
+   Nbr_Assume_Passed : Ghdl_U32 := 0;
    Nbr_Cover_Failed : Ghdl_U32 := 0;
    Nbr_Cover_Passed : Ghdl_U32 := 0;
 
@@ -96,6 +98,8 @@ package body Grt.Psl is
       case Ghdl_Rtiks_Psl (Rti.Kind) is
          when Ghdl_Rtik_Psl_Assert =>
             Put (F, """assertion""");
+         when Ghdl_Rtik_Psl_Assume =>
+            Put (F, """assumption""");
          when Ghdl_Rtik_Psl_Cover =>
             Put (F, """cover""");
       end case;
@@ -130,6 +134,14 @@ package body Grt.Psl is
                Put (F, "failed");
                Inc (Nbr_Assert_Failed);
             end if;
+         when Ghdl_Rtik_Psl_Assume =>
+            if Val = 0 then
+               Put (F, "passed");
+               Inc (Nbr_Assume_Passed);
+            else
+               Put (F, "failed");
+               Inc (Nbr_Assume_Failed);
+            end if;
          when Ghdl_Rtik_Psl_Cover =>
             if Val = 0 then
                Put (F, "not covered");
@@ -186,6 +198,16 @@ package body Grt.Psl is
       Put_U32 (F, Nbr_Assert_Passed);
       Put_Line (F, ",");
 
+      Put (F, "  ""assume"": ");
+      Put_U32 (F, Nbr_Assume_Failed + Nbr_Assume_Passed);
+      Put_Line (F, ",");
+      Put (F, "  ""assume-failure"": ");
+      Put_U32 (F, Nbr_Assume_Failed);
+      Put_Line (F, ",");
+      Put (F, "  ""assume-pass"": ");
+      Put_U32 (F, Nbr_Assume_Passed);
+      Put_Line (F, ",");
+
       Put (F, "  ""cover"": ");
       Put_U32 (F, Nbr_Cover_Failed + Nbr_Cover_Passed);
       Put_Line (F, ",");
diff --git a/src/grt/grt-rtis.ads b/src/grt/grt-rtis.ads
index 030cd7e04..d4664492f 100644
--- a/src/grt/grt-rtis.ads
+++ b/src/grt/grt-rtis.ads
@@ -94,6 +94,7 @@ package Grt.Rtis is
       Ghdl_Rtik_Attribute_Stable,
 
       Ghdl_Rtik_Psl_Assert,
+      Ghdl_Rtik_Psl_Assume,
       Ghdl_Rtik_Psl_Cover,
       Ghdl_Rtik_Psl_Endpoint,