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

Parents
  • 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.

Reply
  • 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.

Children
No data
More questions in this forum