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
Would this assertion not pass if req is high for 2 cycles and gnt is high for 3 or more cycles as well?
property p;
@(posedge clk) $rose(req) |-> !grant[*3] ##1 grant [*1:$] intersect !req[->1];
endproperty
@Abhinash_Prasad_Dash
A few observations ::
(1) As clarified by Deep_R ::
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
These cases are not covered using your solution.
(2) Your consequent requires grant to be low on the clock that $rose(req) is true and grant should remain low for next 2 clocks as well.
The original post doesn't specifically mention this as requirement.
(3) Intersect operator requires LHS & RHS sequence to be start at the same clock as well as end at the same clock.
For the following stimulus ::
always #5 clk = !clk;
initial begin
#4 ; req = 1;
#30 ; grant = 1 ; req = 0;
#2 ; $finish();
end
The assertion passes although ‘req’ was high for 3 clocks and ‘grant’ was high for 1 clock.
Ideally as per intention this should have resulted in assertion failure
Thanks @Have_A_Doubt for pointing out. Confusion on my end thought that after grant goes high it should remain high as long as req is high. Your solution seems to be correct for the requirement.
I wrote this assertion, do you think it will pass?
property P1;
@(posedge clk)
$rose(REQ) ##3 (grant[*1:$] intersect !REQ[->1]) ##1 (grant == $past(REQ, 3)) ##1 (grant == $past(REQ, 2)) ##1 (grant == $past(REQ, 1)) ##1 (grant == 0);
endproperty
@flyant
I haven’t tested your code with stimulus but one quick observation is your property expects $rose(REQ) to be True on every clock else assertion would fail.
If you insist on using ‘intersect’ operator here is one solution which works for the 7 stimulus that I tried ( let me know if it isn’t working as per expectation for any particular stimulus ) ::
property p3;
$rose(req) |-> ( $fell(req)[->1] ##3 1 ) intersect ( 1 ##3 $rose(grant) ##1 $fell(grant)[->1] );
endproperty
Note that intersect operator requires that both LHS & RHS sequence start at the same clock as well as end at the same clock.
Since $fell(req) could be true as soon as 1 clock after $rose(req) I use ##3 1 at the end of LHS sequence
EDIT :: property ‘p3’ clubs (1) and (2). So if grant isn’t asserted 3 clocks after req, ‘p3’ will catch it as well.
the LHS and RHS of intersect are grant[*1:$] and !REQ[->1], why does the property expect $rose(REQ) to be True on every clock
When your property executes on every posedge of clk,
what’s the first thing aka sequence_expression that is evaluated / checked ?
Test the following over multiple clocks ::
property p1;
@(posedge clk) $rose(req) |-> ##3 $rose(grant);
endproperty
property p2;
@(posedge clk) $rose(req) ##3 $rose(grant);
endproperty