I have questions about the irqs defined for TK1 guest linux.

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?

2. what 's the Physical address for Ethernet card on TK1 board?

Thanks

Peng