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.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?
The ethernet card is is PCIE and you should read the PCIE configuration space to find the base address registers.2. what 's the Physical address for Ethernet card on TK1 board?