VPEXTRW $17, X20, (SP)(AX*2)      // 62e37d0815244411 or 62e3fd0815244411
	VPEXTRW $127, X20, (SP)(AX*2)     // 62e37d081524447f or 62e3fd081524447f
	// EVEX: embedded zeroing.
	VADDPD.Z X30, X1, K7, X0  // 6291f58f58c6
	VMAXPD.Z (AX), Z2, K1, Z1 // 62f1edc95f08
	// EVEX: embedded rounding.
	VADDPD.RU_SAE Z3, Z2, K1, Z1   // 62f1ed5958cb
	VADDPD.RD_SAE Z3, Z2, K1, Z1   // 62f1ed3958cb
	VADDPD.RZ_SAE Z3, Z2, K1, Z1   // 62f1ed7958cb