In reply to tsb_matumoto:
Hello,
Hum I’m not sure I understand your question…
I’m pretty sure the proeprty is correct regarding your waveforms and descriptions.
What do you mean by “when $rose(req) happens, (req && ack) is not always true”?
If it’s again related to the possibility to abort transfers, my answer is in the previous message. Add the abort condition to the property.
But what I don’t quite get is that when $rose(req), you don’t know anything about the end of the property. You have to wait for 12 potential cycles.