Assumption for req and ack and response interface

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.

assertion_a: assert property (@(posedge clk) disable iff (rst) $rose(req) |=> $rose(ack));

assumption_a: assume property  (@(posedge clk)disable iff (rst)$rose(req)  |=> $fell(req)##0 !(req) until  $fell(rsp) );

but above seems to be not working, but when I spilit into two assumptions it is working.

assumption_b: assume property  (@(posedge clk)disable iff (rst)$rose(req)  |=> $fell(req));
assumption_c: assume property  (@(posedge clk)disable iff (rst)$fell(req)  |-> !(req) until  $fell(rsp) );

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.

Consider this example: (1) - EDA Playground


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


assumption_a: assume property  (@(posedge clk)disable iff (rst)$rose(req)  |=>
 $fell(req)#-# !(req) until  $fell(rsp) );



http://systemverilog.us/vf/temp1006.sv

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA
    Reflections on Users’ Experiences with SVA - Part II
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
    SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/