« zurück

Kolloquium | „Formale Verifikation von System-on-Chip-Entwürfen“

01.02.2006 | 17 Uhr c.t. | MZH 5210

Dominik Stoffel | Universität Kaiserslautern

Abstract

Die Kosten für den Entwurf eines System-on-Chip (SoC) sind trotz weitgehender Automa­tisierung sehr hoch. Den größten Anteil an den Entwurfskosten stellen heute mit 60 bis 80 Prozent die Kosten für die Verifikation dar. Hier besteht ein hoher Innovations- und Forschungs­bedarf, um den hohen Anforderungen an Produktivität und Qualität gerecht zu werden. In diesem Vortrag verschaffen wir uns zunächst einen Überblick über den Stand der Technik bei der Verifikation industrieller Systementwürfe. Wir stellen die Bereiche vor, in denen bereits heute formale Verifikationsmethoden die konventionellen Techniken ergänzen oder ersetzen, und diskutieren, wo in naher Zukunft weitere Fortschritte zu erwarten sind. Dringender Innovationsbedarf besteht bei der Verifikation der Korrektheit von Strukturen zur Systemintegration, also bei den Kommunikationsschnittstellen zwischen den Modulen eines Systems. Hier können klassische Verfahren wie Simulation nicht mehr die erforderliche Qualität liefern. Genauso stoßen aber auch formale Verifikationstechniken schnell an ihre Grenzen. Wir stellen eine neue Technik für die Verifikation von Kommunikationsblöcken vor, die helfen soll, den besonderen Anforderungen dieses Problems gerecht zu werden. Ein wesentli­ches Merkmal der Struktur solcher Blöcke ist, dass sie meist ein zentrales Haupt-Steuer­werk (engl.: „main finite state machine“) enthalten, das mit den übrigen Steuerwerken kommu­niziert. Die Kenntnis dieser Struktur erlaubt es, ein Verfahren für eine partitionierte Automa­ten­traversierung zu formulie­ren, die den Gesamtzustandsraum anhand der Zustands­übergänge des Haupt-Steuerwerkes zerlegt. In diesem Vortrag erklären wir, warum diese Art der Partitionierung erfolgreicher ist als bisherige Techniken und berichten von der erfolgreichen An­wendung der neuen Technik auf komplexe SoC-Entwürfe, die bei unseren Forschungs­partnern in der Industrie ent­wickelt werden.

»Dominik Stoffel studierte Elektrotechnik an der Universität Karlsruhe (Diplom 1992). In den Jahren 1993 und 1994 arbeitete er als Ingenieur bei Mercedes-Benz in Sindelfingen und entwickelte dort Prüfsysteme für Kfz-Elektronik. Von 1994 bis 1998 war er wissenschaftlicher Mitarbeiter an der Max-Planck-Arbeitsgruppe für Fehlertolerantes Rechnen an der Universität Potsdam. Von 1998 bis 2001 war er als wissenschaftlicher Mitarbeiter am Lehrstuhl für Entwurfsautomatisierung an der Universität Frankfurt beschäftigt. Im Jahre 1999 promovierte er in Technischer Informatik über formale Verifikation sequenzieller Digitalschaltungen. Seit 2001 ist er wissenschaftlicher Assistent am Lehrstuhl für Entwurf informationstechnischer Systeme an der Universität Kaiserslautern. Dominik Stoffel arbeitet auf dem Gebiet des rechnergestützten Schaltungsentwurfs. Die Schwerpunkte seiner Forschung liegen in den Bereichen Schaltungssynthese und -optimierung sowie auf formalen Methoden zur Verifikation digitaler Systeme.