Assertion for checking input signal to be high 7 or more times in last 10 cycles

SystemVerilog
1

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?
@user49 , Could you pls. help here?

Thanks

2

Ambiguous requirements:

  1. contiguous ?
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.

3

In summary,

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

code immediate exceptions(1) - EDA Playground

Wave EPWave Waveform Viewer
ANALYSIS:

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