CCE_INT_COUNTER_ARRAY32
(counter * 8 + CCE_INT_COUNTER_ARRAY32), \
write_csr(dd, CCE_INT_COUNTER_ARRAY32 + (8 * i), 0);