Formal verification of firmware-based System-on-Chip modules

• Applicant: Professor Dr.-Ing. Wolfgang Kunz
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems ; Electronic Semiconductors, Components and Circuits, Integrated Systems, Sensor Technology, Theoretical Electrical Engineering
• Term: from 2013 to 2017
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 238346861

• Final Report Year: 2017

Final Report Abstract

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.

Publications

• "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
  
• "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
  
• 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
  
• 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
  
• “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
  
• 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.