From 0331772c3ef05bad40b748542939ccafab2a9c68 Mon Sep 17 00:00:00 2001
From: Pepijn de Vos <pepijndevos@gmail.com>
Date: Wed, 7 Aug 2019 04:20:14 +0200
Subject: 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
---
 src/grt/grt-rtis.ads | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/grt/grt-rtis.ads')

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,
 
-- 
cgit v1.2.3