基于K Framework的向量化机器学习指令的语义形式化
作者:
作者单位:

作者简介:

通讯作者:

施晓牧,E-mail:xshi0811@gmail.com

中图分类号:

TP311

基金项目:

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


Semantics Formalization for Vectorized Machine Learning Instructions in K Framework
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

黄厚华,刘嘉祥,施晓牧.基于K Framework的向量化机器学习指令的语义形式化.软件学报,,():0

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号