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

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 UltraSPARC T2?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 can no 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 is shifted 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 microprocessors or 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.