The PIRQ_MISC registers in the indirect I/O address space with 0xc00
being the index register aren't IRQ numbers; those configuration bits.
To get an idea, have a look at the interrupt routing register chapter of
for example AMD publication number 45482 . Not sure if that's the
exact one you'll need, but it should be a good starting point.