摘要:
处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足，提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法：利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例，并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率，提出了2种解决方法：首先利用时间阈值实现问题求解超时即终止的策略；其次是结合进程管理与线程管理技术，实现了指令功能约束并行求解框架，将串行求解任务分派给可并行执行的多个线程，提高了求解速度.该技术已成功应用于系统级验证中，有效提升了测试覆盖与质量，取得了很好的效益.
Abstract:
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.
百度学术
下载:
