SBIR Phase I: Automatic Formal Verification of Chip-Multi-Threaded Multicore Processors

SBIR 第一阶段：芯片多线程多核处理器的自动形式验证

• 批准号: 0945974
• 负责人: Miroslav Velev
• 金额: --
• 依托单位: Aries Design Automation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-01-01 至 2010-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0945974&HistoricalAwards=false
• 关键词: SBIR; Phase; Automatic; Formal; Verification

This Small Business Innovation Research (SBIR) Phase I project will result in an efficient and scalable method for design and formal verification of Chip-Multi-Threaded multicore processors, where the individual cores have hardware support for multi-threading. This method will be developed and optimized on the OpenSPARC T2 processor, a publicly available version of the Sun UltraSPARCT2?the industry?s first ?server on a chip,? packaging the most cores and threads of any general-purpose processor available, and integrating all the key functions of a server on a single chip: computing, networking, security, and input/output, plus tight integration with the Solaris operating system.The work will be based on extending an extremely efficient prototype tool flow for formal verification of pipelined processors that outperforms other approaches by orders of magnitude, while requiring minimal manual intervention. The anticipated technical results are highly automatic and scalable method and tool flow for formal verification of chip-multi-threaded multicore processors, where the individual cores have hardware support for multi-threading.The broader impact/commercial potential of this project will be based on the significantly increased reliability of Chip-Multi-Threaded (CMT) multicore processors, where the individual cores have hardware support for multi-threading. Because of power-consumption limitations, performance canno longer be gained by increasing the frequency and/or the complexity of a single core. Instead semiconductor companies are adapting multi-core architectures, where a number of relative simple processor cores are used to simultaneously execute many processes. Thus, the main challenge isshifted to proving the correctness of a single core with hardware support for multithreading, and then of the composition of the cores. The innovation will enhance the scientific and technological understanding by developing automatic and scalable technology to formally verify complex multicore processors. The potential societal benefits are correct, safe, and reliable microprocessors,which is critical, given that millions of microprocessors function autonomously in safety-critical applications. The potential commercial impact of the project will be significant, since the customers will be semiconductor and Intellectual Property design companies that develop microprocessorsor systems on a chip. Since verification is consuming up to 90% of the engineering effort and failing to scale for complex designs, an efficient formal verification technology will have significant potential for commercialization. The technology area of application includes all market sectors that can use high-performance microprocessors, including embedded products, and thus is unlimited.

这个小型企业创新研究（SBIR）第一阶段项目将为芯片多线程多核处理器的设计和正式验证提供一种有效和可扩展的方法，其中单个内核具有多线程的硬件支持。该方法将在OpenSPARC T2处理器上开发和优化，这是Sun UltraSPARCT2？这个行业呢?S优先？芯片上的服务器？封装了所有通用处理器中最多的内核和线程，并在单个芯片上集成了服务器的所有关键功能：计算、网络、安全和输入/输出，以及与Solaris操作系统的紧密集成。这项工作将基于扩展一个极其有效的原型工具流，用于对流水线处理器进行正式验证，其性能优于其他方法的数量级，同时需要最少的人工干预。预期的技术成果是用于正式验证芯片多线程多核处理器的高度自动化和可扩展的方法和工具流，其中单个内核具有多线程的硬件支持。该项目的广泛影响/商业潜力将基于芯片多线程（CMT）多核处理器可靠性的显著提高，其中单个核心具有多线程硬件支持。由于功耗限制，性能不能再通过增加单个核心的频率和/或复杂性来获得。相反，半导体公司正在采用多核架构，在这种架构中，许多相对简单的处理器核心被用来同时执行许多进程。因此，主要的挑战转移到证明具有多线程硬件支持的单核的正确性，然后是核的组合。这项创新将通过开发自动和可扩展的技术来正式验证复杂的多核处理器，从而增强科学和技术的理解。潜在的社会效益是正确、安全和可靠的微处理器，这是至关重要的，因为数百万微处理器在安全关键应用中自主运行。该项目的潜在商业影响将是巨大的，因为客户将是在芯片上开发微处理器系统的半导体和知识产权设计公司。由于验证消耗了高达90%的工程努力，并且无法对复杂的设计进行扩展，因此有效的正式验证技术将具有巨大的商业化潜力。应用的技术领域包括所有可以使用高性能微处理器的市场领域，包括嵌入式产品，因此是无限的。