- Treffer 1 von 1
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.
Verfasser*innenangaben: | Carlos Villarraga |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-45678 |
Betreuer*in: | Wolfgang Kunz |
Dokumentart: | Dissertation |
Sprache der Veröffentlichung: | Englisch |
Datum der Veröffentlichung (online): | 30.01.2017 |
Jahr der Erstverö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: | Formale Methode; Model checking; Programmverifikation; Hardwareverifikation; Formale Beschreibungstechnik; Firmware |
Seitenzahl: | XII, 124 |
Fachbereiche / Organisatorische Einheiten: | Kaiserslautern - 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 |