constant integer t = UInt(Rt); constant integer n = UInt(Rn); constant boolean nontemporal = FALSE; constant boolean tagchecked = wback || n != 31; Constraint c; boolean rt_unknown = FALSE; if wback && n == t && n != 31 then 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 original value when Constraint_UNKNOWN rt_unknown = TRUE; // Value stored is UNKNOWN when Constraint_UNDEF EndOfDecode(Decode_UNDEF); when Constraint_NOP EndOfDecode(Decode_NOP);

bits(64) address; constant boolean privileged = PSTATE.EL != EL0; constant AccessDescriptor accdesc = CreateAccDescGPR(MemOp_STORE, nontemporal, privileged, tagchecked); if n == 31 then CheckSPAlignment(); address = SP[64]; else address = X[n, 64]; if !postindex then address = AddressAdd(address, offset, accdesc); bits(16) data; if rt_unknown then data = bits(16) UNKNOWN; else data = X[t, 16]; Mem[address, 2, accdesc] = data; if wback then if postindex then address = AddressAdd(address, offset, accdesc); if n == 31 then SP[64] = address; else X[n, 64] = address;