Property First Hardware Design - Eine Correct-by-Construction-Methodik für den RTL-Entwurf aus Systemmodellen

• Antragsteller: Professor Dr.-Ing. Wolfgang Kunz
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2016 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 328724410

Das berühmte Gesetz von Moore, nach dem sich etwa alle 1,8 Jahre die Anzahl der Transistoren verdoppelt, die unter ökonomischen Randbedingungen auf einem Chip integriert werden können, hat über Jahrzehnte den technologischen Fortschritt in der Mikro- und Nanoelektronik zutreffend beschrieben. Inzwischen ist jedoch unumstritten, dass die Entwicklung sich in den letzten Jahren stark verlangsamt hat und sich weiter verlangsamen wird, mit weitreichenden Folgen: während in der Vergangenheit durch die Migration auf neue Technologien regelmäßig Innovationsschübe bei mikroelektronischen Systemen ausgelöst werden konnten, sind künftig Verbesserungen in den Architekturen und Mikroarchitekturen der Systeme sowie in den zugehörigen Entwurfs- und Optimierungsverfahren entscheidend, um innovative Produkte zu erzielen. Aggressiv optimierte Entwürfe sind jedoch fehleranfällig und erfordern daher besonders leistungsfähige Verifikations¬techniken. Wie von der Electronic System Design Alliance berichtet wird, hat im vergangenen Jahr der Einsatz formaler Verifikationswerkzeuge um den Faktor zwei zugenommen. Mit dem Ende der von Moore beschriebenen Entwicklung rücken somit innovative Entwurfs- und Verifikationstechniken für System-on-Chip (SoC) Hardware verstärkt in den Mittelpunkt des industriellen Interesses. Gegenstand dieses Projektes ist die Erforschung und Entwicklung einer grundlegend neuen Methodik für den Entwurf von SoC-Hardware, die den künftigen Anforderungen gerecht wird. Die erforschte Methodik soll in neuer Art und Weise Techniken der formalen Verifikation in den Entwurfsablauf integrieren und neueste Erkenntnisse über formale Abstraktionstechniken dazu nutzen, systematisch aus Systemmodellen nachweislich korrekte Hardwareentwürfe auf Register-Transfer-Ebene (RTL) zu gewinnen. Die neue Methodik soll jedoch nicht nur die Aufwände für Entwurf und Verifikation verringern. Durch die vorgesehene Einbindung formaler Methoden in den Entwurfsablauf wird dem Designer frühzeitig ein umfangreiches und detailliertes Wissen über temporale und logische Zusammenhänge zwischen Entwurfskomponenten zur Verfügung gestellt, das er für Optimierungen der Mikroarchitektur nutzen kann. Insbesondere soll in dem Vorhaben gezeigt werden, wie bislang vernachlässigtes Optimierungspotential bei der Reduzierung der Leistungsaufnahme eines SoC-Entwurfs besser ausgeschöpft werden kann. Die vorgeschlagene Methodik erfordert vom Anwender kein fortgeschrittenes Wissen über formale Verifikationstechniken. Auch erlegt sie dem Nutzer keinerlei Einschränkungen bezüglich möglicher Entwurfsverfeinerungen auf. Vielmehr ergänzt sie den heute in der Praxis üblichen, zumeist manuellen Entwurfsprozess um zusätzliche Maßnahmen, die die Korrektheit des RTL-Entwurfs als Verfeinerung eines Systemmodells sicherstellen und das detaillierte Verhalten des Systems auf RT-Ebene sowie den Zusammenhang zwischen Objekten der RT- und der Systemebene gut lesbar und für die Optimierung nutzbar dokumentieren.

• DFG-Verfahren: Sachbeihilfen