From 5465e5e2cf27a4e77ac8aee28445f78f6a08d76b Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Sat, 28 Aug 2021 15:18:43 +0200
Subject: [PATCH] Add example using generate indexes in PSL properties to vunit
 example, see ghdl/ghdl#1850

---
 formal/psl_vunit.sby | 3 ++-
 src/psl_vunit.psl    | 8 ++++++++
 src/psl_vunit.vhd    | 6 +++++-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/formal/psl_vunit.sby b/formal/psl_vunit.sby
index 29ffd6b..a1a7554 100644
--- a/formal/psl_vunit.sby
+++ b/formal/psl_vunit.sby
@@ -18,11 +18,12 @@ sere_0: ghdl --std=08 -gformal=SERE_0 pkg.vhd sequencer.vhd psl_vunit.vhd psl_vu
 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
+all: ghdl --std=08 -gformal=ALL pkg.vhd sequencer.vhd hex_sequencer.vhd psl_vunit.vhd psl_vunit.psl -e psl_vunit
 prep -top psl_vunit
 
 [files]
 ../src/pkg.vhd
 ../src/sequencer.vhd
+../src/hex_sequencer.vhd
 ../src/psl_vunit.vhd
 ../src/psl_vunit.psl
diff --git a/src/psl_vunit.psl b/src/psl_vunit.psl
index 52bd972..8ad4e03 100644
--- a/src/psl_vunit.psl
+++ b/src/psl_vunit.psl
@@ -24,5 +24,13 @@ vunit psl_vunit_vu (psl_vunit(beh)) {
     SERE_3_a : assert always {a; a};
   end generate gen_3;
 
+  -- A simple check for counter increasing
+  counter_check : for i in 0 to 14 generate
+    SERE_4_a : assert always
+      {c = std_logic_vector(to_unsigned(i, 4))}
+      |=>
+      {c = std_logic_vector(to_unsigned(i + 1, 4))};
+  end generate counter_check;
+
 
 }
\ No newline at end of file
diff --git a/src/psl_vunit.vhd b/src/psl_vunit.vhd
index b79d147..830c0f5 100644
--- a/src/psl_vunit.vhd
+++ b/src/psl_vunit.vhd
@@ -1,5 +1,6 @@
 library ieee;
   use ieee.std_logic_1164.all;
+  use ieee.numeric_std.all;
 
 use work.pkg.all;
 
@@ -17,6 +18,7 @@ end entity psl_vunit;
 architecture beh of psl_vunit is
 
   signal a, b : std_logic;
+  signal c : std_logic_vector(3 downto 0);
 
 begin
 
@@ -24,12 +26,14 @@ begin
   --                              012345
   SEQ_A : sequencer generic map ("--____") port map (clk, a);
   SEQ_B : sequencer generic map ("_-____") port map (clk, b);
+  --
+  SEQ_C : hex_sequencer generic map ("0123456789ABCDEF") port map (clk, c);
 
 
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas
   -- synthesis translate_off
-  stop_sim(clk, 6);
+  stop_sim(clk, 18);
   -- synthesis translate_on