check 4KB boundary

Hi All, 

When I try to understand SVA 4KB boundary with 
https://silver.arm.com/browse/BP062

Following  is a property
// start
property AXI_ERRM_AWADDR_BOUNDARY;
    @(posedge `AXI_SVA_CLK)
    !($isunknown({AWVALID,AWBURST,AWADDR})) & AWVALID & (AWBURST == `AXI_ABURST_INCR)

        |-> (AwAddrIncr[ADDR_MAX:12] == AWADDR[ADDR_MAX:12]);
endproperty

and 
always @(AWSIZE or AWLEN or AWADDR) begin : p_WAddrIncrComb
    AwAddrIncr = AWADDR + (AWLEN << AWSIZE); // The final address of the burst
end

//end

If there is the transaction: 
AWADDR: 'd4095
AWLEN:'d0
AWSIZE:'d1
AWBUSRT: incr

as far as I know
This should violate the 4K limit
Does the property check above this part?

Thanks,
Sammy