ARM's Armv8.1-M architecture and the Arm Helium technology of the M-Profile vector extension solution have been declared to increase the machine-learning performance of the Arm Cortex-M processor up to 15 times. With the rapid development of the Internet of Things, the correct execution of the microprocessor is important. Since the development of chip simulators or programs on chip is relied on the official reference manual, it is also important to ensure its correctness. This paper introduces the correctness verification of the vectorized machine-learning instructions in the official reference manual of the Armv8.1-M architecture. We automatically extracted the operation pseudo-code of the vectorized machine-learning instructions, and then formalized them in semantics rules. With the executable framework provided by K Framework, the formalized semantics rules can be executed and tested by the benchmarks.