constant integer t = UInt(Rt); constant integer t2 = UInt(Rt2); constant integer n = UInt(Rn); constant boolean nontemporal = FALSE; constant integer scale = 2 + UInt(opc<1>); constant integer datasize = 8 << scale; constant bits(64) offset = LSL(SignExtend(imm7, 64), scale); constant boolean tagchecked = wback || n != 31; boolean rt_unknown = FALSE; boolean wb_unknown = FALSE; if wback && (t == n || t2 == n) && n != 31 then constant Constraint c = ConstrainUnpredictable(Unpredictable_WBOVERLAPLD); assert c IN {Constraint_WBSUPPRESS, Constraint_UNKNOWN, Constraint_UNDEF, Constraint_NOP}; case c of when Constraint_WBSUPPRESS wback = FALSE; // Writeback is suppressed when Constraint_UNKNOWN wb_unknown = TRUE; // Writeback is UNKNOWN when Constraint_UNDEF EndOfDecode(Decode_UNDEF); when Constraint_NOP EndOfDecode(Decode_NOP); if t == t2 then constant Constraint c = ConstrainUnpredictable(Unpredictable_LDPOVERLAP); assert c IN {Constraint_UNKNOWN, Constraint_UNDEF, Constraint_NOP}; case c of when Constraint_UNKNOWN rt_unknown = TRUE; // Result is UNKNOWN when Constraint_UNDEF EndOfDecode(Decode_UNDEF); when Constraint_NOP EndOfDecode(Decode_NOP);

bits(64) address; bits(64) address2; bits(datasize) data1; bits(datasize) data2; constant integer dbytes = datasize DIV 8; constant boolean privileged = PSTATE.EL != EL0; constant boolean ispair = IsFeatureImplemented(FEAT_LSE2); constant AccessDescriptor accdesc = CreateAccDescGPR(MemOp_LOAD, nontemporal, privileged, tagchecked, ispair); if n == 31 then CheckSPAlignment(); address = SP[64]; else address = X[n, 64]; if !postindex then address = AddressAdd(address, offset, accdesc); if accdesc.ispair then constant bits(2*datasize) full_data = Mem[address, 2 * dbytes, accdesc]; if BigEndian(accdesc.acctype) then data2 = full_data<(datasize-1):0>; data1 = full_data<(2*datasize-1):datasize>; else data1 = full_data<(datasize-1):0>; data2 = full_data<(2*datasize-1):datasize>; else address2 = AddressIncrement(address, dbytes, accdesc); data1 = Mem[address , dbytes, accdesc]; data2 = Mem[address2, dbytes, accdesc]; if rt_unknown then data1 = bits(datasize) UNKNOWN; data2 = bits(datasize) UNKNOWN; X[t, datasize] = data1; X[t2, datasize] = data2; if wback then if wb_unknown then address = bits(64) UNKNOWN; elsif postindex then address = AddressAdd(address, offset, accdesc); if n == 31 then SP[64] = address; else X[n, 64] = address;