Efficient Distributed Bounded Property Checking

Abstract

Today, verification of industrial size designs like multi-million gate ASICs (Application Specific Integrated Circuit) and SoC (System-on-a-Chip) processors consumes up to 75%of the design effort. The trend to augment functional verification with formal verification tries to alleviate this problem. Efficient property checking algorithms based on binary decision diagrams (BDDs) and satisfiability (SAT) solvers allow the automatic verification of medium-sized designs. However, the steadily increasing design sizes still leave verification as the major bottleneck, because formal methodologies do not yet scale to very large designs.

To address these problems researchers came up with the idea of combining symbolic simulation and bounded model checking on-the-fly. The current tools pioneer in handling comparatively larger designs by partitioning the state set and they can be represented using partitioned ordered BDDs (POBDDs). These partitions will be explored in a divide-and-conquer manner. However, still they face memory exhaustion for very large models due to the BDD explosion problem. Even the SAT based bounded model checking (BMC) can search up to a maximum depth allowed by the physical memory on a single server. These observations motivated the parallelization of symbolic state space traversal algorithms. Distributed algorithms verify larger models and return results faster than sequential versions. Existing schemes for parallelizing BDD-based verification algorithms often suffer from state overlap or duplicate work, cross over states among partitions, inefficient work distribution, improper load balancing, synchronicity and communication overhead. The algorithms concentrate heavily either on reachability (validation) or falsification but not both together.

My main contributions include a dynamic overlap reduction and a hybrid distributed algorithms. The dynamic overlap reduction technique smoothens the state space traversal of each network node by removing the state overlap that it suffers from. The removal of overlap works in an asynchronous manner, i.e., with out waiting for other processors to complete their image computations. This method has the natural side effect of dynamic load balancing among network nodes, i.e., the nodes that deal with a large state space at one time point will be later assigned a small state space and vice versa. Since all the nodes perform asynchronous state space traversal on their whole state subsets, the method is best suitable for validation.

The hybrid method is an asynchronous distributed algorithm, suited for both fast error detection and complete validation. This approach combineswell known windowing and dynamic overlap reduction techniques. The windowing technique has partitions that are identified by unique combination of variables. Each window restricts its state space at regular intervals to keep the reachable state space within it’s window region. The real state space is discriminated by the window as owned and non-owned states. The nodes on the cluster machine are employed with two different types of tasks. Some nodes, windows aim at faster falsification on the basis of the windowing technique. The other type of nodes called helpers are intending for validation on the basis of the dynamic overlap reduction. All the network nodes asynchronously traverse their local state spaces for both error states detection and reachability of a time bound. Thus, the hybrid algorithm efficiently combines both windowing and dynamic overlap reduction techniques to obtainmore synergy and gains the advantages of using both the approaches. Further, the algorithm expedites the verification process by reassigning the work to idle nodes as quickly as possible. As a result it avoids the wasted computation power and makes the system work efficient.

The dynamic overlap reduction and hybrid algorithms are best suitable for homogeneous system configurations like a cluster. However, this thesis also presents a grid-based parallelization algorithm which is suitable for fast falsification of very large designs. In addition, all the parallel algorithms in this thesis partition the state space using the Minimal overlap algorithm which pioneers in statically minimizing the cross over states or state overlap among the partitions.

The parallel algorithms speedup the distributed verification and automatically checks the correctness of very large hardware designs. The distributed computation shows approximately linear speedups in execution time and enables faster verification of properties. As a supplement, this thesis also presents a novel distributed algorithm, which uses mixed forward and backward traversal mechanism for Black Box verification.

Heutzutage benötigt die Verifikation von industriellen Designswie 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. Aktuelle Tools sind in der Lage vergleichsweise große Designs durch Partitionierung des Zustandsraums zu bewältigen. Der Zustandsraum wird dabei auf partitionierte geordnete BDDs (POBDDs) abgebildet und mit einer Teile-und-Herrsche Strategie durchsucht. Trotzdem kämpfen diese Tools immer noch mit Speicherproblemen bei sehr großen Modellen bedingt durch den bei BDDs auftretenden Speicher überlauf. Auch SAT-basierende bounded model checking Tools (BMC) sind in der Suchtiefe beschränkt, durch den physikalisch zur Verfügung stehenden Hauptspeicher eines einzelnen Rechenknotens. Diese Beobachtungen motivierten die Parallelisierung der Algorithmen zur Traversierung von symbolischen Zustandsräumen. 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 auf beides zusammen.

Meine Hauptarbeit beinhaltet eine dynamische Reduzierung der Überlappung (dynamic overlap reduction) und einen hybriden verteilten Algorithmus. Die Technik zur dynamischen Reduzierung von Überlappungen verbessert die Traversierung des Zustandsraumes von jedem Rechenknoten durch Reduzierung der Überlappungen. Die Überlappungs-Reduzierung arbeitet asynchron d.h. ohne zu warten bis andere Knoten ihre Image Berechnung beendet haben. Diese Methode hat den natürlichen Seiteneffekt der dynamischen Lastbalancierung zwischen den Netzwerkknoten, d.h. die Knoten, die zu Beginn einen großen Teil des Zustandsraums bekommen, werden im nächsten Durchlauf einen kleineren Teil bekommen und vice versa. Da alle Knoten eine asynchrone Exploration ihres eigenen Zustandsraums durchführen ist diese Methode sehr gut zur Validierung geeignet.

Bei der hybriden Methode handelt es sich um einen asynchronen verteilten Algorithmus, der sowohl geeignet ist zum schnellen Auffinden von Fehlern als auch zur vollständigen Verifikation. Der 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 in unregelmäßigen Abständen, um den Erreichbaren Zustandsraum in den eigenen window Grenzen zu halten. Der gesamte Zustandsraum wird eingeteilt in benutzte und noch nicht benutzte Zustände. Den Knoten des Rechen-Clusters werden zwei unterschiedliche Aufgaben zugeteilt. Einige Knoten, windows, versuchen schnell Fehler zu finden auf Basis der windowing Technik. Der andere Typ von Knoten, helper, versucht zu validieren auf Basic der dynamischen Überlappungs-Reduzierung. Alle Netzwerkknoten traversieren asynchron ihren lokalen Zustandsraum mit zwei Zielen: auffinden von Fehlerzuständen und Erreichbarkeit einer Zeitschranke. Somit kombiniert der hybride Algorithmus auf effiziente Weise sowohl windowing als auch dynamische Überlappungs-Reduzierung, um dadurch mehr Synergien zu erzeugen und um die Vorteile beider Methoden zu nutzen. Der Algorithmus beschleunigt außerdem den Verifikationsprozess durch ein so schnell wie möglich erneute Verteilung der Arbeit auf im Leerlauf befindliche Knoten. Als Ergebnis wird dadurch die Verschwendung von Rechenleistung verhindert und die Effizienz des Systems gesteigert.

Beide Ansätze sind bestens geeignet für homogene System-Konfigurationen wie z.B. Cluster. Außerdem wird innerhalb der Dissertation auch ein Grid-basierender Algorithmus vorgestellt, welcher für die schnelle Fehlersuche in großen Entwürfen geeignet ist. Zusätzlich benutzen alle parallelen Algorithmen in dieser Dissertation den Minimal overlap Algorithmuswelcher eine statische Minimierung der Kreuz-Überlappungs-Zustände bzw. der Überlappungszustände zwischen den Partitionen durchführt.

Die parallelen Algorithmen beschleunigen die verteilte Verifikation und überprüfen automatisch die Korrektheit von sehr großen Hardware-Designs. Die verteilte Berechnung zeigt annähernd linearen Speedup in der Ausführungszeit und ermöglicht die schnellere Verifikation von Eigenschaften. Als Ergänzung dieser Arbeit wird ein neuer verteilter Algorithmus präsentiert, welcher einen gemischten Vorwärts- und Rückwärts traversierungs-Mechanismus benutzt zur Black- Box-Verifikation.