Assertion to check reset is synchronised to the input clock

SystemVerilog
,
1

Hi, I am trying to write a property for the following behaviour. We have the following signals: clk, rst, ref_rst. The behaviour is the rst is asserted at the second posedge of clk after the ref_rst is asserted. We have an asynchronous ref_rst, the synchronous rst follows the asynchronous rst after 2 cycles of the clk. Will the below property work fine and is sufficient to check this behaviour?
The image shows the clk, ref_rst and rst signals:
image

property rst_chk;
        @(posedge clk)
        $rose(ref_rst) |-> ##1 $rose(rst);
endproperty

Edit: 2 cycles won’t be accurate according to the waveform attached. It should be 1 cycle after the ref_rst is captured as high on clock posedge.

2

In what way is ref_rst asynchronous? When can it be de-asserted?

3

Hi Dave, thanks for replying.
The ref_rst can be asserted & de-asserted at any time irrespective of the clock.