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

Award Information
National Science Foundation
Solitcitation Year:
Solicitation Number:
NSF 09-541
Award Year:
Phase I
Agency Tracking Number:
Solicitation Topic Code:
Small Business Information
Aries Design Automation
2705 W Byron St, Chicago, IL, 60618
Hubzone Owned:
Woman Owned:
Socially and Economically Disadvantaged:
Principal Investigator
 Miroslav Velev
 (773) 856-6633
Business Contact
 Miroslav Velev
Title: DPhil
Phone: (773) 856-6633
Research Institution
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.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government