VADDPD X30, X29, X10        // 6211950058d6
	VADDPD X12, X11, X28        // 6241a50858e4
	VADDPD X30, X11, X28        // 6201a50858e6
	VADDPD X12, X29, X28        // 6241950058e4
	VADDPD X30, X29, X28        // 6201950058e6
	VADDPD (AX), X29, X0        // 62f195005800
	VADDPD (AX), X1, X28        // 6261f5085820
	VADDPD (AX), X29, X28       // 626195005820
	VADDPD (AX), X29, X10       // 627195005810

		// Test AVX512 suffixes.
		{"VADDPD.A X0, X1, X2", `unknown suffix "A"`},
		{"VADDPD.A.A X0, X1, X2", `unknown suffix "A"; duplicate suffix "A"`},
		{"VADDPD.A.A.A X0, X1, X2", `unknown suffix "A"; duplicate suffix "A"`},
		{"VADDPD.A.B X0, X1, X2", `unknown suffix "A"; unknown suffix "B"`},
		{"VADDPD.Z.A X0, X1, X2", `Z suffix should be the last; unknown suffix "A"`},

	// Usage of rounding with invalid operands.
	VADDPD.RU_SAE X3, X2, K1, X1     // ERROR "unsupported rounding"
	VADDPD.RD_SAE X3, X2, K1, X1     // ERROR "unsupported rounding"
	VADDPD.RZ_SAE X3, X2, K1, X1     // ERROR "unsupported rounding"
	VADDPD.RN_SAE X3, X2, K1, X1     // ERROR "unsupported rounding"
	VADDPD.RU_SAE Y3, Y2, K1, Y1     // ERROR "unsupported rounding"
	VADDPD.RD_SAE Y3, Y2, K1, Y1     // ERROR "unsupported rounding"