Synchronized Generation of Directed Tests Using Satisfiability Solving

Directed test generation is important for the functional verification of complex system-on-chip designs. SAT based bounded model checking is promising for counter example generation which can be used in directed testing. Existing research has explored two directions to accelerate the SAT solving process: learning during solving of one property with different bounds, or solving multiple properties with known bounds. This paper combines the advantages of both approaches by introducing a novel SAT-solving technique which exploits the similarities among SAT instances for multiple properties and bounds on the same design. The proposed technique ensures that the knowledge obtained in previous solving iterations be shared across different bounds as well as between different properties. Our experimental results demonstrate that our approach can significantly reduce overall test generation time (on average 10 times) compared to existing methods.