Hi,

The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller.

can you please point out the reference or reason to choose this address for Tx1 board?

/* These devices are used by the seL4 kernel. */
#define UARTA_PPTR                          0xffffffffffff0000
#define GIC_DISTRIBUTOR_PPTR        0xffffffffffff3000
#define GIC_CONTROLLER_PPTR         0xffffffffffff4000

These addresses are used during kernel device map to access in the userspace

map_kernel_devices : kernel_devices[i].paddr :0x50042000       kernel_devices[i].pptr 0xffffffffffff4000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000        vaddr :0x1f4
map_kernel_devices : kernel_devices[i].paddr :0x50041000       kernel_devices[i].pptr 0xffffffffffff3000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000        vaddr :0x1f3
map_kernel_devices : kernel_devices[i].paddr :0x70006000       kernel_devices[i].pptr 0xffffffffffff0000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000        vaddr :0x1f0

Regards,

Munees