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

Period of Performance: 01/01/2010 - 12/31/2010

$150K

Phase 1 SBIR

Recipient Firm

Aries Design Automation, LLC
2705 West Byron Street
Chicago, IL 60618
Principal Investigator

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.