I need to write an assertion to catch response of a request if request is asserted after certain control signal. There are two control signals “start” and “eop”, for every start there is an eop at the end of the process. If “request” is asserted after start and before eop, the “response” shall come only after “eop” and not before. I have come up with an assertion which works also, but I am not convinced that this is the best way to achieve this, can someone help me how do I make it better. Following is assertion I am using right now:
// I need to write an assertion to catch response of a request if request is asserted after certain control signal.
// There are two control signals "start" and "eop", for every start there is an eop at the end of the process.
ap_start2eop: assert property(@(posedge clk) $rose(start) |-> strong (##[1:$] $rose(eop)));
// [Ben] Wirte short assertions when you see them fit.
// If "request" is asserted after start and before eop, the "response" shall come only after "eop" and not before.
// I have come up with an assertion which works also, but I am not convinced that this is the best way to achieve this,
// can someone help me how do I make it better. Following is assertion I am using right now:
property check_rsp;
@(posedge clk)
$rose(start) |=> req[->1] |-> strong(
first_match(!ack [*0:$] ##1 $rose(eop) ##1 $fell(eop)) ##[0:10] (ack == 1) );
endproperty
// [Ben] WIth $rose(start) |-> req[->1] you state that req CAN OCCUR in the SAME cycle as start.
// I think you want to say that req can occur any cycle AFTER start, thus you need to write
// $rose(start) |=> req[->1]
// [Ben] If ack NEVER occurs, but eop does, the assertion the way yo have will not fail because of the !ack [*0:$]
// (!ack [*0:$] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) is same as
// (!ack [*0 ] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) or
// (!ack [*1] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) or
// ..
// (!ack [*n] ##1 $rose(eop) ##1 $fell(eop) ##[0:10] (ack == 1)) // n==infinity
// THUS, you need the first_match()
// [Ben] On the "strong", you may want to qualify that for the whole consequent
// [Ben] Avoid writing unnecessary parenheses, like ($rose(start)), $rose(start) is sufficient
ap_check_rsp: assert property(check_rsp)
$display("assertion passed");
else
$display("assertion failed");
// [Ben] Add labels.
// FOr assertions that are not reused and that do not have local variables, avoid writing a separate property declaration.
In reply to ben@SystemVerilog.us:
Got this interesting response from Ed, a colleague and author of “SVA: The Power of Assertions in SystemVerilog by Eduard Cerny (2014-08-24”
the spec itself is confusing or incomplete. E.g.,
- verify only if start is followed by req then ack does happen until after eop happens? req is after start and strictly before eop?
- does it also have to check for the case when req does not happen, i.e. that eop does happen?
For the first one I think it should be
$rose(start) ##1 req[->1] |=> strong(!ack throughout eop[->1] ##[1:10] ack)
to check for the 2nd case and that eop is a pulse should be done separately
It would be better if liveness could be replaced by some bound on the open-ended interval to make it a safety property.
You are right the spec is not complete, if req comes anywhere else other than between start and eop than ack is expected at very next clock. I am validating this using interface monitor and assertion is not required to cover this scenario.
There is no dependency of eop on req, eop will come no matter what for each start, my test case sequence end condition is to receive eop. Bounded assertion for this interface is difficult as cycles consumed between start and eop depends on lot of factors which changes dynamically during simulation like random read response delays.
I also tried the property in last comment there is a small issue with the consequent, following works:
$rose(start) ##1 req[->1] |=> strong((!ack throughout eop[->1]) ##[1:10] ack)
The only change I made is to add parentheses around “!ack throughout eop[->1]”. I think earlier the entire sequence on RHS of throughout was getting evaluated which was causing assertion to fail.