Hi all,

I’m trying to understand the implementation details and physical memory usage of seL4 for Tx1 

we have available physical memory in Tx1 is 6GB. 

DRAM (4GB) - available address range 8000_0000 - FFFF_FFFF

DRAM2 (4GB to 6GB) - available address range - 1_0000_0000 - 2_7FFF_FFFF 

In the hardware.h file (/kernel/include/plat/tx1/plat/machine/hardware.h),the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } 

'1MiB starting from 0xa7f00000 is reserved by the elfloader for monitor mode hooks'.I understand from the code its required only for 

Tk1. (/projects/tools/elfloader-tool/src/plat/tk1/monitor.S). As per my understanding is not not applicable for Tx1 so we can use 

contiguous region of physical ram 2GB to 4GB. Also it's allow to use higher physical memory for seL4 kernel ie > 4GB ?

Thanks in advance.

Regards,

Munees