CACHE_WRITEBACK
ASSERT(!(cache & CACHE_WRITEBACK));
printf("#define\tCACHE_WRITEBACK 0x%x\n", CACHE_WRITEBACK);