Theorie des Schaltkreisentwurfs und der Schaltkreisverifikation

Wintersemester 2005/06

Beate Bollig

Termine

Wann? Wo? Wer?
Vorlesungen: Mo 16.00 - 18.00 OH 14 304 Beate Bollig
Do 8:30 - 10.00 OH 14 304 Beate Bollig
Übung: Do 10:00 - 12:00 OH 14 304 Beate Bollig

Die erste Vorlesung findet am 17. Oktober 2005 statt.
Ab dem 28.11.2005 findet die Veranstaltung in der Otto Hahn Str. 14 statt.

Inhalt

Die Vorlesung Theorie des Schaltkreisentwurfs und der Schaltkreisverifikation beschäftigt sich mit dem Entwurf und der Verifikation von Hardware. Auch wenn sich in der Berufswelt mehr Informatikerinnen und Informatiker mit Softwarefragen als mit Hardwarefragen befassen, ist doch klar, dass vieles, was heute mit Rechnern realisiert werden kann, nur durch Erfolge im Hardwarebereich möglich wurde. Immer größere Schaltungen mit einer immer größer werdenden Anzahl von logischen Bausteinen können auf einem Chip integriert werden. Die Schaltungen sind so groß, dass ad-hoc Methoden für ihren Entwurf und ihre Verifikation nicht mehr ausreichen. Die Vorlesung beschäftigt sich mit dem Entwurf und der Analyse von Algorithmen für die beim Hardwareentwurf und bei der Hardwareverifikation anfallenden Probleme.

Beim Entwurf guter Hardware hat man viele Probleme, die gleichzeitig gelöst werden müssen. Die Anzahl logischer Bausteine oder anderer Hardwarekomponenten, die Rechenzeit, d.h., die Tiefe bzw. Verzögerung von Schaltkreisen und die benötigte Chipfläche sollen minimiert werden und zugleich soll der entworfene Schaltkreis leicht zu testen sein. Es ist meist nicht schwierig zu zeigen, dass bereits die Optimierungsprobleme, die nur eines der genannten Optimierungsziele verfolgen, NP-hart sind, und wir deswegen zu Approximationsalgorithmen oder sogar heuristischen Algorithmen greifen müssen. Um so schwieriger ist es, viele Optimierungsziele gleichzeitig zu verfolgen. Im Allgemeinen gibt es keine global optimale Lösung, die bezüglich aller Ziele so gut ist wie die beste Lösung, wenn wir nur ein Ziel verfolgen. Deshalb sind wir an pareto-optimalen Lösungen interessiert, dies sind Lösungen, so dass es keine andere Lösung gibt, die bezüglich eines Zieles echt besser und bezüglich aller anderen Ziele nicht schlechter ist.

Die Vorlesung beschäftigt sich zunächst mit zweistufigen Schaltkreisen. Für diese Schaltkreise sind die Algorithmen für die Minimierung gut verstanden, wenn auch für größere Eingaben nicht gerade effizient. Für den Entwurf mehrstufiger Schaltkreise sind dagegen nur Heuristiken bekannt. Es lohnt sich daher, für gut strukturierte Funktionen, die häufiger vorkommen, spezielle Hardware zu entwerfen. In der Vorlesung werden Schaltkreise für die Grundrechenarten entworfen. Es wird sich herausstellen, dass gerade die Methoden, die man für die Grundrechenarten in der Schule gelernt hat, für die Realisierung in Hardware ungeeignet sind. Ein weiterer Schwerpunkt der Vorlesung ist die Darstellung von booleschen Funktionen im Rechner. Eine solche Darstellung soll möglichst kompakt sein, aber effiziente Algorithmen für Operationen auf booleschen Funktionen erlauben (z. B. für den Äquivalenztest oder für die Verknüpfung zweier Funktionen mit einem booleschen Operator). Ordered Binary Decision Diagrams (OBDDs) scheinen für diesen Zweck besonders geeignet zu sein. In der Vorlesung werden grundlegende Eigenschaften von OBDDs sowie ihre Anwendung beim Hardwareentwurf behandelt.

Begleitmaterial zur Vorlesung

Begleitmaterial zur Vorlesung findet sich hier als ps-Dokument.

Literatur:

  • Wegener, I. (1996).
    Effiziente Algorithmen für grundlegende Funktionen.
    Teubner, 2. Auflage.
    Das Buch steht unter Effiziente Algorithmen für grundlegende Funktionen
    elektronisch zur Verfügung.

  • Wegener, I. (2000).
    Branching Programs and Binary Decision Diagrams--Theory and Applications.
    SIAM Monographs in Discrete Mathematics and Applications.

  • Hachtel, G.D., Somenzi, F. (1996).
    Logic Synthesis and Verification Algorithms.
    Kluwer Academic Publishers.

    Weitere Unterlagen zur Vorlesung finden sich hier.

    Übungen

    Der Übungsbetrieb beginnt in der zweiten Vorlesungswoche am 27. Oktober 2005. Die aktuellen Übungsblätter werden jeweils bis zur Vorlesung am Donnerstag im Netz bereitgestellt.

    Die Übungsblätter als ps-Dateien:

    Blatt1 Blatt2 Blatt3 Blatt4 Blatt5 Blatt6 Blatt7 Blatt8 Blatt9 Blatt10 Blatt11 Blatt12 Blatt13 Blatt14


    20.7.2006 - Beate Bollig