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

摘要

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 sorgfaltig abgewogenen Einsatz unterschiedlicher Optimierungstechniken konnen grosse industrielle Schaltkreise ohne Abbruche (Aborts) verarbeitet werden. Ferner wird eine Laufzeitverbesserung gegenuber vergleichbaren Werkzeugen erreicht. Es stellt sich heraus, dass die wahrend der Testmustergenerierung entstehenden SAT-Instanzen sehr heterogene Eigenschaften aufweisen. Die Mehrzahl der Instanzen wird in sehr kurzer Zeit gelost. Fur solche Instanzen sind die in den letzten Jahren entwickelten Optimierungstechniken etwa im Bereich der Praprozessierung eher kontraproduktiv, da der Aufwand die erreichte Gesamtbeschleunigung oft ubersteigt. Dies gilt im wesentlichen auch fur die Option der Thread-Parallelitat. Bei den schwer entdeckbaren Fehlern konnen hingegen durch die Parallelisierung Laufzeitvorteile realisiert werden.