Immediate assertion property - systemVerilog

[Essam]

Hi

I am trying to verify a function in my design of network switch where
I am using immediate assertion . the part I am verifying is a register
in a ring of shift registers. The register has an external input and
external output that are connected to input and output port via FIFO,
it also has internal input and output. R0In is input and R0Out is
output, the R0In is initially 16’h0000 and then it changes its value
randomly every few or several clock cycles. While the value of R0Out
either 16’h0000 or 16’hYYYY (any value other than 0000). So, the
output (R0Out) either 0000 or yyyy for few or several clock cycle.

For the input I am writing the property like this
property P1;
@(posedge clk)
not $stable(R0In) ;
endproperty;

this work fine but for the output R0Out, it is quite difficult. I am
trying to check only when the R0Out value change from (0000 to yyyy or
from yyyy to 0000) either one of them or from yyyy to xxxx.
If you I use same syntax as P1 above then it will assert both
condition or 0000 to yyyy and yyyy to 0000. so I used the following
systax

property P1;
@(posedge clk)
not $stable(R0Out) && R0Out != 16’h0000;
endproperty;

if you have any comment or better way to write the assertion property
please let me know

thanks

Essam