Untested code, but looks very promising for your needs.
I user Perplexity.ai to clarify the case when valid drops but rises again before
idel has a chance to rise. There I did a ync_accept_on the property, making it vacuous.
// SVA Package: Dynamic and range delays and repeats
// SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy Provides a library and model solutions
// I need to code assertions for the following scenario
// once valid is deasserted, idle should not be asserted before x_delay cycles.
// Here x_delay is from a register which can change mid simulation and also can be 0,
// Another point, valid can be asserted back before idle is asserted check has to be disabled now,
// REPHRASE: VALID may rise again before IDLE has a chance to rise. In this scenario, IDLE should not rise.
// The check for IDLE rising should be disabled when VALID rises again before IDLE has asserted.
// valid 1 1 1 1 1 0 0 1 1 1 0 0 0 0 0 0 0 0
// idle 0 0 0 0 0 0 0 0 0 0 0 0 0 1
// accept_on ( expression_or_dist ) property_expr
module m;
import sva_delay_repeat_range_pkg::*;
/* //----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)." */
bit clk, idle, valid, reset_n=1;
bit[2:0] range=3;
assert property (@ (posedge clk)
disable iff (!reset_n)
sync_accept_on ( $rose(valid, @(posedge clk)) )
$fell(valid) |-> sq_rpt_simple_count(! idle, range) ##1 idle);
endmodule
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf