0000nnnnmmmm1111 macl ← ZeroExtend32(MACL); mach ← ZeroExtend32(MACH); s ← ZeroExtend1(S); m_field ← ZeroExtend4(m); n_field ← ZeroExtend4(n); m_address ← SignExtend32(Rm); n_address ← SignExtend32(Rn); value2 ← SignExtend32(ReadMemory32(ZeroExtend32(n_address))); n_address ← n_address + 4; IF (n_field = m_field) { m_address ← m_address + 4; n_address ← n_address + 4; } value1 ← SignExtend32(ReadMemory32(ZeroExtend32(m_address))); m_address ← m_address + 4; mul ← value2 × value1; mac ← (mach << 32) + macl; result ← mac + mul; IF (s = 1) IF (((result ⊕ mac) ∧ (result ⊕ mul))< 63 FOR 1 > = 1) IF (mac< 63 FOR 1 > = 0) result ← (1 << 47) - 1; ELSE result ← - (1 << 47); ELSE result ← SignedSaturate48(result); macl ← result; mach ← result >> 32; Rm ← Register(m_address); Rn ← Register(n_address); MACL ← ZeroExtend32(macl); MACH ← ZeroExtend32(mach);