Formal Property Verification: Property uncoverable if signal used in always block

Ż*In reply to dave_59:*

On always @($rose(testSignal, @(posedge clk)))
I see it triggering when testsignal rises 2ns after the posedge clk.
But the $rose should be tested @posedge clk.
Question: why then is the always @($rose(testSignal, @(posedge clk)))triggering?
At that time (2ns after the posedge of clk) there is no $rose tested in the clk edge that occurred 2ns before the testsignal changes.
Looks like the $rose is ignoring the specified clk edge.
Agree, this is a very unusual way of using the $rose.
Ben