In reply to moogyd:
In reply to ben@SystemVerilog.us:
Actually, the throughout version behaves as I expect (and wanted).
For the throughout property example, I explicitely added the parentheses to ensure the correct behaviour - I already came across this “gotcha”
// Need to be careful with () here. It seems that the "##1" may have higher precedence than the "throughout"
property AP_req_ack0 ;
$rose(req_i) |-> (req_i throughout ack_o[->1]) ##1 !req_i ;
endproperty : AP_req_ack0
So the req_i througout only applies to ack_o[->1]
You are correct about the precedence rules. From my book, I am showing below those rules:
I am still not sure about the until_with version.
Basically, it works (i.e reports a failure) if the req_i becomes inactive before the ack_o becomes active (the until_with part).
However, if I change the stimulus such that the req_i stays high after ack_o, the “throughout” version correctly reports a failure, but the “until_with” version does not, which implies it is not “moving on” to the !req_i check.
1800 says: An until property of one of the overlapping forms (i.e., until_with, s_until_with) 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, and including a clock tick at which property_expr2 evaluates to true.
Thus, if property_expr1 evaluates to false (your req_i) then the property expression with the until_with fails. However, if req_i stays high after ack_o, I would have expected a failure. Can you share the test code?
At some point in your email, you state that:
Is the converse true? i.e. is it correct to treat
req_i until_with ack_o
as a sequence? If not, I guess using the ##1 is invalid in this case?
The converse is NOT true. If you look at the BNF for a property you’ll see
property_expr ::=
sequence_expr
| strong ( sequence_expr )
| weak ( sequence_expr )
| ( property_expr )....
But the BNF for a sequence does NOT show a sequence as a property as a possibility.
Actually, that makes sense because of the hierarchy of operators: sequences are built out of expressions (a sequence of 1 terms is the expression). Properties are built out of sequences. Concurrent assertions are built out of properties.
One interesting thing I noticed is that if I try to add parentheses to the property
property AP_req_ack1 ;
$rose(req_i) |-> (req_i until_with ack_o) ##1 !req_i ;
endproperty : AP_req_ack1
I get complilation error. With Aldex Riviera Pro (EDA playground)
The simulation tools are correct, you cannot concatenate a property with a sequence. The (req_i until_with ack_o) is a property. However, you can concatenate a sequence with a property with the followed-by operators
property_expr ::= // among other things
sequence_expr #-# property_expr
| sequence_expr #=# property_expr
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA 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 978-1539769712
- 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