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
is a sequential operator whereas nexttime is a property operator.
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
- SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115