SVA to check a N-stage synchronizer output

SystemVerilog
, , , ,
7

If signal A changes at T6 then signal B should have changed at T3 or T2 or T1.

sequence b2a_change( N , M );
 $changed(b) ##[N:M] $changed(a);
endsequence

property b_2_a( N , M );
  @(posedge clk) disable iff (!rst_n)
    $changed(a) |→ b2a_change(N,M).triggered;
endproperty

b2a:assert property( b_2_a(3,5) ) else `uvm_error(..)