In reply to Alonso14:
A simplistic model (for 1 bit req/gnt, and not fully tested for all cases) is below:
always @(posedge req) req_id++;
always @(posedge gnt) gnt_id++;
property p_uniq_req_gnt;
int v_req_id;
($rose(req), v_req_id = req_id) |->
##[1:4] (gnt && (v_req_id == gnt_id ));
endproperty : p_uniq_req_gnt
a_p_uniq_req_gnt : assert property (p_uniq_req_gnt);
Idea - you will need tags/IDs to mark requests and grants.
// Edited - removed use of $sampled for local variables
// But will be needed for subroutine calls in some cases
// Thanks Ben Cohen for pointing this out.
Regards
Srini
www.go2uvm.org