SVA with multiple Implication operators

SystemVerilog
1

Hello Experts,

I would like your feedback on the following approach. The formal property below is written using multiple implication operators. It verifies that an AHB read access can overlap with a write access, demonstrating the pipelined nature of the AHB protocol. Please comment on the SVA coding style used here and share the pros and cons of this approach.

//AHB to AEI Read After Write
property p_ahb_to_aei_read_after_write; 
  logic [31:0] ahb_addr;
  @(posedge hclk) disable iff (!hresetn || ahb_s_hresp)
  s_ahb_read_addr_phase_seq(ahb_addr) |=> aei_read_seq(ahb_addr) 
           |-> wait_seq
           |-> ((ahb_s_hreadyout) &&(ahb_s_hrdata == aei_m_rdata)) 
           ##0 s_ahb_write_addr_phase_seq(ahb_addr)
           |=> aei_write_seq(ahb_addr) 
           |-> wait_seq 
           |-> (aei_m_wdata == ahb_s_hwdata);
endproperty

Thanks in advance!