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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Carlos Villarraga
Advisor:Wolfgang Kunz
Document Type:Doctoral Thesis
Language of publication:English
Publication Date:2017/01/30
Year of Publication:2017
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2016/12/07
Date of the Publication (Server):2017/01/31
Tag:Firmware; Formal Verification; Hardware/Software co-verification; Model checking; Symbolic execution
GND-Keyword:Formale Methode; Model checking; Programmverifikation; Hardwareverifikation; Formale Beschreibungstechnik; Firmware
Number of page:XII, 124
Faculties / Organisational entities:Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
CCS-Classification (computer science):B. Hardware
DDC-Cassification:6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau
Licence (German):Standard gemäß KLUEDO-Leitlinien vom 30.07.2015