CAS_CDRXADDR2
(((uint64_t)CAS_CDRXADDR2(sc,0)) >> 32));
CAS_CDRXADDR2(sc, 0));
KASSERT((CAS_CDRXADDR2(sc, 0) & 0x1fff) == 0);