Detect AHB data-phase of AHB Write/Read Access and check the write/read data is valid. (SVA)

SystemVerilog
, ,
1 
Detect AHB write data-phase of AHB Write Access and check the write data is valid. (SVA)

property detect_write_data_phase;

$past(hready && hwrite && (htrans inside {SEQ, NONSEQ})) |-> 
                                           !$isunknown(hwdata);

endproperty

Please help, if the above will correctly detect the write-data phase of AHB write access.


// DATA -Phase of Read transfer check Assertion
 
  property read_data_valid;
    @(posedge HCLK) disable iff (~HRESETn)
     ((hreadyout) && (hwrite == READ) && 
(htrans inside {SEQ, NONSEQ})) ##[1:$] (hreadyout)
     |->   (hresp == OKAY) && !$isunknown(hrdata); 
  endproperty