x29 := (uint64(p384Uint1(x28)) + x8)
	var x30 uint64
	_, x30 = bits.Mul64(x17, 0x100000001)
	var x32 uint64
	var x33 uint64
	x33, x32 = bits.Mul64(x30, 0xffffffffffffffff)
	var x34 uint64
	var x35 uint64
	x35, x34 = bits.Mul64(x30, 0xffffffffffffffff)
	var x36 uint64
	var x37 uint64
	x37, x36 = bits.Mul64(x30, 0xffffffffffffffff)
	var x38 uint64
	var x39 uint64

	// EVEX: High-16 X registers.
	VADDPD X30, X1, X0          // 6291f50858c6
	VADDPD X2, X29, X0          // 62f1950058c2
	VADDPD X30, X29, X0         // 6291950058c6
	VADDPD X2, X1, X28          // 6261f50858e2
	VADDPD X30, X1, X28         // 6201f50858e6
	VADDPD X2, X29, X28         // 6261950058e2
	VADDPD X30, X29, X28        // 6201950058e6
	VADDPD X30, X11, X10        // 6211a50858d6

	VPSHRDQ $42, X8, X14, K3, X30                      // 62438d0b73f02a
	VPSHRDQ $42, -7(DI)(R8*1), X14, K3, X30            // 62238d0b73b407f9ffffff2a
	VPSHRDQ $42, (SP), X14, K3, X30                    // 62638d0b7334242a
	VPSHRDQ $42, X14, X11, K3, X30                     // 6243a50b73f62a
	VPSHRDQ $42, X19, X11, K3, X30                     // 6223a50b73f32a