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.
We invented techniques that allow us to automatically formally verify pipelined processors with hardware support for multithreading. These techniques are based on efficient use of the property of Positive Equality that results in orders of magnitude speedup. To the best of our knowledge, this is the first work on automatic formal verification of multithreaded pipelined processors. We also developed techniques that allow us to formally verify the integration of multithreaded pipelined processors in a multi-processor chip via a shared memory system that they are connected to with switches. We also invented techniques that allow us to formally verify the integration of a pipelined processor with an array of reconfigurable functional units. These techniques are applicable for any implementation of the reconfigurable functional units, for any number of them, and for any topology of the connections between the functional units. Reconfigurable processors offer significantly increased performance at reduced power consumption, compared to conventional processors. To the best of our knowledge, this is the first work on automatic formal verification of the integration of pipelined processors with arrays of reconfigurable functional units. We also developed an automated debugging method that allows us to efficiently locate and correct bugs when formally verifying pipelined, superscalar, or VLIW processors. The method is at least an order of magnitude more efficient compared to previous approaches. This is critical, because debugging consumes 50% of the verification time, which takes two-thirds to 90% of the design cycle for new microprocessors.
