Efficient Distributed Bounded Property Checking

• Antragsteller: Professor Dr. Wolfgang Rosenstiel (†)
• Fachliche Zuordnung: Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing ; Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2009 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 88389064

Heutzutage benötigt die Verifikation von industriellen Designs wie z.B. ASICs (Application Specific Integrated Circuit) und SoC (System-on-a-Chip) bis zu 75 % der Entwicklungskosten. Der Trend funktionale Verifikation durch formale Verifikation zu erweitern versucht dieses Problem zu lösen. Effiziente Algorithmen basierend auf BDDs (Binary Decision Diagrams) und SAT (Satisfiability) erlauben die automatische Verifikation von mittelgroßen Designs. Durch die ständig wachsenden Designgrößen bleibt die Verifikation trotzdem der Flaschenhals, da formale Methoden noch nicht für sehr große Designs skalieren. Um diese Probleme zu beheben wurde in der Forschung die Idee entwickelt symbolic simulation und bounded model checking direkt zu kombinieren. Ungeachtet dessen versuchen heutige Tools durch Partitionierung des Zustandsraums und durch Exploration dieser Partitionen (POBDDs) durch eine Teile-und-Herrsche Strategie immer größere Designs zu verifizieren. Trotzdem kämpfen diese Tools immer noch mit Speicherproblemen und sind daher nicht in der Lage sehr große Designs zu überprüfen. Diese Beobachtung motivierte die Parallelisierung der Algorithmen zur symbolischen Zustandsraumexploration. Die verteilten Algorithmen können größere Modelle verifizieren und liefern die Ergebnisse schneller als die sequentiellen Versionen. Existierende Methoden zur Parallelisierung von BDD-basierenden Verifikationsalgorithmen kämpfen oft mit Zustandsraumüberlappungen, ineffizienter Verteilung, schlechter Lastbalancierung, sowie Synchronisierungs- und Kommunikations-Overhead. Die Algorithmen konzentrieren sich entweder auf Erreichbarkeit (Validierung) oder auf das schnelle Finden von Fehlern aber nicht beides zusammen. Die Hauptarbeit des Antragstellers konzentriert sich auf hybride, hauptsächlich asynchrone verteilte Algorithmen, die sich sowohl zur schnellen Fehlerauffindung als auch zur kompletten Validierung eignen. Dieser Ansatz kombiniert bereits bekannte windowing und dynamic overlap reduction Techniken. Der windowing Ansatz benutzt Partitionen die durch eindeutige Variablenkombinationen identifiziert werden. Jedes window beschränkt seinen Zustandsraum, um die Eindeutigkeit zu gewährleisten. Der gesamte Zustandsraum wird eingeteilt in benutzte und noch nicht benutzte Zustände. Die dynamic overlap reduction Technik verbessert die Zustandsraumtraversierung von jeder Partition durch Beseitigung des Overlaps. Der Ansatz skaliert die verteilte Verifikation und überprüft automatisch die Korrektheit von sehr großen Hardware-Designs. Die verteilte Berechnung zeigt annähernd linearen Speedup in Bezug auf die Ausführungszeit und beschleunigt die Verifikation von Eigenschaften. Ein Tool oder eine Methode, die eine schnelle Verifikation erlaubt, ist immer eine bevorzugte Wahl für die Industrie. Das Ziel dieser Arbeit ist es mit sehr großen Designs zu arbeiten und diese schnell zu verifizieren. Dazu sollen die existierenden Ideen, Tools und Erfahrungen angepasst und auf echte industrielle Designs angewandt werden. Die Industrie hat immer noch Probleme sehr große Designs zu verifizieren. Motiviert durch diesen Umstand soll diese Arbeit darüber hinaus durch Transfer des Wissens und der Erfahrungen des Autors, die er im Laufe seiner Promotion gesammelt hat, eine Verbesserung für die Industrie bringen. Es ist sehr wichtig das industrielle Umfeld zu nutzen und die daraus resultierenden Erfahrungen anzuwenden, um die eigenen Forschungsschwerpunkte zu erweitern und zielgerichtet zu verbessern.

• DFG-Verfahren: Sachbeihilfen (Transferprojekt)
• Beteiligte Institution: Robert Bosch GmbH; Geschäftsbereich Automotive Electronics