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

点击翻译按钮获取中文摘要

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 shall be explored. The starting point of this project is a comprehensive case study in collaboration with Xilinx Inc. to assess the special characteristics of a firmware-based design style and the resulting implications for verification. The objective of this project is to do research in and to develop fully automatic techniques for generating joint computational models for hardware and software. The new models will allow us to apply standard methods of hardware verification also to firmware-based SoC designs. The project benefits from the proposer's long experience in the field of System-on-Chip verification as well as from active collaborations with industrial providers as well as users of formal verification technology.