property p;
@(posedge clk) nexttime a;
endproperty
property q;
@(posedge clk) ##5 a;
endproperty
As per my understanding, both properties are equivalent. What is the difference between them?
property p;
@(posedge clk) nexttime a;
endproperty
property q;
@(posedge clk) ##5 a;
endproperty
As per my understanding, both properties are equivalent. What is the difference between them?
Here is a page from my just released SVA Handbook on this topic
nexttime::SystemVerilog Assertions Handbook 4th Edition, 2016
Basically, the difference between ‘nexttime’ and ‘##’ delay is that
property_expr ::=
nexttime property_expr // Weak Nexttime
| nexttime [ constant _expression ] property_expr // Weak Nexttime
| s_nexttime property_expr // Strong Nexttime
| s_nexttime [ constant_expression ] property_expr // Strong Nexttime
Thus, he nexttime property operators are equivalent to the followed-by
operator with the antecedent equal to the sequence (##k 1’b1).
nexttime [k] property_expr is same as
( (##k 1’b1) #-# property_expression)
Note :
ap_illegal: assert property(a |-> b ##2 not(c |-> f)); // <<-- illegal
ap_legal: assert property(a |-> b ##2 1 #-# not(c |-> f));
ap_legal2: assert property(a |-> nexttime[2] not(c |-> f));
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us