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,
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