I have a property to check if the data is stable while some signal is zero, something like:
~arb |=> $stable(data)
This is true only if a clear signal is not activated.
I am using a flop to store a flag if the clear signal is asserted during the transaction, and checking it in the precondition:
~arb & ~is_cleared |=> $stable(data)
I don't like this solution, is not elegant and it needs many logic to manage the flop load and clear.
Any idea of how to do it only with SVA in a better way?