The pillars of the bridge on the cover of this book date from the Roman Empire and they are in daily use today, an example of conventional engineering at its best. Modern commodity operating systems are examples of current system programming at its best, with bugs discovered and fixed on a weekly or monthly basis. This book addresses the question of whether it is possible to construct computer systems that are as stable as Roman designs. The authors successively introduce and explain specifications, constructions and correctness proofs of a simple MIPS processor; a simple compiler for a C dialect; an extension of the compiler handling C with inline assembly, interrupts and devices; and the virtualization layer of a small operating system kernel. A theme of the book is presenting system architecture design as a formal discipline, and in keeping with this the authors rely on mathematics for conciseness and precision of arguments to an extent common in other engineering fields. This textbook is based on the authors' teaching and practical experience, and it is appropriate for undergraduate students of electronics engineering and computer science. All chapters are supported with exercises and examples.

Hardware correctness is becoming ever more important in the design of computer systems. The authors introduce a powerful new approach to the design and analysis of modern computer architectures, based on mathematically well-founded formal methods which allows for rigorous correctness proofs, accurate hardware costs determination, and performance evaluation. This book develops, at the gate level, the complete design of a pipelined RISC processor with a fully IEEE-compliant floating-point unit. In contrast to other design approaches, the design presented here is modular, clean and complete.

The pillars of the bridge on the cover of this book date from the Roman Empire and they are in daily use today, an example of conventional engineering at its best. Modern commodity operating systems are examples of current system programming at its best, with bugs discovered and fixed on a weekly or monthly basis. This book addresses the question of whether it is possible to construct computer systems that are as stable as Roman designs. The authors successively introduce and explain specifications, constructions and correctness proofs of a simple MIPS processor; a simple compiler for a C dialect; an extension of the compiler handling C with inline assembly, interrupts and devices; and the virtualization layer of a small operating system kernel. A theme of the book is presenting system architecture design as a formal discipline, and in keeping with this the authors rely on mathematics for conciseness and precision of arguments to an extent common in other engineering fields. This textbook is based on the authors' teaching and practical experience, and it is appropriate for undergraduate students of electronics engineering and computer science. All chapters are supported with exercises and examples.

This monograph is based on the third author's lectures on computer architecture, given in the summer semester 2013 at Saarland University, Germany. It contains a gate level construction of a multi-core machine with pipelined MIPS processor cores and a sequentially consistent shared memory. The book contains the first correctness proofs for both the gate level implementation of a multi-core processor and also of a cache based sequentially consistent shared memory. This opens the way to the formal verification of synthesizable hardware for multi-core processors in the future. Constructions are in a gate level hardware model and thus deterministic. In contrast the reference models against which correctness is shown are nondeterministic. The development of the additional machinery for these proofs and the correctness proof of the shared memory at the gate level are the main technical contributions of this work.

This book presents a formal model for evaluating the cost effectiveness of computer architectures. The model can cope with a wide range of architectures, from CPU design to parallel supercomputers. To illustrate the formal procedure of trade-off analyses, several non-pipelined design alternatives for the well-known RISC architecture called DLX are analyzed quantitatively. It is formally proved that the interrupt mechanism proposed for the DLX architecture handles nested interrupts correctly.
In an appendix all programs to compute the cost and cycle time of the designs described are listed in C code. Running these simple C programs on a PC is sufficient to verify the results presented. The book addresses design professionals and students in computer architecture.

This work is building on results from the book named "A Pipelined Multi-core MIPS Machine: Hardware Implementation and Correctness" by M. Kovalev, S.M. Muller, and W.J. Paul, published as LNCS 9000 in 2014. It presents, at the gate level, construction and correctness proof of a multi-core machine with pipelined processors and extensive operating system support with the following features: * MIPS instruction set architecture (ISA) for application and for system programming * cache coherent memory system * store buffers in front of the data caches * interrupts and exceptions * memory management units (MMUs) * pipelined processors: the classical five-stage pipeline is extended by two pipeline stages for address translation * local interrupt controller (ICs) supporting inter-processor interrupts (IPIs) * I/O-interrupt controller and a disk

Dieses Lehrbuch beschaftigt sich in mathematisch praziser Weise mit einem ganz und gar praktischen Thema, namlich dem Entwurf digitaler Hardware. Neben einer Diskussion der mathematischen Grundbegriffe werden die notwendigen theoretischen Grundlagen behandelt. Schliesslich wird dann das vollstandige Design eines einfachen Rechners entwickelt.

Das vorliegende Lehrbuch beschaftigt sich in mathematisch praziser Weise mit ei- nem ganz und gar praktischen Thema, namlich dem Entwurf von Hardware. Kapitel 1 enthalt eine Diskussion mathematischer Grundbegriffe. In den Kapiteln 2 bis 4 werden die notwendigen theoretischen Grundlagen uber Boole'sche Ausdrucke, Schaltkreiskomplexitat und Rechnerarithmetik behandelt. Der UEbergang von der abstrakten Schaltkreistheorie zum Entwurf konkreter Schaltungen findet nahtlos in Kapitel 5 statt, wo aus den Verzoegerungszeiten von Gattern das zeitliche Verhal- ten von Flipflops und anderen Speicherbausteinen abgeleitet wird. Kapitel 6 enthalt dann das vollstandige Design eines einfachen Rechners. Das Lehrbuch ist aus Vorlesungen des zweiten Autors entstanden. Kapitel 2 bis 6 enthalten den Stoff fur eine einsemestrige Anfangervorlesung. Kapitel 1 ist mehr ein Nachschlagewerk fur nagende Fragen, die sich fruher oder spater einstellen. Kapitel und Abschnitte, die mit einem Stern gekennzeichnet sind, kann man uberspringen. Die Darstellung grosser Teile der Kapitell, 5 und 6 ist neu. Die Kapitel 2 bis 4 haben einen erheblichen Anteil an fortgeschrittenem Material. Es hat sich jedoch gezeigt, dass Erstsemester damit keine besonderen Schwierigkeiten haben. Im Einzelnen enthalt Kapitell eine Entwicklung des formalen Mengenkonzepts in einer fur Studienanfanger verstandlichen Form. Die Satze und Beweise in diesem Kapitel sind von vorne bis hinten klassische Mathematik. Der Standpunkt, von dem aus wir sie interpretieren, ist bewusst ubermutig und nicht klassisch. Wir wollen damit den Studierenden schmackhaft machen, von Zeit zu Zeit auch Wohlvertrautes von einem frischen - naturlich nicht unsinnigen - Standpunkt aus zu betrachten. Das ist insbesondere beim Forschen manchmal sehr nutzlich.

Dieser Band erscheint aus Anlafi des sechzigsten Geburtstags von Gunter Hotz. Er enthiilt Arbeiten seiner Schuler, Freunde und Kollegen. Gunter Hotz ist seit 1969 Professor fur Numerische Mathematik und Informatik an der Universitiit des Saarlandes. Er hat am Aufbau des Fachbereichs Informatik der Universitiit des Saarlandes groBen Anteil, und er hat die Entwicklung der Infor matik in Deutschland wesentlich mitgepriigt. Dies wird durch die Vielfalt der hier erscheinenden Arbeiten eindrucksvoll belegt. Mit den Beitriigen im vorliegenden Buch mochten die Autoren bei Herrn Hotz einen Teil des Dankes, zu dem sie aus unterschiedlichen Grunden verpflichtet sind, abstatten. Saarbrucken, im November 1991 J. Buchmann, H. Ganzinger, W. J. Paul Inhaltsverzeichnis Abolhassan, Drefenstedt, Keller, Paul, Scheerer: On the Physical Design of PRAMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Bernd Becker: Synthesis for Testability: Binary Decision Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Eberhard Bertsch: Ahnlichkeit von Grammatiken - Ansatze und Erfahrungen . . . . . . . . . . . . . . . . . . . . 41 Hans-Peter Blatt: Verteilung der Nullstellen von Polynomen auf JordanbOgen . . . . . . . . . . . . . . . . . . . . 55 Johannes Buchmann, Stephan Diillmann: Distributed Class Group Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Volker Claus: Complexity Measures on Permutations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 Martin Dietzfelbinger, Friedheim Meyer auf der Heide: Dynamic Hashing in Real Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Ferdinand, Seidl, Wilhelm: Baumautomaten zur Codeselektion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 Michael J. Fischer, Sophia A. Paleologou: Decision Making in the Presence of Noise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 B. Halstenberg, R. Reischuk: Uber den Nutzen von Orakelfragen bei nichtdeterministischen Kommunikationsprotokollen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 Uwe Hinsberger, Reiner Kalla: Performance Optimization of Combinational Circuits . . . . . . . . . . . . . . . . . . . . . . . . . 185 Thomas Kretschmer: An Algebraic Characterization of Context-Free Languages . . . . . . . . . . . . . . . . . . . . 209 Juraj Hromkovi, Burkhard Monien: The Bisection Problem for Graphs of Degree 4 (Configuring Transputer Systems) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ."

Das Buch prAsentiert die Resultate einer vierjAhrigen Kooperation zwischen der UniversitAt des Saarlandes und der Siemens AG. Schwerpunkte sind die Themenbereiche Vernetzung, Entwicklung von Software-Tools und von wissenschaftlicher Anwender-Software. Der Band wurde zusammengestellt anlAAlich einer AbschluAtagung mit umfassender PrAsentation aller Projektergebnisse. Neben einer EinfA1/4hrung in das Gesamtprojekt werden ausgewAhlte Projekte detailliert vorgestellt. Ziel des Bandes ist es, von einem gelungenen Versuch zu berichten, in einer Hochschule durch den breiten Einsatz von Arbeitsplatzrechnern in allen Wissenschaftsbereichen die Arbeitsbedingungen in groAem Umfang zu verbessern. Von zusAtzlichem Interesse ist die Tatsache, daA einige der vorgestellten Entwicklungen unter gewissen Voraussetzungen Interessenten zur VerfA1/4gung gestellt werden kAnnen.