In reply to ben@SystemVerilog.us:
Hi Ben,
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 precendence 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]
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.
At some point in your email, you state that:
You are requiring that the property (which is a sequence in this case, but a sequence can be a property)…
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?
One interesting thing I noticed is that if I try to add parantheses 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)
ERROR VCP2000 “Syntax error. Unexpected token: ##[O_HASHHASH]. Expected tokens: ‘;’.” “testbench.sv” 69 48
FAILURE “Compile failure 1 Errors 0 Warnings Analysis time: 0[s].”
Exit code expected: 0, received: 1
(Also checked the incisive)
Again, this implies that there is some fundamental difference between the throughout and until_with operators
Thanks,
Steven