Formal Verification Approach for I2C Slave

Hello,

I am new in formal verification and I have a concept question about how to verify an I2C Slave block.

I think the response should be valid for any serial interface which needs to receive information for several clocks before making an action.

The the protocol description is the following: 

I have a serial clock (SCL), Serial Data Input (SDI) and Serial Data Output (SDO), all are ports of the I2C Slave block.

The protocol looks like this:

The first byte which is received by the slave consists in 7bits of sensor address and the 8th bit is the command 0/1 Write/Read.

After the first 8 bits, the slave sends an ACK (SDO = 1 for 1 clock) if the sensor address is correct.

Lets consider only this case, where I want to verify that the slave responds with an ACK if the sensor address is correct.

The only solution I found so far was to use the internal buffer from the block which saves the received bits during 8 clocks. The signal is called shift_s.

I also needed to use internal chip state (state_s) and an internal counter (shift_count_s).

Instead of doing an direct check of the SDO(sdo_o) depending on SDI (sdi_d_i), I used the internal shift_s register.

My question is if my approach is the correct one or there is a possibility to write the verification at a blackbox level.

Below you have the 2 properties: first checks connection from SDI to internal buffer, the second checks the connection between internal buffer and output.

property prop_i2c_sdi_store;
  @(posedge sclk_n_i)
  $past(i2c_bl.state_s == `STATE_RECEIVE_I2C_ADDR)
    |-> i2c_bl.shift_s == byte'({ $past(i2c_bl.shift_s), $past(sdi_d_i)});
endproperty
APF_I2C_CHECK_SDI_STORE: assert property(prop_i2c_sdi_store);

property prop_i2c_sensor_addr(sens_addr_sel, sens_addr);
@(posedge sclk_n_i) (i2c_bl.state_s == `STATE_RECEIVE_I2C_ADDR) && (i2c_addr_i == sens_addr_sel) && (i2c_bl.shift_count_s == 7)
  ##1 (i2c_bl.shift_s inside {sens_addr, sens_addr+1}) |-> sdo_o;
endproperty
APF_I2C_CHECK_SENSOR_ADDR0: assert property(prop_i2c_sensor_addr(0, `I2C_SENSOR_ADDRESS_A0));
APF_I2C_CHECK_SENSOR_ADDR1: assert property(prop_i2c_sensor_addr(1, `I2C_SENSOR_ADDRESS_A1));
APF_I2C_CHECK_SENSOR_ADDR2: assert property(prop_i2c_sensor_addr(2, `I2C_SENSOR_ADDRESS_A2));
APF_I2C_CHECK_SENSOR_ADDR3: assert property(prop_i2c_sensor_addr(3, `I2C_SENSOR_ADDRESS_A3));

PS: i2c_addr_i is address selection for the slave (there are 4 configurable sensor addresses, but this is not important for the case).

Thank you!