This book contains extended and revised versions of the best papers that have been presented during the twelfth edition of the IFIP TC10/WG10.5 International Conference on Very Large Scale Integration, a Global System-on-a-Chip Design & CAD Conference. The 12* edition was held at the Lufthansa Training Center in Seeheim-Jugenheim, south of Darmstadt, Germany (December 1-3, 2003). Previous conferences have taken place in Edinburgh (81), Trondheim (83), Tokyo (85), Vancouver (87), Munich (89), Edinburgh (91), Grenoble (93), Tokyo (95), Gramado (97), Lisbon (99)andMontpellier(01). The purpose of this conference, sponsored by IFIP TC 10 Working Group 10.5, is to provide a forum to exchange ideas and show research results in the field of microelectronics design. The current trend toward increasing chip integration brings about exhilarating new challenges both at the physical and system-design levels: this conference aims to address these exciting new issues. The 2003 edition of VLSI-SoC conserved the traditional structure, which has been successful in previous editions. The quality of submissions (142 papers) made the selection process difficult, but finally 57 papers and 14 posters were accepted for presentation in VLSI-SoC 2003. Submissions came from Austria, Bulgaria, Brazil, Canada, Egypt, England, Estonia, Finland, France, Germany, Greece, Hungary, India, Iran, Israel, Italy, Japan, Korea, Malaysia, Mexico, Netherlands, Poland, Portugal, Romania, Spain, Sweden, Taiwan and the United States of America. From 57 papers presented at the conference, 18 were selected to have an extended and revised version included in this book.

This book contains extended and revised versions of the best papers that have been presented during the twelfth edition of the IFIP TC10/WG10.5 International Conference on Very Large Scale Integration, a Global System-on-a-Chip Design & CAD Conference. The 12* edition was held at the Lufthansa Training Center in Seeheim-Jugenheim, south of Darmstadt, Germany (December 1-3, 2003). Previous conferences have taken place in Edinburgh (81), Trondheim (83), Tokyo (85), Vancouver (87), Munich (89), Edinburgh (91), Grenoble (93), Tokyo (95), Gramado (97), Lisbon (99)andMontpellier(01). The purpose of this conference, sponsored by IFIP TC 10 Working Group 10.5, is to provide a forum to exchange ideas and show research results in the field of microelectronics design. The current trend toward increasing chip integration brings about exhilarating new challenges both at the physical and system-design levels: this conference aims to address these exciting new issues. The 2003 edition of VLSI-SoC conserved the traditional structure, which has been successful in previous editions. The quality of submissions (142 papers) made the selection process difficult, but finally 57 papers and 14 posters were accepted for presentation in VLSI-SoC 2003. Submissions came from Austria, Bulgaria, Brazil, Canada, Egypt, England, Estonia, Finland, France, Germany, Greece, Hungary, India, Iran, Israel, Italy, Japan, Korea, Malaysia, Mexico, Netherlands, Poland, Portugal, Romania, Spain, Sweden, Taiwan and the United States of America. From 57 papers presented at the conference, 18 were selected to have an extended and revised version included in this book.

This book constitutes the refereed proceedings of the IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design Methodologies, CHARME '95, held in Frankfurt, Germany, in October 1995.
The 20 revised full papers presented were carefully selected by the program committee and address all current aspects of research and advanced applications in the field of formal verification of hardware. Among the topics covered are model checking, theorem proving, formally verified synthesis, process algebras, finite state systems, verification environments, language containment, and VHDL.

Die Korrektheit eines digitalen Systems vollstandig nachzuweisen - dieses Problem, das von grossem praktischen Interesse ist, wirft eine Reihe grund legender Fragen der Modellierung von Hardware, der Entwicklung geeig neter Reprasentationen, der Moglichkeit formalen Argurnentierens und der technischen Realisierbarkeit von Verifikationswerkzeugen auf. Das vorliegende Buch gibt eine Einfuhrung fur diejenigen, die sich mit dem Gebiet der Hardwareverifikation vertraut machen wollen. Wahrend ein Buch uber dieses Thema - insbesondere auf Deutsch verfasst - vor einigen Jahren noch etwas fast missionarisches gehabt hatte, findet das Gebiet inzwischen verbreitetes Interesse, was sich in einer zunehmenden Anzahl an Konferen zen und Veroffentlichungen wiederspiegelt. Dieses Interesse hat seine Ur sache einmal sicherlich in einem gesteigerten Problembewusstsein, dass man sich eben bei VLSI-Bausteinen keine Entwurfsfehler mehr leisten kann. Zum anderen wird immer mehr erkannt, dass das Problem der Verifikation fun damental ist fur den gesamten Bereich des Hardwareentwurfs. Das Buch ist entstanden aus meiner Habilitationsschrift, aus Materialien zu einer Vorlesung "Entwurfsmethodik fur komplexe digitale Systeme," die ich an der Technischen Hochschule Darmstadt von 1985 bis 1990 hielt, so wie aus einer Reihe englischsprachiger Berichte, die ich zum Zwecke der Selbstverstandigung uber das Gebiet geschrieben habe. Mein besonderer Dank gilt Prof. R. Piloty fur die jahrelange Forderung mei ner Arbeit. Er bot mir die Moglichkeit, meine Ideen uber die Verifikation digitaler Systeme wahrend meiner Zeit als Mitarbeiter und spater als Habi litand am Institut fur Datentechnik der Technischen Hochschule Darmstadt zu entwickeln."