(* Translation-intrinsically-before *) let tr-ib = [Imp & TTD & R]; iico_data; [B]; iico_ctrl; [Exp & M | MMU & FAULT] (* Notions of Same Location - PA, VA, and including Fault Effects *) let TTD-same-oa = same-oa(TTD*TTD) let same-loc = [M]; loc; [M] | [MMU & Translation & FAULT]; same-low-order-bits | same-low-order-bits; [MMU & Translation & FAULT] | (tr-ib^-1; TTD-same-oa; tr-ib) & same-low-order-bits let po-loc = po & same-loc (* Same-cache-line relation *) (* NOTE : currently assumes all locations are on different cache lines *) (* also extends to IC without a location specified *) let scl = loc | (M | DC.CVAU | IC) * (IC.IALLU | IC.IALLUIS) | (IC.IALLU | IC.IALLUIS) * (M | DC.CVAU | IC) let va-loc = (tr-ib; same-low-order-bits; tr-ib^-1) & loc let po-va-loc = po & va-loc