In reply to ben@SystemVerilog.us:
Thanks Ben for the code. I have updated my sequence and properties as below as per my requirement. I would like to see one pulse of a followed by b whenever c is asserted. But somehow i see 2 pulse of a sometimes and 1 b. Any suggestion to avoid this extra pulse?
sequence s_a;
$rose(a) ##1 $fell(a);
endsequence
sequence s_b;
$rose(b) ##1 $fell(b);
endsequence
property P1;
@(posedge clk) disable iff(~rst_n) rose(c) |=>c throughout ((s_a and (##[0:] s_b)));
endproperty
property P2;
@(posedge clk) disable iff(~rst_n) !c|->(a==0 && b==0);
endproperty
property P3;
@(posedge clk) disable iff(~rst_n) $rose(c) |=> not(b ##1 a[->1]);
endproperty
property P4;
@(posedge clk) disable iff(~rst_n) $rose(c) |=> not(!a ##1 b[->1]);
endproperty
property P5;
@(posedge clk) disable iff(~rst_n) $rose(c) |-> not(b || a);
endproperty
Thanks
CoS