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

• Erstellungsjahr: 2017

Zusammenfassung der Projektergebnisse

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. Unter Firmware 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 zunehmend Verbreitung, nicht nur bei FPGAs (field programmable gate arrays) sondern im klassischen System-on-Chip-Entwurf. Er 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 sind formale Verifikationstechniken für Firmware-basierte System-on-Chip Module erforscht und entwickelt worden. Als Ergebnis des Projektes stehen nun vollautomatische Techniken zur Generierung von gemeinsamen Berechnungsmodellen für Hardware und Software zur Verfügung. Zentrales Ergebnis des Projektes ist, dass auf Basis der neuen Modelle Standardverfahren der Hardwareverifikation wie property checking und equivalence checking nun auch für Firmware-basierte SoC-Module einsetzbar sind. Das reaktive Verhalten von Software und Hardware wird durch die neuen Techniken hardwarezyklengenau modelliert, so dass eine formale Hardware/Software-Coverifikation möglich ist. Im Projekt sind darüber hinaus Arbeiten durchgeführt worden, die es erlauben, binären Softwarecode von Drittanbietem, ebenfalls in die Betrachtung einzubeziehen. Dazu wurde eigens eine Disassemblierungstechnik entwickelt, die auf die Anforderung der hier betrachteten Probleme zugeschnitten ist. Die Anwendungen der neuen Technik gehen über die formale Verifikation funktionaler Systemeigenschaften hinaus. Durch die genaue Modellierung der Hardware/Software-Schnittstelle ist auch die Betrachtung nicht-funktionaler Eigenschaften wie etwa Robustheit und Sicherheit im Fehlerfalle möglich. Die Erweiterung und Nutzung der hier entwickelten Techniken auf die Sicherheitsanalyse ist Gegenstand eines bereits bewilligten DFG-Projektes.

Projektbezogene Publikationen (Auswahl)

• "Software in a Hardware View: New Models for HW-dependent Software in SoC Verification and Test", Proc. IEEE International Test Conference (ITC14), October, 2014. Seattle, USA
  C. Villarraga, B. Schmidt, B. Bao, R, Raman, C. Bartsch, T. Fehmel, D. Stoffel, W. Kunz
  (Siehe online unter https://doi.org/10.1109/TEST.2014.7035308)
• "A New Property Lan­ guage for the Specification of Hardware-Dependent Embedded System Software" in F. Oppenheimer (Ed.), Languages, Design Methods, and Tools for Electronic Systems Design, Springer, 2015
  B. Bao, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz
  
• A HW-dependent Software Model for Cross-Layer Fault Analysis in Embedded Systems, IEEE Latin-American Test Symposium (LATS-2016), Brazil, 2016
  C. Bartsch, C. Villarraga, D. Stoffel, W. Kunz
  (Siehe online unter https://doi.org/10.1109/LATW.2016.7483356)
• Speculative Disassembly of Binary Code, International Conference on Compilers, Architectures and Synthesis for Embedded Systems (CASES), Embedded Systems Week 2016, Pittsburgh, USA, 2016
  M. A. Ben Khadra, D. Stoffel, W. Kunz
  (Siehe online unter https://doi.org/10.1145/2968455.2968505)
• goSAT: Floating-point Satisfiability as Global Optimization, in Formal Methods in Computer-Aided Design (FMCAD'17), 2017
  M. A. Ben Khadra, D. Stoffel, W. Kunz
  (Siehe online unter https://doi.org/10.23919/FMCAD.2017.8102235)
• “Cycle-Accurate Software Modeling for RTL Verification of Embedded Systems”, IEEE Design and Diagnostics of Electronic Circuits and Systems (DDECS), Dresden, 2017
  M. Schwarz, C. Villarraga, D. Stoffel, W. Kunz
  (Siehe online unter https://doi.org/10.1109/DDECS.2017.7934571)
• Software in a Hardware View New - Models for HW-dependent Software in SoC Verification. In: Drechsler R. (eds) Formal System Verification, pages 123-154. ISBN 978-3-319-57685-5 Springer Cham. 2018
  Villarraga C., Stoffel D., Kunz W.