integer n = UInt(Rn); integer t = UInt(Rt); integer t2 = UInt(Rt2); if L:opc<0> == '01' || opc == '11' then UNDEFINED; integer scale = 2 + UInt(opc<1>); constant integer datasize = 8 << scale; bits(64) offset = LSL(SignExtend(imm7, 64), scale); boolean tagchecked = wback || n != 31; boolean rt_unknown = FALSE; if wback && (t == n || t2 == n) && n != 31 then Constraint c = ConstrainUnpredictable(Unpredictable_WBOVERLAPST); assert c IN {Constraint_NONE, Constraint_UNKNOWN, Constraint_UNDEF, Constraint_NOP}; case c of when Constraint_NONE rt_unknown = FALSE; // value stored is pre-writeback when Constraint_UNKNOWN rt_unknown = TRUE; // value stored is UNKNOWN when Constraint_UNDEF UNDEFINED; when Constraint_NOP EndOfInstruction();

bits(64) address; bits(64) address2; bits(datasize) data1; bits(datasize) data2; constant integer dbytes = datasize DIV 8; boolean privileged = PSTATE.EL != EL0; AccessDescriptor accdesc = CreateAccDescGPR(MemOp_STORE, FALSE, privileged, tagchecked); if n == 31 then CheckSPAlignment(); address = SP[]; else address = X[n, 64]; if !postindex then address = GenerateAddress(address, offset, accdesc); if rt_unknown && t == n then data1 = bits(datasize) UNKNOWN; else data1 = X[t, datasize]; if rt_unknown && t2 == n then data2 = bits(datasize) UNKNOWN; else data2 = X[t2, datasize]; if IsFeatureImplemented(FEAT_LSE2) then bits(2*datasize) full_data; if BigEndian(accdesc.acctype) then full_data = data1:data2; else full_data = data2:data1; accdesc.ispair = TRUE; Mem[address, 2*dbytes, accdesc] = full_data; else address2 = GenerateAddress(address, dbytes, accdesc); Mem[address, dbytes, accdesc] = data1; Mem[address2, dbytes, accdesc] = data2; if wback then if postindex then address = GenerateAddress(address, offset, accdesc); if n == 31 then SP[] = address; else X[n, 64] = address;