On Tue 27-Sep-2016 7:38 AM, PX wrote: 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? Interrupts 0-31 are reserved by ARM, so we offset the interrupt numbers by 32. This offsetting gets exposed to user space, hence the differences from the manual. 2. what 's the Physical address for Ethernet card on TK1 board? The ethernet card is is PCIE and you should read the PCIE configuration space to find the base address registers. Adrian