RMIXL_PIC_IRTENTRYC1
c1 = RMIXL_PICREG_READ(RMIXL_PIC_IRTENTRYC1(irt));
RMIXL_PICREG_WRITE(RMIXL_PIC_IRTENTRYC1(irt), 0); /* high word */
KASSERT(RMIXL_PICREG_READ(RMIXL_PIC_IRTENTRYC1(irt)) == 0);
RMIXL_PICREG_WRITE(RMIXL_PIC_IRTENTRYC1(irt), irtc1); /* high word */