If REQ is asserted then the GRANT will be asserted after 3 clock cycles and the GRANT need to be high for the no.of cycles that the REQ was high
I didn’t get the last part
GRANT need to be high for the no.of cycles that the REQ was high
Assume that $rose( req ) is true at T0 so $rose( grant ) must be true at T3.
Do you mean that req will go low i.e de-assert after T3 or at T3 ?
(a) If Req goes low at T3 then grant should be remain asserted for 3 clocks ? i.e T3 T4 T5
(a) If Req goes low at T5 then grant should be remain asserted for 5 clocks ? i.,e T3 T4 T5 T6 T7
This would just be
REQ |-> ##3 GRANT;
If Req is high for 1 cycle, then grant will be high for 1cycle after #3 delay
If Req is high for 2 cycles, then grant will be high for 2cycles after #3 delay
If Req is high for random cycles continuously, then grant will be high for that many cycles of req after #3 delay
overall grant is dependent on req
Hi dave,
If Req is high for 2 cycle then grant should be high for 2 cycles
is it possible to count how many cycles req is high and can we place that many cycles for grant to be high after #3 dealy
It would really help if you could create an example that demonstrates the conditions you want to check and we can test the validity of the assertions.
always @(posedge clk) begin
req=$random;
grant=$random;
end
property prop_1;
@(posedge clk) $rose(req) |-> ##3 $rose(grant);
endproperty
assert property(prop_1);
property prop_2;
@(posedge clk) req |-> ##3 grant;
endproperty
assert property(prop_2);
property prop_3;
@(posedge clk) $rose(req) |-> ##3 $fell(grant);
endproperty
assert property(prop_3)
Note: Can we use multiple property for it? If Yes, then here all 3 properties must pass then only our design check is successful
- As per my understanding I wrote it, expecting good solution for the above question
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
1 Like