Formal Verification of Firmware-Based System-on-Chip Modules

  • In current practices of system-on-chip (SoC) design a trend can be observed to integrate more and more low-level software components into the system hardware at different levels of granularity. The implementation of important control functions and communication structures is frequently shifted from the SoC’s hardware into its firmware. As a result, the tight coupling of hardware and software at a low level of granularity raises substantial verification challenges since the conventional practice of verifying hardware and software independently is no longer sufficient. This calls for new methods for verification based on a joint analysis of hardware and software. This thesis proposes hardware-dependent models of low-level software for performing formal verification. The proposed models are conceived to represent the software integrated with its hardware environment according to the current SoC design practices. Two hardware/software integration scenarios are addressed in this thesis, namely, speed-independent communication of the processor with its hardware periphery and cycle-accurate integration of firmware into an SoC module. For speed-independent hardware/software integration an approach for equivalence checking of hardware-dependent software is proposed and an evaluated. For the case of cycle-accurate hardware/software integration, a model for hardware/software co-verification has been developed and experimentally evaluated by applying it to property checking.

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Carlos Villarraga
URN (Permalink):urn:nbn:de:hbz:386-kluedo-45678
Betreuer:Wolfgang Kunz
Sprache der Veröffentlichung:Englisch
Veröffentlichungsdatum (online):30.01.2017
Jahr der Veröffentlichung:2017
Veröffentlichende Institution:Technische Universität Kaiserslautern
Titel verleihende Institution:Technische Universität Kaiserslautern
Datum der Annahme der Abschlussarbeit:07.12.2016
Datum der Publikation (Server):31.01.2017
Freies Schlagwort / Tag:Firmware; Formal Verification; Hardware/Software co-verification; Model checking; Symbolic execution
GND-Schlagwort:Firmware; Formale Beschreibungstechnik; Formale Methode; Hardwareverifikation; Model checking; Programmverifikation
Seitenzahl:XII, 124
Fachbereiche / Organisatorische Einheiten:Fachbereich Elektrotechnik und Informationstechnik
CCS-Klassifikation (Informatik):B. Hardware
DDC-Sachgruppen:6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vom 30.07.2015

$Rev: 13581 $