Hi,
I am looking for assertion to check the below:
Whenever input valid_i gets asserted for 7 or more cycles in last 10 cycles, then output signal valid_o should become 1.
Could someone pls. help me with this assertion? @ben2 , Could you pls. help here?

ap_7in10_contiguous: assert property(
@(posedge clk) valid_i[*7] within 1[*10] |-> valid_o);
// |-> for valid_o at the end of the 10th cycle
// |-> for valid_o at the 11th cycle.
p_7in10_noncontiguous: assert property(
@(posedge clk) valid_i[=7] intersect 1[*10] |-> valid_o);
// DO NOT USE THE within, see my paper

#11 Paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!

Link to the list of papers and books that I wrote, many are now donated.

a[=3] within 1[*5] is same as
##[0:$] a[->3] ##0 1 ##[0:$] 1
//If a is repeated 3 or more times, the sequence is considered a match
//Compare the sim results for
ap_3in5_noncontiguous: assert property(
@(posedge clk) $rose(a) |-> a[=3] intersect 1[*5]) p_insct++; else f_insct++;
ap_3in5_noncontiguous_BAD: assert property(
@(posedge clk) $rose(a) |-> a[=3] within 1[*5]) p_withn++; else f_withn++;

a[=3] within 1[*5] is same as
##[0:$] // The within container
!a[*0:$] ##1 a // same as a[->1]
##1 !a[*0:$] ##1 a // same as a[->1]
##1 !a[*0:$] // This and the previous 3 lines represent a[=3]
##[0:$] 1 // the within container
Analyzing the last 3 lines: a ##1 !a[*0:$] ##[0:$] we get
a ##1!a[*0] ##[0:$] or a ##1!a[*1:$] ##[0:$] //
a ##1!a[*0] ##[0:$] is same as
a ##1 empty ##[0:$] is same as
a ##0 1 ##[0:$] 1
Note: a ##1!a[*1:$] ##[0:$] is not needed since the sequence with the [*0] does not use it.
The other sequences are not needed.
My paper also does this analysis