Click here for the answer.
This is actually a very common problem, although written in a simplified form above. You’ll find this property common across most formal bus interface property files: Wishbone, Avalon, AXI, AXI-Lite, AXI stream, AHB, APB, and more. Indeed, knowing how to get this right is important to formally verifying any kind of hand-shaking interaction.
Failing this property would be an indication that a transaction may have been dropped.