In reply to ben@SystemVerilog.us:
Well this one you wrote here just above, seems to be the code for the AsFrom. I am still trying to get the desired result on my testbench for the AsFrom. I don’t know why the second part of the assertion (XNOR) doesn’t work with me. Haven’t yet checked the code for the Await.
Grand Summary of the two properties:
AsFrom: Initially O is 0, A comes at any time. On Kth arrival of A sampled on clk, O should be there, and afterwards O is exactly same as A.
Await: Initially O is 0, A comes at any time. On Nth arrival of A sampled on clk, O should be there, and afterwards O is zero again forever.
So yes O is ON once for a single clock cycle in its lifetime for the AWAIT property. Its not a contradiction, O will be 1 on the Nth detection of A, telling that the signal we were waiting for has arrived. Afterwards its zero forever. At that time when O=1, A must be 1 for the Nth time.
But for the other property AsFrom, O starts after the Kth event on A. and is exact copy of A. My apologies that the wording I chose made it confusing.