In reply to bhajanpreetsinght:
// Requirements should be defined by an implementation, and this is what I see.
// I am struggling with your requirements. This is what I understand:
// 1) a, b, c, d, e must remain hi for a duration defined by a variable.
// 2) At the end of this duration of cycles, signal w should reamin deasserted (i.e., w==0) for 1 to 3 cycles.
// [Ben] This test is to be done for any string of a, b, c, d, e that remains hi for that period of cycles.
// 3) If a, b, c, d, e do not remain hi for the dynamically specified duration,
// this is a don't care situation.
//
//[Ben] This type of spec appears to be a sync pattern
/* I intend to use the dynamic repeat from the package
//----------------------------------------------------------------
// ****** 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)."
*/
module m;
import sva_delay_repeat_range_pkg::*;
bit clk, a, b, c, d, e, w;
int duration;
sequence q_abcde; @(posedge clk) a && b && c && d && e; endsequence
assert property(@(posedge clk)
sq_rpt_simple_count(q_abcde,duration) |-> w==0[*1:3]);
endmodule
Ben