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

In reply to katce:

Because @(expr) means suspend the process until the expression changes. So the event e_rose gets generated when $rose goes from 0 to 1 and 1 to 0. You would really need

@(posedge $rose(testSignal, @(posedge clk)))

You can use $rose, $fell, etc. outside a property. See 16.9.3 Sampled value functions in the 1800-2017 LRM. But using $rose inside a procedural event control statement makes for a very unclear clocking context.

Use Ben’s solution.