软件学报

作者：黄厚华，刘嘉祥，施晓牧

单位：黄厚华，深圳大学 计算机与软件学院, 广东 深圳 51806011,刘嘉祥，深圳大学 计算机与软件学院, 广东 深圳 51806002,施晓牧，深圳大学 计算机与软件学院, 广东 深圳 51806003

关键词：ARMv8.1-M架构;向量化指令;机器学习;K Framework;形式化语义

基金：深圳市科创委基础研究面上项目(JCYJ20210324094202008);国家自然科学基金(62002228);深圳市高等院校稳定支持计划(20200810045225001)

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

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期