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

1 files changed, 6 insertions, 0 deletions

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