In reply to ben@SystemVerilog.us:
Dear Ben,
thank you for your example and explanation.
Can you please explain me why e_rose is generated two times each time the testSignal rose? When the clocking event is specified to @(posedge clk), I would have expected that it only happens at the positive clock edge, not at the positive edge of testSignal.
I put this code into a module for formal verification. I was actually surprised that I can use $rose outside a property, because I thought the always blocks would be synthesized. I am not sure how $rose is behaving in synthesized code.
And then I am wondering how using the signal in an always block can have an influence on the coverability of the cover property. Do you know that?
Thank you,
K.