Formale Verifikation Firmware-basierter System-on-Chip-Module

• Antragsteller: Professor Dr.-Ing. Wolfgang Kunz
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Elektronische Halbleiter, Bauelemente und Schaltungen, Integrierte Systeme, Sensorik, Theoretische Elektrotechnik
• Förderung: Förderung von 2013 bis 2017
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 238346861

Beim Entwurf von System-on-Chip (SoC) Modulen wird vermehrt ein neuer Entwurfsstil eingesetzt, bei dem Steuerfunktionen des Moduls nicht wie bisher üblich in Hardware, sondern als Firmware, die auf speziell dafür vorgesehenen Prozessoren ausgeführt wird, implementiert werden. UnterFirmware versteht man Software, die für den Nutzer des Moduls nicht zugänglich ist und bereits während der Fertigung beispielweise in einem ROM (Read Only Memory) abgelegt wird. Dieser Entwurfsstil findet aktuell insbesondere bei FPGAs (field programmable gate arrays) weite Verbreitung und bietet Vorteile in Hinblick auf Flächenbedarf und Wartbarkeit des Moduls. Die enge Verzahnung von Hardware und Software in niedriger Granularität wirft aber erhebliche Verifikationsprobleme auf, da Software und Hardware nicht wie sonst üblich getrennt verifiziert werden können. Im Rahmen dieses Forschungsvorhabens sollen formale Verifikationstechniken für Firmware-basierte System-on-Chip Module erforscht und entwickelt werden. Ausgangspunkt für die geplanten Arbeiten ist eine umfangreiche Fallstudie in Zusammenarbeit mit der Firma Xilinx, bei der die spezielle Charakteristik dieses Entwurfsstils und die daraus resultierenden Anforderungen an die Verifikation untersucht wurden. Ziel der geplanten Arbeiten sind vollautomatische Techniken zur Generierung von gemeinsamen Berechnungsmodellen für Hardware und Software, die dazu dienen sollen, künftig Standardverfahren der Hardwareverifikation für Firmware-basierte SoC-Module einsetzbar zu machen. Das Projekt profitiert von der langjährigen Erfahrung des Antragstellers im Bereich der formalen System-on-Chip-Verifikation sowie von Kooperationen sowohl mit industriellen Anbietern als auch mit Anwendern formaler Verifikationstechniken.

• DFG-Verfahren: Sachbeihilfen