From 5e23ba91710399e42e11d76212ffc8c03e1508e6 Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Tue, 16 Jun 2020 20:00:02 +0200
Subject: [PATCH] Add example for PSL verification units (vunit)

---
 README.md            | 10 +++++-----
 formal/psl_vunit.sby | 28 ++++++++++++++++++++++++++++
 formal/tests.mk      |  3 ++-
 src/psl_vunit.psl    | 28 ++++++++++++++++++++++++++++
 src/psl_vunit.vhd    | 36 ++++++++++++++++++++++++++++++++++++
 5 files changed, 99 insertions(+), 6 deletions(-)
 create mode 100644 formal/psl_vunit.sby
 create mode 100644 src/psl_vunit.psl
 create mode 100644 src/psl_vunit.vhd

diff --git a/README.md b/README.md
index 853eb68..e98380e 100644
--- a/README.md
+++ b/README.md
@@ -61,14 +61,14 @@ The next lists will grow during further development
 
 ### Functions
 
-* `prev()` function (Synthesis only, see [prev() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_prev.vhd))
-* `stable()` function (Synthesis only, see [stable() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_stable.vhd))
-* `rose()` function (Synthesis only, see [rose() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_rose.vhd))
-* `fell()` function (Synthesis only, see [fell() example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_fell.vhd))
+* `prev()` function (Synthesis only)
+* `stable()` function (Synthesis only)
+* `rose()` function (Synthesis only)
+* `fell()` function (Synthesis only)
 
 ### Convenient stuff
 
-* Partial support of PSL vunits in synthesis
+* Partial support of PSL vunits (synthesis)
 
 ## Not yet supported by GHDL:
 
diff --git a/formal/psl_vunit.sby b/formal/psl_vunit.sby
new file mode 100644
index 0000000..29ffd6b
--- /dev/null
+++ b/formal/psl_vunit.sby
@@ -0,0 +1,28 @@
+[tasks]
+sere_0 bmc
+sere_1 bmc
+sere_2 bmc
+sere_3 bmc
+all bmc
+bmc all
+
+[options]
+depth 25
+bmc: mode bmc
+
+[engines]
+bmc: smtbmc z3
+
+[script]
+sere_0: ghdl --std=08 -gformal=SERE_0 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
+sere_1: ghdl --std=08 -gformal=SERE_1 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
+sere_2: ghdl --std=08 -gformal=SERE_2 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
+sere_3: ghdl --std=08 -gformal=SERE_3 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
+all: ghdl --std=08 -gformal=ALL pkg.vhd sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
+prep -top psl_vunit
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_vunit.vhd
+../src/psl_vunit.psl
diff --git a/formal/tests.mk b/formal/tests.mk
index 98e27cf..eae450b 100644
--- a/formal/tests.mk
+++ b/formal/tests.mk
@@ -30,4 +30,5 @@ psl_prev \
 psl_stable \
 psl_rose \
 psl_fell \
-psl_logical_iff
+psl_logical_iff \
+psl_vunit
\ No newline at end of file
diff --git a/src/psl_vunit.psl b/src/psl_vunit.psl
new file mode 100644
index 0000000..52bd972
--- /dev/null
+++ b/src/psl_vunit.psl
@@ -0,0 +1,28 @@
+vunit psl_vunit_vu (psl_vunit(beh)) {
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  gen_0 : if FORMAL = "SERE_0" or formal = "ALL" generate
+    -- This assertion holds
+    SERE_0_a : assert {a};
+  end generate gen_0;
+
+  gen_1 : if FORMAL = "SERE_1" or formal = "ALL" generate
+    -- This assertion holds
+    SERE_1_a : assert {a; a};
+  end generate gen_1;
+
+  gen_2 : if FORMAL = "SERE_2" or formal = "ALL" generate
+    -- This assertion holds
+    SERE_2_a : assert {a; a and b};
+  end generate gen_2;
+
+  gen_3 : if FORMAL = "SERE_3" or formal = "ALL" generate
+    -- This assertion doesn't hold at cycle 2
+    SERE_3_a : assert always {a; a};
+  end generate gen_3;
+
+
+}
\ No newline at end of file
diff --git a/src/psl_vunit.vhd b/src/psl_vunit.vhd
new file mode 100644
index 0000000..b79d147
--- /dev/null
+++ b/src/psl_vunit.vhd
@@ -0,0 +1,36 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_vunit is
+  generic (
+    formal : string := "ALL"
+  );
+  port (
+    clk : in std_logic
+  );
+end entity psl_vunit;
+
+
+architecture beh of psl_vunit 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;