I have a req-ack-response interface, where req is asserted for one clock cycle and ack will be asserted in next clock cycle and next req will asserted only after response is asserted.I have written one assumption and one assertion as below.
with assumption_a when I check with assertion with $rose(req) |=> ##2 $rose(ack)); it is passing which is not correct. with assumption_b and assumption_c $rose(req) |=> ##2 $rose(ack)); is failing, which is as excepected.
I didn’t understand why splitting the assumption is working fine.
In reply to KranthiDV:
Your issue is your misunderstanding of the until property operator.
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
ap1: assert property(@ (posedge clk) $rose(a) |=> b ##1 a until c);
The until requires that the property*(b ##1 a)* repeats and must be true at every cycle.
See the images below.
What you need is the concatenation of a sequence and a property.
Thus, the following is illegal:
property P_illegal; a_sequence ##1 a_property; endproperty : P_illegal
This capability is introduced with the followed-by operators #-# and #=# that concatenates a sequence and a property. The followed-by operators are of the following forms for the definition of a property:
[1] sequence_expr #-# property_expr // concatenation with zero cycle delay
| sequence_expr #=# property_expr // concatenation with one cycle delay