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

在片上系统（SoC）模块的现代设计实践中，可以观察到基于固件的设计风格的强烈趋势。SoC模块的某些控制功能不再以硬件实现，而是作为在特别为此目的而实例化的处理器上运行的固件来实现。固件是一种特殊的软件，该模块的用户无法访问，并且存储在，例如，在芯片制造期间已经在ROM（只读存储器）中。这种设计风格特别受欢迎，尤其是在FPGA（现场可编程门阵列）设计中，并且在面积消耗和可维护性方面具有几个优点。然而，硬件和软件在低粒度级别上的紧密耦合提出了实质性的验证挑战，因为独立地验证硬件和软件的常规实践不再足够。在这个项目中，正式验证技术的固件为基础的SoC模块进行了探索。该项目的起点是与Xilinx Inc.合作进行的全面案例研究。评估基于固件的设计风格的特点以及由此产生的对核查的影响。该项目的目标是研究和开发用于生成硬件和软件的联合计算模型的全自动技术。新模型将使我们能够将标准的硬件验证方法应用于基于固件的SoC设计。该项目受益于提案人在片上系统验证领域的长期经验，以及与工业提供商和正式验证技术用户的积极合作。

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.