From d2db77183ea3b868bc207078816e191a6356d9da Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 18 May 2020 13:53:23 +0200
Subject: [PATCH] Fix SERE, replacing within with && operator

---
 README.md                                        |  3 ++-
 src/psl_sere_non_consecutive_goto_repetition.vhd | 16 ++++++++--------
 ...sl_sere_non_consecutive_repeat_repetition.vhd | 12 ++++++------
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/README.md b/README.md
index b9b8614..bf1a3c7 100644
--- a/README.md
+++ b/README.md
@@ -51,6 +51,7 @@ The next lists will grow during further development
 * Consecutive repetition operator ([*], [+], [*n], [*i to j])
 * Non consecutive repetition operator ([=n], [=i to j])
 * Non consecutive goto repetition operator ([->], [->n], [->i to j])
+* Length-matching and operator (&&)
 * within operator
 
 ## PSL features not yet supported by GHDL:
@@ -61,4 +62,4 @@ The next lists will grow during further development
 ## 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)
+* next_event_a[i to j] operator
diff --git a/src/psl_sere_non_consecutive_goto_repetition.vhd b/src/psl_sere_non_consecutive_goto_repetition.vhd
index 3ddf4c5..3f3841b 100644
--- a/src/psl_sere_non_consecutive_goto_repetition.vhd
+++ b/src/psl_sere_non_consecutive_goto_repetition.vhd
@@ -46,20 +46,20 @@ begin
   SERE_2_a : assert always {req} |=> {busy[->5]; done};
 
   -- Non consecutive repetition of 3 cycles without padding
-  -- busy has to hold on 3 cycles between req & and the first done
-  -- This is a more exact version of the assertions before using the
-  -- within SERE operator (busy[*3] has to hold during done don't holds)
+  -- busy has to hold on exactly 3 cycles between req & and the first done
+  -- This is a more exact version of the assertions before using
+  -- the length-matching and SERE operator &&
   -- This assertion holds
-  SERE_3_a : assert always {req} |=> {{{busy[->3]} within {not done[+]}}; done};
+  SERE_3_a : assert always {req} |=> {{{busy[->3]} && {not done[+]}}; done};
 
   -- Non consecutive repetition of 4 cycles without padding
-  -- busy has to hold on 4 cycles between req & and the first done
+  -- busy has to hold on exactly 4 cycles between req & and the first done
   -- This assertion doesn't hold at cycle 7
-  SERE_4_a : assert always {req} |=> {{{busy[->4]} within {not done[+]}}; done};
+  SERE_4_a : assert always {req} |=> {{{busy[->4]} && {not done[+]}}; done};
 
-  -- At least one occurance of busy directly in the cycle before done holds
+  -- Equivalent to SERE_3_a
   -- This assertion holds
-  SERE_5_a : assert always {req} |=> {{{busy[->]} within {not done[+]}}; done};
+  SERE_5_a : assert always {req} |=> {{{busy[=2]; busy[->]} && {not done[+]}}; done};
 
 
 end architecture psl;
diff --git a/src/psl_sere_non_consecutive_repeat_repetition.vhd b/src/psl_sere_non_consecutive_repeat_repetition.vhd
index 7854244..010b60b 100644
--- a/src/psl_sere_non_consecutive_repeat_repetition.vhd
+++ b/src/psl_sere_non_consecutive_repeat_repetition.vhd
@@ -46,16 +46,16 @@ begin
   SERE_2_a : assert always {req} |=> {busy[=5]; done};
 
   -- Non consecutive repetition of 3 cycles with possible padding
-  -- busy has to hold on 3 cycles between req & and the first done
-  -- This is a more exact version of the assertions before using the
-  -- within SERE operator (busy[*3] has to hold during done don't holds)
+  -- busy has to hold on exactly 3 cycles between req & and the first done
+  -- This is a more exact version of the assertions before using
+  -- the length-matching and SERE operator &&
   -- This assertion holds
-  SERE_3_a : assert always {req} |=> {{{busy[=3]} within {not done[+]}}; done};
+  SERE_3_a : assert always {req} |=> {{{busy[=3]} && {not done[+]}}; done};
 
   -- Non consecutive repetition of 4 cycles with possible padding
-  -- busy has to hold on 4 cycles between req & and the first done
+  -- busy has to hold on exactly 4 cycles between req & and the first done
   -- This assertion doesn't hold at cycle 8
-  SERE_4_a : assert always {req} |=> {{{busy[=4]} within {not done[+]}}; done};
+  SERE_4_a : assert always {req} |=> {{{busy[=4]} && {not done[+]}}; done};
 
 
 end architecture psl;