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
---
 testsuite/gna/issue880/psl.vhdl | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 testsuite/gna/issue880/psl.vhdl

(limited to 'testsuite/gna/issue880/psl.vhdl')

diff --git a/testsuite/gna/issue880/psl.vhdl b/testsuite/gna/issue880/psl.vhdl
new file mode 100644
index 000000000..a1e203f5f
--- /dev/null
+++ b/testsuite/gna/issue880/psl.vhdl
@@ -0,0 +1,30 @@
+entity psl is
+end;
+
+architecture behav of psl is
+  signal a, b, c : bit;
+  signal clk : bit;
+  subtype wf_type is bit_vector (0 to 7);
+  constant wave_a : wf_type := "10010100";
+  constant wave_b : wf_type := "01001010";
+  constant wave_c : wf_type := "00100101";
+begin
+  process
+  begin
+    for i in wf_type'range loop
+      clk <= '0';
+      wait for 1 ns;
+      a <= wave_a (i);
+      b <= wave_b (i);
+      c <= wave_c (i);
+      clk <= '1';
+      wait for 1 ns;
+    end loop;
+    wait;
+  end process;
+  
+  -- psl default clock is (clk'event and clk = '1');
+  -- psl a1: assume always a |=> b;
+  -- psl a2: assume always a -> eventually! c;
+  -- psl c1: cover {a;b;c};
+end behav;
-- 
cgit v1.2.3