Simulation is the major technique used for processor verification.In the late of the verification process

simulation requires a lot of expert time and computer resources to verify residual complicated functional points

which slows down the verification progress.This paper introduces a test generation method based on model checking engine to address this problem.First

an abstract microprocessor model focuses on these uncovered functional points is constructed using local modeling strategy.Second

model checker reads this abstract model and automatically produces test generator directives.Finally

these directives guide random test generator to generate test programs that cover the specified functional points.Experiments on verifying PKUnity UniCore32 microprocessor demonstrated that this method spent little time to cover these uncovered coverage tasks and increased the verification efficiency.