(江南计算技术研究所 江苏无锡 214083) (tanjian131@163.com)
出版日期: 2020-12-01基金资助:国家重点研发计划项目(2017YFB0202703)Data Constraint Generation Technology for Microprocessor Instruction Verification Based on SMT Solver
Tan Jian, Luo Qiaoling, Wang Liyi, Hu Xiahui, Fan Hao, Xu Zhan(Jiangnan Institute of Computing Technology, Wuxi, Jiangsu 214083)
Online: 2020-12-01Supported by:This work was supported by the National Key Research and Development Program of China (2017YFB0202703).摘要/Abstract
摘要： 处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足，提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法：利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例，并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率，提出了2种解决方法：首先利用时间阈值实现问题求解超时即终止的策略；其次是结合进程管理与线程管理技术，实现了指令功能约束并行求解框架，将串行求解任务分派给可并行执行的多个线程，提高了求解速度.该技术已成功应用于系统级验证中，有效提升了测试覆盖与质量，取得了很好的效益.
参考文献
相关文章 10
| [1] | 吴淇毓，周福才，王强，李宇溪. 可有效更新的低存储开销公共可验证数据库方案[J]. 计算机研究与发展, 2018, 55(8): 1800-1808. |
| [2] | 郭曦,王盼. 程序状态条件合并中变量隐式关联分析方法[J]. 计算机研究与发展, 2018, 55(10): 2331-2342. |
| [3] | 王翀,吕荫润,陈力,王秀利,王永吉,. SMT求解技术的发展及最新应用研究综述[J]. 计算机研究与发展, 2017, 54(7): 1405-1425. |
| [4] | 刘经德,陈振邦,王戟. 基于求解开销预测的符号执行搜索策略研究[J]. 计算机研究与发展, 2016, 53(5): 1086-1094. |
| [5] | 王勇献 张理论 刘 巍 车永刚 徐传福 王正华. CFD并行计算中的多区结构网格二次剖分方法与实现[J]. 计算机研究与发展, 2013, 50(8): 1762-1768. |
| [6] | 王文迪, 汤 文, 段 勃, 张春明, 张佩珩, 孙凝晖,. 基于Hash索引的高通量基因序列比对并行加速技术研究[J]. , 2013, 50(11): 2463-2471. |
| [7] | 赵云山 宫云战 周 傲 王 前 周虹伯. 静态缺陷检测中的误报消除技术研究[J]. , 2012, 49(9): 1822-1831. |
| [8] | 咸鹤群, 冯登国,. 外包数据库模型中的完整性检测方案[J]. , 2010, 47(6): 1107-1115. |
| [9] | 徐贵红, 张 健,. 基于约束的主动规则终止性分析[J]. , 2006, 43(5): 894-900. |
| [10] | 季晓慧, 张 健, . 一种求解混合约束问题的快速完备算法[J]. , 2006, 43(3): 551-556. |
PDF全文下载地址:
https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=4321
