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

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.