Leitfliden der Informatik R. Drechsler/B. Becker Graphenbasierte Funktionsdarstellung Leitfiiden der Informatik Herausgegeben von Prof. Dr. Hans-Jurgen Appelrath, Oldenburg Prof. Dr. Volker Claus, Stuttgart Prof. Dr. Dr. h.c. mult. Gunter Hotz, Saarbrucken Prof. Dr. Lutz Richter, Zurich Prof. Dr. Wolffried Stucky, Karlsruhe Prof. Dr. Klaus Waldschmidt, Frankfurt Die Leitfaden der Informatik behandeln - Themen aus der Theoretischen, Praktischen und Technischen Informatik entsprechend dem aktuellen Stand der Wissenschaft in einer systemati schen und fundierten Darstellung des jeweiligen Gebietes. - Methoden und Ergebnisse der Informatik, aufgearbeitet und dargestellt aus Sicht der Anwendungen in einer fOr Anwender verstandlichen, exak ten und prazisen Form. Die Bande der Reihe wenden sich zum einen als Grundlage und Erganzung zu Vorlesungen der Informatik an Studierende und Lehrende in Informa tik-Studiengangen an Hochschulen, zum anderen an "Praktiker", die sich einen Uberblick uber die Anwendungen der Informatik( -Methoden) ver schaffen wollen; sie dienen aber auch in Wirtschaft, Industrie und Verwal tung tatigen Informatikern und Informatikerinnen zur Fortbildung in pra xisrelevanten Fragestellungen ihres Faches. Graphenbasierte Funktionsdarstellung Boolesche und Pseudo-Boolesche Funktionen Von Dr. phil. nat. Rolf Drechsler und Prof. Dr. rer. nat. Bernd Becker Universitat Freiburg B. G. Teubner Stuttgart 1998 Dr. phil. nat. Rolf Drechsler Geboren 1969 in Rtisselsheim. Studium der Informatik und Mathematik an der Johann Wolfgang Goethe-Universitat in Frankfurt am Main (1988 bis 1992), 1995 Promotion. Seit 1996 wiss. Assistent am Institut fUr Informatik der Albert-Ludwigs Universitat Freiburg. Prof. Dr. rer. nat. Bernd Becker Geboren 1954 in Hermeskeil. Studium der Mathematik und Informatik an der Uni versitat des Saari andes (1973 bis 1979). 1982 Promotion und 1988 Habilitation. Von 1989 bis 1995 Professor (Komplexitatstheorie und Effiziente Algorithmen) an der Johann Wolfgang Goethe-Universitat in Frankfurt am Main, seit 1995 Professor (Rechnerarchitektur) an der Albert-Ludwigs-Universitat in Freiburg. Die Deutsche Bibliothek - CIP-Einheitsaufnahme Drechsler, Rolf: Graphenbasierte Funktionsdarstellung : Boolesche und Pseudo Boolesche Funktionen / von Rolf Drechsler und Bernd Becker. - Stuttgart: Teubner, 1998 (Leitfiiden der Informatik) ISBN 978-3-519-02149-0 ISBN 978-3-663-01442-3 (eBook) DOI 10.1007/978-3-663-01442-3 Das Werk einschlieBlich aller seiner Teile ist urheberrechtlich geschiitzt. Jede Verwertung auBerhalb der engen Grenzen des U rheberrechtsgesetzes ist ohne Zustimmung des Verlages unzulassig und strafbar. Das gilt besonders fUr Vervielfaltigungen, Obersetzungen, Mikroverfilmungen und die Ein speicherung und Verarbeitung in elektronischen Systemen. © B. G. Teubner Stuttgart 1998 Gesamtherstellung: Zechnersche Buchdruckerei GmbH, Speyer Einband: Peter Pfitz, Stuttgart Fur M onika) Michael) Marvin und Miklas und Usch) Bastian) Ruben und Johanna Ach Gott! die Kunst ist lang; Und kurz ist unser Leben. Mir wird, bei meinem kritischen Bestreben, Doch oft urn Kopf und Busen bang. Wie schwer sind nicht die Mittel zu erwerben, Durch die man zu den Quellen steigt! Und eh man nur den halben Weg erreicht, MuB wohl ein armer Teufel sterben. Johann Wolfgang von Goethe, Faust I, 1808 Vorwort Kompakte Darstellung und effiziente Manipulation Boolescher Funktionen sind in vie len Bereichen, insbesondere des computergestutzten Schaltkreisentwurfes, zentrale Aufgaben. 1m Hinblick auf Anwendungen ist es dabei von groBem Inter esse, einen guten KompromiB zwischen den oben angesprochenen, sich "wider sprechenden" Zielen, Kompaktheit und EjJizienz, zu finden. Besonderer Beliebtheit erfreuen sich in dies em Zusammenhang die von Bryant 1986 eingefUhrten Ordered Binary Decision Diagrams (OBDDs): Sie werden ins besondere in den Bereichen Verijikation und Logiksynthese auch industriell er folgreich eingesetzt. Mit wachsender Zahl von Anwendungen sind auch inharente Nachteile sichtbar geworden und haben vor all em in den letzten drei Jahren zu Weiterentwicklungen des Basiskonzeptes gefUhrt. Dabei hat sich eine ganze Familie von graphenba sierten Funktionsdarstellungen entwickelt, dieje nach Anwendungsgebiet Vorteile gegenuber den klassischen OBDDs bieten. In dies em Buch wird eine Klassifizierung der verschiedenen Ansatze sowohl aus theoretischer wie auch praktischer Sicht gegeben. Es werden diverse Datenstruk turen fUr Boolesche (und Pseudo-Boolesche) Funktionen vorgestellt und deren Vor- und Nachteile untersucht. Das Buch wendet sich sowohl an den Einsteiger als einfuhrende Darstellung als auch an den erfahrenen Benutzer. Es werden ver schiedene Anwendungen diskutiert, die dem Leser ein tieferes Verstandnis der Materie ermoglichen. Grundlage des Buches ist sowohl die Dissertationsschrift des Erstautors als auch Materialien zu der Vorlesung "Datenstrukturen und effiziente Algorithmen" , die 8 der Zweitautor an der Johann Wolfgang Goethe-Universitat in Frankfurt am Main uber mehrere Jahre hinweg hielt. In diesem Zusammenhang sei unserem Fachkollegen Prof. Hans Eveking gedankt, der sich als Zweitgutachter zu obiger Dissertation zur Verfugung stellte. Weiterhin haben viele Diskussionen mit den Forschungsgruppen von Prof. Chri stoph Meinel, Prof. Paul Molitor und Prof. Ingo Wegener wesentlich zur Gestal tung des Buches beigetragen. Wir mochten all denen danken, die in den vergangenen Jahren intensiv durch Zu sammenarbeiten zu diesem Buch beigetragen haben: Stefan Eckrich, Reinhard Enders, Dr. Ralf Hahn, Thilo Harich, Dr. Joachim Hartmann, Harry Hengster, Andreas Hett, Stefan Horeth, Andrea Jahnke, Martin Keirn, Dr. Rolf Krieger, Mi chael Martin, Dirk Moller, Konrad Novak, Prof. Marek Perkowski, Tonja Pfeiffer, Stefan Ruppertz, Andisheh Sarabi, Horst Schafer, Michael Theobald, Dr. Ralph Werchner. Ohne ihre Hilfe ware die oftmals aufwendige Entwicklung und Um setzung der im folgenden beschriebenen Konzepte nicht in dieser Form moglich gewesen. Unser besonderer Dank gilt den Korrekturlesern Dr. Ursula Becker, Nicole Gockel, Wolfgang Gunther und Dr. Christoph Scholl fur die sorgfaltige Durch sicht des Buches und zahlreiche konstruktive Verbesserungsvorschlage. AbschlieBend danken wir dem Teubner Verlag, insbesondere Dr. Peter Spuhler, fur die reibungslose Zusammenarbeit und Prof. Gunter Hotz fUr vertrauensvolle Unterstutzung, nicht nUl" bei der Herausgabe des vorliegenden Buches. Freiburg im Breisgau, im November 1997 Rolf Drechsler Bernd Becker Inhaltsverzeichnis 1 Einleitung 13 2 Decision Diagrams 19 2.1 Einleitung 19 2.2 Boolesche Funktionen, Pseudo-Boolesche Funktionen 19 2.3 Grundlagen 24 2.4 Restriktionen 27 2.5 Reduktion 28 2.6 Aufgaben 34 3 Bit-level Decision Diagrams 37 3.1 Einleitung .. 37 3.2 Allgemeine Bemerkungen . 37 3.3 Binary Decision Diagrams 38 3.4 Functional Decision Diagrams 42 3.5 Kronecker Functional Decision Diagrams 43 3.6 Komplementierte Kanten . 44 3.7 Aufgaben 50 4 Word-level Decision Diagrams 51 4.1 Einleitung 51 4.2 Kantengewichte 52 10 INHALTSVERZEICHNIS 4.3 Multi-Terminal Binary Decision Diagrams 53 4.4 Edge-Valued Binary Decision Diagrams . 54 4.5 Multiplicative Binary Moment Diagrams 54 4.6 Kronecker Multiplicative Binary Moment Diagrams 55 4.7 Aufgaben ................. . 57 5 Darstellungsgro6e von Decision Diagrams 59 5.1 Einleitung ......... . 59 5.2 Bit-level Decision Diagrams 60 5.2.1 Wieviele bit-level DD-Typen gibt es? 60 5.2.2 Allgemeine T-Funktion . . . 65 5.2.3 Exponentielle Unterschiede . 70 5.2.4 Untere Schranken fur die GroBe von OBDDs und OpFDDs 79 5.3 Word-level Decision Diagrams 91 5.3.1 Einfache Uberlegungen 91 5.3.2 Kantengewichte. 92 5.3.3 Zerlegungstypen. 92 5.4 Uberblick 94 5.5 Aufgaben 96 6 Algorithmen fUr Decision Diagrams 99 6.1 Einleitung .......... . 99 6.2 Auswertung und Erfiillbarkeit 100 6.3 Syntheseoperationen 102 6.3.1 OBDDs ... 102 6.3.2 OFDDs und OKFDDs 108 6.3.3 Word-level DDs 115 6.4 Minimieren von DDs 115 6.4.1 Vertauschen von Variablen . 115 INHALTSVERZEICHNIS 11 6.4.2 Exaktes Minimieren 119 6.4.3 Heuristisches Minimieren . 121 6.5 Aufgaben ... 128 7 Implementierung 131 7.1 Einleitung ........ . 131 7.2 Ein einfaches BDD-Paket . 131 7.3 Speicherverwaltung 143 7.4 Verfiigbare Pakete . 144 7.5 Aufgaben ..... 144 8 Experimentelle Ergebnisse 147 8.1 Einleitung ........ . 147 8.2 Bit-level Decision Diagrams 147 8.2.1 Exakte Minimierung 147 8.2.2 Heuristische Methoden 148 8.3 Word-level Decision Diagrams 154 8.4 Aufgaben ........... 159 9 Ausblick und weitere Anwendungen 161 9.1 Einleitung.. 161 9.2 Logiksynthese 161 9.2.1 Minimierung zweistufiger Schaltungen . 161 9.2.2 Synthese von mehrstufigen (testbaren) Schaltungen 164 9.3 Testen ........................ . 166 9.3.1 Testmustergenerierung und Fehlersimulation 166 9.3.2 Initialisierung endlicher Automaten 167 9.3.3 Built-in-Self-Test 167 9.4 Verifikation . . . . . . . 168 9.4.1 Verifikation kombinatorischer Schaltkreise 168