PCMU_INTR_MAP_REG_TID_SHIFT
return ((mondo) | (cpu_id << PCMU_INTR_MAP_REG_TID_SHIFT) |
PCMU_INTR_MAP_REG_TID_SHIFT);