TIGUAN: Thread-parallel Integrated test pattern Generator Utilizing satisfiability ANalysis

Abstract:
Wir stellen den automatischen Testmustergenerator TIGUAN vor, der auf einem thread-parallelen SAT-Solver basiert. Durch eine enge Integration von SAT-Engine und ATPG-Algorithmus und einen sorgfältig abgewogenen Einsatz unterschiedlicher Optimierungstechniken können große industrielle Schaltkreise ohne Abbrüche (Aborts) verarbeitet werden. Ferner wird eine Laufzeitverbesserung gegenüber vergleichbaren Werkzeugen erreicht. Es stellt sich heraus, dass die während der Testmustergenerierung entstehenden SAT-Instanzen sehr heterogene Eigenschaften aufweisen. Die Mehrzahl der Instanzen wird in sehr kurzer Zeit gelöst. Für solche Instanzen sind die in den letzten Jahren entwickelten Optimierungstechniken etwa im Bereich der Präprozessierung eher kontraproduktiv, da der Aufwand die erreichte Gesamtbeschleunigung oft übersteigt. Dies gilt im wesentlichen auch für die Option der Thread-Parallelität. Bei den schwer entdeckbaren Fehlern können hingegen durch die Parallelisierung Laufzeitvorteile realisiert werden.