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

Award Information
Agency:
National Science Foundation
Branch
n/a
Amount:
$150,000.00
Award Year:
2010
Program:
SBIR
Phase:
Phase I
Contract:
0945974
Award Id:
98942
Agency Tracking Number:
0945974
Solicitation Year:
n/a
Solicitation Topic Code:
IC3
Solicitation Number:
n/a
Small Business Information
2705 W Byron St, Chicago, IL, 60618
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
361627933
Principal Investigator:
MiroslavVelev
DPhil
(773) 856-6633
miroslav.velev@aries-da.com
Business Contact:
MiroslavVelev
DPhil
(773) 856-6633
miroslav.velev@aries-da.com
Research Institute:
n/a
Abstract
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


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government