From ed269c05edba2112cdc65c1ceb04eb3c2c384a9c Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 8 Nov 2021 16:50:26 +0100
Subject: [PATCH] Add PSL vunit inherit example as ghdl/ghdl#1899 was fixed

* New example of PSL inherit usage
* Add example to formal tests
* Add issue_1899 to issues tests
* Add inherit to README
---
 README.md                    |  1 +
 formal/psl_vunit_inherit.sby | 19 +++++++++++++++++++
 formal/tests.mk              |  1 +
 issues/tests.mk              |  3 ++-
 src/psl_vunit_inherit.psl    | 23 +++++++++++++++++++++++
 src/psl_vunit_inherit.vhd    | 33 +++++++++++++++++++++++++++++++++
 6 files changed, 79 insertions(+), 1 deletion(-)
 create mode 100644 formal/psl_vunit_inherit.sby
 create mode 100644 src/psl_vunit_inherit.psl
 create mode 100644 src/psl_vunit_inherit.vhd

diff --git a/README.md b/README.md
index 1828d1f..3419983 100644
--- a/README.md
+++ b/README.md
@@ -80,6 +80,7 @@ The next lists will grow during further development
 * Partial support of named sequences (some parameter types missing)
 * Partial support of named properties (some parameter types missing)
 * Partial support of PSL `endpoint` (simulation only, in PSL comments)
+* vunit inhiterance (`inherit`, synthesis only)
 
 ### Yosys formal extensions (reference to [Symbiyosys docs](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables))
 
diff --git a/formal/psl_vunit_inherit.sby b/formal/psl_vunit_inherit.sby
new file mode 100644
index 0000000..f579812
--- /dev/null
+++ b/formal/psl_vunit_inherit.sby
@@ -0,0 +1,19 @@
+[tasks]
+bmc
+
+[options]
+depth 25
+bmc: mode bmc
+
+[engines]
+bmc: smtbmc z3
+
+[script]
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_vunit_inherit.vhd psl_vunit_inherit.psl -e psl_vunit_inherit
+prep -top psl_vunit_inherit
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_vunit_inherit.vhd
+../src/psl_vunit_inherit.psl
diff --git a/formal/tests.mk b/formal/tests.mk
index ff5a0a8..c9d28a8 100644
--- a/formal/tests.mk
+++ b/formal/tests.mk
@@ -36,6 +36,7 @@ psl_fell \
 psl_onehot \
 psl_onehot0 \
 psl_vunit \
+psl_vunit_inherit \
 yosys_anyconst \
 yosys_anyseq \
 psl_abort
diff --git a/issues/tests.mk b/issues/tests.mk
index 1a70fc3..daf8b21 100644
--- a/issues/tests.mk
+++ b/issues/tests.mk
@@ -11,4 +11,5 @@ issue_1372 \
 issue_1591 \
 issue_1658 \
 issue_1832 \
-issue_1850
\ No newline at end of file
+issue_1850 \
+issue_1899
diff --git a/src/psl_vunit_inherit.psl b/src/psl_vunit_inherit.psl
new file mode 100644
index 0000000..21714dd
--- /dev/null
+++ b/src/psl_vunit_inherit.psl
@@ -0,0 +1,23 @@
+vunit psl_vunit_inherit_0_vu {
+  
+  -- Named sequences
+  sequence s_a (boolean data) is {data; data};
+  sequence s_b (boolean data) is {data};
+
+}
+
+
+vunit psl_vunit_inherit_vu (psl_vunit_inherit(beh)) {
+
+  inherit psl_vunit_inherit_0_vu;
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion holds
+  SERE_0_a : assert always s_a(a) |-> s_b(b);
+
+  -- This assertion holds, similar to SERE_0_a
+  PROP_0_a : assert always {a; a} |-> {b};
+
+}
diff --git a/src/psl_vunit_inherit.vhd b/src/psl_vunit_inherit.vhd
new file mode 100644
index 0000000..59fb822
--- /dev/null
+++ b/src/psl_vunit_inherit.vhd
@@ -0,0 +1,33 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+  use ieee.numeric_std.all;
+
+use work.pkg.all;
+
+
+entity psl_vunit_inherit is
+  port (
+    clk : in std_logic
+  );
+end entity psl_vunit_inherit;
+
+
+architecture beh of psl_vunit_inherit is
+
+  signal a, b : std_logic;
+
+begin
+
+
+  --                              012345
+  SEQ_A : sequencer generic map ("--____") port map (clk, a);
+  SEQ_B : sequencer generic map ("_-____") port map (clk, b);
+
+  -- Stop simulation after longest running sequencer is finished
+  -- Simulation only code by using pragmas
+  -- synthesis translate_off
+  stop_sim(clk, 6);
+  -- synthesis translate_on
+
+
+end architecture beh;