Hardware veri?cation is the process of checking whether a design conforms to its speci?cations of functionality and timing. In today s design processes it becomes more and more important. Very large scale integrated (VLSI) circuits and the resulting digital systems have conquered a place in almost all areas of our life, even in security sensitive applications. Complex digital systems control airplanes, have been used in banks and on intensive-care units. Hence, the demand for error-free designs is more important than ever. In addition, economic reasons underline this demand as well. The design and production process of present day VLSI-circuits is highly time- and cost-intensive. Mo- over, it is nearly impossible to repair integrated circuits. Thus, it is desirable to detect design errors early in the design process and not just after producing the prototype chip. All these facts are re?ected by developing and prod- tion statistics of present day companies. For example, In?neon Technologies [118] assumed that about 60% to 80% of the overall design time was spent for veri?cation in 2000. Other sources cite the 3-to-1 head count ratio between veri?cation engineers and logic designers. This shows that verifying logical correctness of the design of hardware systems is a major gate to the problem of time-to-market (cf. [113]). With the chip complexity constantly increasing, the dif?culty as well as the - portance of functional veri?cation of new product designs has been increased. It is not only more important to get error-free designs. Inhaltsverzeichnis Fundamentals.- Preliminaries.- Representation of Boolean and Pseudo Boolean Functions.- Equivalence Checking of Combinational Circuits.- Use of Canonical Data Structures.- SAT and ATPG Based Equivalence Checking.- Exploiting Similarities.- Checking Equivalence for Partial Implementations.- Permutation Independent Boolean Comparison.- Equivalence Checking of Sequential Circuits.- Formal Basics.- The Latch Correspondence Problem.
Paul Molitor Boeken



Kompaktkurs VHDL
mit vielen anschaulichen Beispielen
Die Entwicklung moderner Hardware erfordert eine abstrakte Beschreibung der wesentlichen Komponenten. VHDL ist eine zu diesem Zweck entwickelte Hardwarebeschreibungssprache und mittlerweile ein weltweit verbreiteter Standard in der Industrie.§Durch geschickte Verbindung von Theorie und praktische Beispielen führt das Buch leicht verständlich und stets motivierend in VHDL ein. Bewusst verzichten die Autoren dabei auf die Erläuterung nur selten benutzter Konstrukte, sondern konzentrieren die Darstellung auf die Betrachtung der Sprache unter dem Aspekt der Schaltkreissynthese.§Das Buch umfasst den Stoff einer einsemestrigen Vorlesung und bietet dem Leser eine leicht verständliche und mit vielen interessanten Beispielen unterlegte Einführung in die Sprache VHDL.
Datenstrukturen und effiziente Algorithmen sind entscheidend für den automatisierten Entwurf großer digitaler Schaltungen. In den letzten Jahren hat sich das Gebiet der Logiksynthese durch neue Technologien und die Entwicklung effizienter Datenstrukturen rasant weiterentwickelt. Das Buch präsentiert die heute verwendeten Datenstrukturen und Algorithmen der logischen Synthese kombinatorischer Schaltungen. Der erste Teil bietet eine anschauliche Einführung in die Grundlagen der Verbandstheorie und Booleschen Algebren sowie in die aktuellen Zielarchitekturen. Im zweiten Teil wird die traditionelle zweistufige logische Synthese behandelt, einschließlich exakter und heuristischer Methoden zur Berechnung von Minimalpolynomen. Nach einer detaillierten Darstellung binärer Entscheidungsgraphen (reduced ordered binary decision diagrams) wird die mehrstufige Logiksynthese behandelt, insbesondere die funktionale Dekomposition Boolescher Funktionen und algebraische Methoden, wie sie im SIS-Paket der UC Berkeley verwendet werden. Das Buch richtet sich an Studierende der Informatik und Elektrotechnik und legt großen Wert auf anschauliche Konzepte. Es verbindet theoretische Grundlagen mit Illustrationen, um ein vertieftes Verständnis zu fördern. Dozenten können Vorlesungsfolien (ca. 650 Stück) über E-Mail anfordern.