Firmware Verification in SoC modules

Contact: Carlos Villarraga, Michael Schwarz

In modern design practices for System-on-Chip (SoC) modules a strong trend towards a firmware-based design style can be observed. Certain control functions of an SoC module are no longer implemented in hardware but as “firmware” running on processors instantiated particularly for this purpose. Firmware is a special software that is not accessible to the user of this module and that is stored, e.g., in a ROM (read-only-memory) already during manufacturing of the chip. This design style enjoys particular popularity especially with FPGA (field programmable gate array) designs and offers several advantages with respect to area consumption and maintainability. However, 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.

In this project, formal verification techniques for firmware-based SoC modules are explored. Our goal is to develop joint computational models and algorithms that are adapted to this specific application domain. While there exists a large number of formal hardware and software verification techniques there is not yet a satisfactory solution for jointly verifying the hardware and software components of a firmware-based IP core

Check out:

• our preliminary case study with Xilinx Inc., San Jose, CA, USA [pdf]
• our book chapter on the subject.