It would easier to split it into 2 concurrent assertions
(1) Grant should be asserted 3 clocks after $rose( req)
property prop_1;
@(posedge clk) $rose(req) |-> ##3 $rose(grant);
endproperty
assert property(prop_1);
(2) Grant should remain asserted for same no. of clocks as Req
property p2;
int unsigned req_t , grant_t ;
( ($rose(req),req_t = 0) ##0( (req,req_t++)[*1:$] ##1 $fell(req) ) ) and
( ($rose(grant)[->1],grant_t = 0) ##0( (grant,grant_t++ )[*1:$] ##1 $fell(grant) ) ) |-> ( req_t == grant_t );
endproperty
assert property( @(posedge clk) p2) $display("T:%0t Pass",$time);
else $display("T:%0t Fails",$time);
Note: ‘and’ operator requires LHS & RHS sequence start at same clock.
Since grant ideally is to be asserted after 3 clocks, I use $grant[->1] in RHS.
$rose(grant)[->1] could also be replaced with $rose(req) ##3 $rose(grant)
I tested (2) with the following stimulus. It’s working as per expectations
always #5 clk = !clk;
initial begin
#4 ; req = 1;
`ifdef M1
// req is high for 1 clock from T0 to T1. Grant is asserted from T3 to T4
#10 ; req = 0;
#20 ; grant = 1;
#10 ; grant = 0;
`elsif M2
// req is high for 1 clock from T0 to T1. Grant is asserted from T3 to T5 i.e 2 clocks ( which is Incorrect ) !!
#10 ; req = 0;
#20 ; grant = 1;
#20 ; grant = 0;
`elsif M3
// req is high for 2 clocks from T0 to T2. Grant is asserted from T3 to T5
#20 ; req = 0;
#10 ; grant = 1;
#20 ; grant = 0;
`elsif M4
// req is high for 2 clocks from T0 to T2. Grant is asserted from T3 to T4 i.e 1 clock ( which is Incorrect ) !!
#20 ; req = 0;
#10 ; grant = 1;
#10 ; grant = 0;
`elsif M5
// req is high for 3 clocks from T0 to T3. Grant is asserted fro T3 to T6
#30 ; req = 0;
grant = 1;
#30 ; grant = 0;
`elsif M6
// req is high for 3 clocks from T0 to T3. Grant is asserted from T3 to T5 i.e 2 clocks ( which is Incorrect ) !!
#30 ; req = 0;
grant = 1;
#20 ; grant = 0;
`endif
#2 ; $finish();
end