A robust and scalable technique for the constraints solving problem in high-level verification

Constraints solving is an important problem in a random simulation-based functional verification methodology. Constraints are used to model the environmental restrictions of the design under verification and the job of the constraints solver is to produce multiple random solutions that satisfy the constraints. We present RACE, a new word-level ATPG-based system for solving combinational constraint expressions. RACE builds a high-level circuit model to represent the constraints and implements a branch-and-bound algorithm to solve them. Experimental results on industrial test cases demonstrate the effectiveness of RACE. RACE has been successfully used for random stimulus generation in the context of a commercial high-level test-bench automation tool with simulation for RTL verification.