How do external irq's get mapped?

[Charles Krinke]

Let me try a more simplified IRQ question a different way by only
referring to the 8541.

There are 12 external interrupt sources, irq[0..11] and as I understand
it, they all go through one vector, ExternalInput set in
head_fsl_booke.S and this vector resolves to "do_IRQ()", which I believe
is in arch/powerpc/kernel/irq.c (not arch/ppc/kernel/...).

I am striving to understand how mapping of these external pins
irq[0..11] gets to IRQ numbers as shown with "cat /proc/interrupts".

Could someone point me at some references I can read to understand this
nuance of the 8541 in a linux-2.6.17.11 kernel, please.

Charles