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

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

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.