基于K Framework的向量化机器学习指令语义形式化

Semantics Formalization of Vectorized Machine Learning Instructions in K Framework

ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术,并命名为ARM Helium,声明能为ARM Cortex-M处理器提升达15倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟程序,片上应用程序开发的依据,是程序正确性基本保障.主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究.基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码,并将其转换为形式化语义转换规则.通过K Framework提供的可执行框架利用测试用例,验证机器学习指令算数运算执行的正确性.

ARM develops an M-Profile vector extension solution in terms of ARMv8.1-M micro processor architecture and names it ARM Helium.It is declared that ARM Helium can increase the machine learning performance of the ARM Cortex-M processor by up to 15 times.As the Internet of Things develops rapidly,the correct execution of microprocessors is important.In addition,the official manual of instruction sets provides a basis for developing chip simulators and on-chip applications,and thus it is the basic guarantee of program correctness.This study introduces these mantic correctness of vectorized machine learning instructions in the official manual of the ARMv8.1-M architecture by using K Framework.Furthermore,the study automatically extracts pseudo codes describing the vectorized machine learning instruction operation based on the manual and then formalizes them in semantics rules.With the executable framework provided by K Framework,the correctness of machine learning instructions in arithmetic operation is verified.