Register value is updated based on handshake on B Channel

SystemVerilog
,
1

Hi Forum,
In my Tb I have 2 AXI4 interfaces :

  1. 32-bit CSR interface to read/write RTL registers
  2. 128-bit Exception interface for RTL to send Write txns to firmware.
    FW would send BResp to RTL upon successfully writing it to it’s OCM

The intent is to check that value of register TAIL_PTR is updated in RTL when handshake occurs on (2)

(A) Upon seeing handshake on B channel I could initiate a register read ( via RAL on (1) )
One limitation with this approach would be that this would consume more than 1 clocks so it wouldn’t ensure that register has updated value on the next clock of the BResp handshake.

(B) Using SVA ::

 logic [31:0] ptr_reg;
 assign ptr_reg = <RTL_hierarchy_of_reg_TAIL_PTR> ;

 assert property(  @(posedge clk)  $rose( Bresp & BValid & BReady ) |=> $changed( ptr_reg )  );

Should I go with (B) or does there exist a better solution ?