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

在片上系统(SoC)模块的现代设计实践中，可以观察到基于固件的设计风格的强烈趋势。SoC模块的某些控制功能不再在硬件中实现，而是作为在特别为此目的实例化的处理器上运行的固件来实现。固件是该模块的用户不可访问的特殊软件，并且例如在芯片制造期间已经存储在ROM(只读存储器)中。这种设计风格特别受欢迎，尤其是现场可编程门阵列(现场可编程门阵列)设计，并在面积消耗和可维护性方面提供了几个优势。然而，硬件和软件在低粒度水平上的紧密耦合增加了大量的验证挑战，因为独立验证硬件和软件的传统实践不再足够。在本项目中，将探索基于固件的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.