Fixed entity & file names of [=] examples

README.md

@@ -58,7 +58,7 @@ The next lists will grow during further development
 * Synthesis of strong operator versions
 * SERE goto repetition operator ([->], [->n], [->i to j])
 
-## PSL features supported by GHDL, behaviour under investigation
+## PSL features under investigation
 
 * before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd)
 * next_event_a[i to j] operator (Behaviour currently under investigation)

formal/psl_sere_consecutive_repeat_repetition.sby

@@ -1,18 +0,0 @@
-[tasks]
-bmc
-
-[options]
-depth 25
-bmc: mode bmc
-
-[engines]
-bmc: smtbmc z3
-
-[script]
-bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_consecutive_repeat_repetition.vhd -e psl_sere_consecutive_repeat_repetition
-prep -top psl_sere_consecutive_repeat_repetition
-
-[files]
-../src/pkg.vhd
-../src/sequencer.vhd
-../src/psl_sere_consecutive_repeat_repetition.vhd

formal/psl_sere_non_consecutive_repeat_repetition.sby

@@ -0,0 +1,18 @@
+[tasks]
+bmc
+
+[options]
+depth 25
+bmc: mode bmc
+
+[engines]
+bmc: smtbmc z3
+
+[script]
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_non_consecutive_repeat_repetition.vhd -e psl_sere_non_consecutive_repeat_repetition
+prep -top psl_sere_non_consecutive_repeat_repetition
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_sere_non_consecutive_repeat_repetition.vhd

formal/tests.mk

@@ -17,4 +17,5 @@ psl_sere \
 psl_sere_overlapping_suffix_impl \
 psl_sere_non_overlapping_suffix_impl \
 psl_sere_consecutive_repetition \
-psl_sere_consecutive_repeat_repetition
+psl_sere_non_consecutive_repeat_repetition \
+psl_sere_non_consecutive_goto_repetition