Verifikation unvollständiger Schaltkreise

Hochschulschrift

Zusammenfassung: Die vorliegende Arbeit betrachtet verschiedene Aspekte der formalen Verifikation unvollständiger Schaltkreise. Unvollständige Schaltkreise sind sequentielle Schaltkreise, in denen einige Teile unbekannt sind; wir modellieren diese unbekannten Bereiche durch „Black Boxes“ mit unbekanntem sequentiellen Verhalten. Wir nehmen an, dass Black Boxes durch beliebige sequentielle Schaltkreise mit der gleichen Anzahl von Ein- und Ausgängen ersetzt werden können. Es gibt mehrere Anwendungen für die formale Verifikation unvollständiger Schaltkreise, wie etwa die Verifikation noch nicht fertiggestellter Designs in einem frühen Stadium der Entwicklung, Fehlerlokalisation in einem fehlerhaften Schaltkreis und die Abstraktion komplexer Teilschaltkreise zur Beschleunigung der Verifikation. Zuerst betrachten wir das grundlegende Problem der symbolischen CTL-Modellprüfung unvollständiger Schaltkreise; dabei untersuchen wir zu einem gegebenen CTL-Ausdruck zwei Fragestellungen: Zum einen, ob sich ein unvollständiger Schaltkreis so vervollständigen lässt, dass der CTL-Ausdruck erfüllt wird („Ist der CTL-Ausdruck realisierbar?“) und zum anderen, ob der CTL-Ausdruck für alle Vervollständigungen des unvollständigen Schaltkreises erfüllt wird („Ist der CTL-Ausdruck valide?“). Zur Beantwortung dieser Fragen verwenden wir mehrere approximative Modellierungen der Black Boxes, auf Grundlage derer wir obige Fragen korrekt beantworten können. Zusätzlich betrachten wir eine Methode zur exakten Beantwortung der beiden Fragen unter der Annahme, dass die Ersetzungen der Black Boxes bezüglich der Anzahl der hinzugefügten Flipflops beschränkt sind. Für den Fall, dass die durch Black Boxes modellierten Bereiche im Schaltkreis nicht vollständig unbekannt sind, betrachten wir die Möglichkeit, „Annahmen“ über das sequentielle Verhalten der Black Boxes zu spezifizieren und in der Modellprüfung zu berücksichtigen. Zusätzlich untersuchen wir Heuristiken, die aus einer Menge von Annahmen diejenigen auswählen, die zum Beweis der Realisierbarkeit bzw. Validität eines CTL-Ausdrucks ausreichen. Erfüllt ein Schaltkreis eine Spezifikation nicht, werden üblicherweise Gegenbeispiele generiert, die dem Entwickler den Fehler illustrieren und ihm helfen, den Fehler zu verstehen. Hierzu sollten Gegenbeispiele möglichst verständlich sein und über so wenige Komponenten wie möglich argumentieren. In diesem Kontext lassen sich Black Boxes einsetzen, um einzelne Komponenten für die Gegenbeispielsberechnung auszublenden, so dass das resultierende Gegenbeispiel eine verringerte Anzahl von Komponenten verwendet und damit das Verstehen des Fehlers vereinfacht. Schließlich betrachten wir noch eine Methode, für unvollständige Schaltkreise die BDD-basierte Symbolische Modellprüfung mit dem SAT-basierten Bounded Model Checking (BMC) zu verknüpfen und dabei die Vorteile der beiden Methoden zu vereinen. Zu jedem der angesprochenen Themen betrachten wir eine Reihe experimenteller Ergebnisse, die die Effektivität und Realisierbarkeit der vorgestellten Methoden zeigen
Zusammenfassung: In this work, different aspects of formal verification of incomplete designs are investigated. Incomplete designs are sequential circuits in which some parts are unknown. These unknown parts are considered to be “Black Boxes” with unknown sequential behavior that can be replaced by any other sequential circuit with the same number of inputs and outputs as the according Black Box.There are many applications for formal verification applied to incomplete designs, such as early verification checks on unfinished designs, error localization in faulty designs, and the abstraction of complex parts of a design in order to simplify the model checking task.First, we consider the problem of performing CTL model checking for an incomplete circuit. For this, we examine two questions: Is there a completion of the incomplete circuit so that the CTL property is satisfied (“Is the CTL property realizable?”) and is the CTL property satisfied for all possible completions of the incomplete circuit (“Is the CTL property realizable?”). A series of approximate, yet sound algorithms to analyze incomplete designs with increasing quality and computational resources is presented. Additionally, we consider a concept for exact symbolic model checking of incomplete designs containing several Black Boxes with bounded memory.Due to its approximative nature, symbolic model checking for incomplete designs may be unable to provide proofs when the approximations are too coarse. Therefore, we investigate a method to include assumptions about the Black Box behavior into the model checking routine. Additionally, we consider different heuristic-based approaches to automatically select a subset of local component assumptions that is sufficient to prove or disprove a given CTL property.If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. The concept of Black Boxes can also be used to mask out components for counterexample computation. By doing so, the resulting counterexample argues about a reduced number of components in the system facilitating the tasks of understanding and correcting the error.Finally, we consider a method that integrates BDD-based symbolic model checking into SAT-based bounded model checking for incomplete designs, taking advantage of what each type of model checking technique has to offer. For this, the BDD-based model checking is deeply integrated into the SAT solving routine and also provides minimized conflict clauses, providing valuable information to the SAT solver.For each of these aspects of formal verification of incomplete designs, a series of experimental results demonstrates the effectiveness and feasibility of the considered methods

Angaben zum Objekt

• Standort: Deutsche Nationalbibliothek Frankfurt am Main
• Umfang: Online-Ressource
• Sprache: Deutsch
• Anmerkungen: Albert-Ludwigs-Universität Freiburg, Dissertation, 2015

Klassifikation und Themen

• Klassifikation: Mathematik
• Schlagwort: Logische Schaltung ; Model Checking ; Blackbox ; Gegenbeispiel ; Verifikation ; Lemma ; Verifikation

Beteiligte, Orts- und Zeitangaben

• Ereignis: Veröffentlichung
• (wo): Freiburg
• (wer): Universität
• (wann): 2015
• Urheber: Nopper, Tobias Johannes
• Beteiligte Personen und Organisationen: Scholl, Christoph

Weitere Informationen

• DOI: 10.6094/UNIFR/10154
• URN: urn:nbn:de:bsz:25-freidok-101548
• Rechteinformation: Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Letzte Aktualisierung: 25.03.2025, 13:50 MEZ