Path Constraint Solving Based Test Generation for Hard-to-Reach States

Test generation for hard-to-reach states has been one of the hardest tasks in functional verification. In this paper, we present PACOST, a PAth Constraint Solving based Test generation method which operates in an abstraction-guided simulation framework to cover hard-to-reach states. PACOST combines concrete simulation and symbolic simulation in a path constraint solver to generate a set of valid input vectors for exploring different simulation paths, followed by next state selection considering abstract distances. In addition, two backtracking strategies are proposed to alleviate the dead end problem and ensure fast converge to the target state. Experimental results show that PACOST is effective in covering hard-to-reach states.