In reply to MICRO_91:
See my paper Reflections on Users’ Experiences with SVA, part 2
https://verificationacademy.com/verification-horizons/july-2022-volume-18-issue-2/reflections-on-users-experiences-with-sva-part-2
Addresses the usage of these four relationship operators: throughout, until, intersect, implies
On your requirements, I suggest one of the following solutions. I assumed that ev is a variable and not an event. The a2 is for delays and repeats that are fixed at elaboration time. The a1 solution uses delays and repeat values that are defined in variables; that uses my SVA Package: Dynamic and range delays and repeats
https://rb.gy/a89jlh Provides a library and model solutions
module tb;
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_range_pkg::*;
int pre=2, post=3;
bit sig, ev;
// Using from the package
// sequence dynamic_delay(count);
// sequence sq_rpt_simple_count(sq, count);
// For m = 2 and n =3 :
a1: assert property (strong(dynamic_delay(pre) ##0 ev) implies sig[*1:$] ##1 ev ##1 sq_rpt_simple_count(sig, post)) ;
a2: assert property (strong(##2 ev) implies sig[*1:$] ##1 ev ##1 sig[*3]) ;
sig 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
ev - - - - - 1 - - - - - - - - - - - - - - - - -
<--->
<--------->
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog