In reply to Shubhabrata:
module m;
bit clk, vld, req, ack, rst_n=1;
int err1, err2, pass1, pass2;
initial forever #10 clk = !clk;
property p1; // need 2 or more vld in this example
int count = 0;
@(posedge clk) disable iff(!rst_n)
$rose(req) |=>
((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)##1
$rose(ack) && !vld [->1] );
endproperty
assert property (p1) pass1=pass1+1; else err1=err1+1;
// Above assertion misses the condition of a ack and a vld in the same cycle
// particularly if this should be an error
// The following des check for this.
// I don;t think you need the first_match here
// but I believe the simulator will not try the other threads
property p2;
int count = 0;
@(posedge clk) disable iff(!rst_n)
$rose(req) |=>
first_match((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)) ##1
$rose(ack) && !vld [->1];
endproperty
assert property (p2) pass2=pass2+1; else err2=err2+1;
ap_ack_vld: assert property(@(posedge clk) not($rose(ack) && vld)) else err3=err3+1;
Ben