Assertion for ACK and REQ

Ben,

I guess the following assertion would cover both the requirements :

property req_ack;
@(posedge refclk)
$rose(req) |=> (##[9:20] ack) intersect (!req throughout ack[->1]);
endproperty

Thanks