基于SMT求解器的微处理器指令验证数据约束生成技术  

Data Constraint Generation Technology for Microprocessor Instruction Verification Based on SMT Solver

作　　者：谭坚[1] 罗巧玲 王丽一[1] 胡夏晖 范昊[1] 徐占[1] Tan Jian;Luo Qiaoling;Wang Liyi;Hu Xiahui;Fan Hao;Xu Zhan(Jiangnan Institute of Computing Technology,Wuxi,Jiangsu 214083)

机构地区：[1]江南计算技术研究所,江苏无锡214083

出　　处：《计算机研究与发展》2020年第12期2694-2702,共9页Journal of Computer Research and Development

基　　金：国家重点研发计划项目(2017YFB0202703)。

摘　　要：处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法:首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益.During the development of the processor,it is necessary to fully verify the instructions datapaths.The existing simulation verification methods have insufficient functional coverage in terms of instruction result operands constraints,relationship constraints between operands,and internal constraints of instructions,etc.This paper proposes an instruction constraint solving method based on satisfiability modulo theory(SMT)solver.The SMT solver is introduced to convert the instruction function verification tasks into constraint satisfaction problems.Constraint satisfaction problem techniques are used to generate validation tuple data,which can be used to verify the functional correctness of the instructions set.The modeling processes and examples are given in four aspects:the instruction result operand constraints,the instruction operand constraints,the instruction internal constraints,and float-pointing instructions operand constraints.In order to improve the modeling efficiency,we propose two strategies.First,once the time threshold is reached,the current process is terminated;second,using process management and thread management technology,a parallel solution framework for instruction function constraints is implemented,and a series of serial solving tasks are assigned to multiple threads that can be executed in parallel,and the speed of solution is accelerated under the conditions of the same constraints coverage.Our experiences show that under the right circumstances,instruction constraint solving technology based on SMT provides technical support for system-level functional verification to achieve test coverage of complex scenarios.

关 键 词：指令功能 数据路径 约束求解 SMT求解器 验证数据 并行加速 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]