check 4KB boundary

Hi All, 

When I try to understand SVA 4KB boundary with

Following  is a property
// start
    @(posedge `AXI_SVA_CLK)

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

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


If there is the transaction: 
AWADDR: 'd4095

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


  • Hi Sammy,

    Your AXI transaction would NOT violate a 4K boundary.

    You are using a start address (4095) that isn't aligned to the transfer width (16-bit), so what this 1-beat transaction would actually transfer is just one byte.

    Although the AXI protocol describes that it supports "unaligned transfers", the actual implementation is still transfers to AxSIZE aligned sections of the data bus, so when AWSIZE indicates a 16-bit transfer, the unaligned start address means that only upper half of this 16-bit data will be transferred.

    There are a few examples of this in the AXI spec, so have a look at figure A3-13 showing AxSIZE=32-bit transfers in INCR transactions. The unaligned start addresses mean that in the 2nd, 3rd and 4th examples that the first transfer doesn't actually transfer 32-bits.

    The remaining transfers in the INCR bursts in these examples DO transfer 32-bits each, so these are AxSIZE aligned, and it is only the first transfer that was unaligned.

    FIXED bursts type transactions remain unaligned for each transfer in the transaction, and WRAP bursts cannot use unaligned start addresses.

More questions in this forum