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

基于固件的片上系统模块的形式验证

• 批准号: 238346861
• 负责人: Professor Dr.-Ing. Wolfgang Kunz
• 金额: --
• 依托单位: Lehrstuhl für Entwurf informationstechnischer Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2013
• 资助国家: 德国
• 起止时间: 2012-12-31 至 2016-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/238346861?language=en
• 关键词: Formal; verification; firmware; based; System

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.

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

项目成果

A HW-dependent software model for cross-layer fault analysis in embedded systems

用于嵌入式系统跨层故障分析的硬件相关软件模型

• DOI: 10.1109/latw.2016.7483356
• 发表时间: 2016
• 期刊: 2016 17th Latin-American Test Symposium (LATS)
• 作者: C. Bartsch;C. Villarraga;D. Stoffel;W. Kunz
• 通讯作者: W. Kunz

Speculative disassembly of binary code

• DOI: 10.1145/2968455.2968505
• 发表时间: 2016-10
• 期刊: 2016 International Conference on Compliers, Architectures, and Sythesis of Embedded Systems (CASES)
• 作者: M. Ammar;Benguettache Khadra;D. Stoffel;W. Kunz

Software in a hardware view: New models for HW-dependent software in SoC verification and test

硬件视图中的软件：SoC 验证和测试中依赖于硬件的软件的新模型

• DOI: 10.1109/test.2014.7035308
• 发表时间: 2014
• 期刊: 2014 International Test Conference
• 作者: C. Villarraga;B. Schmidt;B. Bao;C. Bartsch;T. Fehmel;D. Stoffel;W. Kunz
• 通讯作者: W. Kunz

Cycle-accurate software modeling for RTL verification of embedded systems

用于嵌入式系统 RTL 验证的周期精确软件建模

• DOI: 10.1109/ddecs.2017.7934571
• 发表时间: 2017
• 期刊: 2017 IEEE 20th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS)
• 作者: M. Schwarz;C. Villarraga;D. Stoffel;W. Kunz
• 通讯作者: W. Kunz