Add example for PSL verification units (vunit)

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:
 

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

formal/tests.mk

@@ -30,4 +30,5 @@ psl_prev \
 psl_stable \
 psl_rose \
 psl_fell \
-psl_logical_iff
+psl_logical_iff \
+psl_vunit

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;
+
+
+}

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;