sfcc_cache_wbinv_range
void sfcc_cache_wbinv_range(vaddr_t, vsize_t);
cpu_dcache_wbinv_range = sfcc_cache_wbinv_range;
cpu_dcache_inv_range = sfcc_cache_wbinv_range;
cpu_dcache_wb_range = sfcc_cache_wbinv_range;