ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2020, Vol. 57 ›› Issue (12): 2694-2702.doi: 10.7544/issn1000-1239.2020.20190718

Previous Articles     Next Articles

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

Tan Jian, Luo Qiaoling, Wang Liyi, Hu Xiahui, Fan Hao, Xu Zhan   

  1. (Jiangnan Institute of Computing Technology, Wuxi, Jiangsu 214083)
  • Online:2020-12-01
  • Supported by: 
    This work was supported by the National Key Research and Development Program of China (2017YFB0202703).

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.

Key words: instruction function, datapaths, constraint solving, SMT solver, verification data, parallel acceleration

CLC Number: