Hi All, When I try to understand SVA 4KB boundary with https://silver.arm.com/browse/BP062Following is a property// startproperty 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]);endpropertyand always @(AWSIZE or AWLEN or AWADDR) begin : p_WAddrIncrComb AwAddrIncr = AWADDR + (AWLEN << AWSIZE); // The final address of the burstend//end
If there is the transaction: AWADDR: 'd4095AWLEN:'d0AWSIZE:'d1AWBUSRT: incras far as I knowThis should violate the 4K limitDoes the property check above this part?Thanks,Sammy
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.