In reply to sraja:
That is better. Originally you wrote that pop should go hight for one cycle. You did not specify what should happen if more than one of PC0…PC3 goes high at the same time. And you did not specify if PC0 could go high again before pop goes high. Here’s an assertion that should work for what you wrote:
property grant_follows_request(req,gnt);
@(posedge clk) $rose(req) |-> s_eventually !gnt ##1 gnt ##1 !gnt;
endproperty
property in_between(r0,r1,r2,r3,gnt);
@(posedge clk) $rose(r0) |=> !r1&&!r2&&!r3 until gnt;
endproperty
A1 :assert property ( grant_follows_request(pc0,pop) );
A2 :assert property ( in_between(pc0,pc1,pc2,pc3,pop) );
You’ll need to repeat these assertions for PC1…PC3.