SBIR Phase I: Techniques for Analysis of Counterexamples from Formal Verification of High-Level Microprocessor Designs

Award Information
Agency: National Science Foundation
Branch: N/A
Contract: 0611382
Agency Tracking Number: 0611382
Amount: $100,000.00
Phase: Phase I
Program: SBIR
Solicitation Topic Code: EO
Solicitation Number: NSF 05-605
Solicitation Year: 2005
Award Year: 2006
Award Start Date (Proposal Award Date): N/A
Award End Date (Contract End Date): N/A
Small Business Information
6157 North Sheridan Road, Suite 16M, Chicago, IL, 60660
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: Y
Principal Investigator
 Miroslav Velev
 (773) 856-6633
Business Contact
 Miroslav Velev
Title: Dr
Phone: (773) 856-6633
Research Institution
This Small Business Innovation Research (SBIR) Phase I research proposes to study the feasibility of automatic methods for analysis of counterexamples from formal verification of pipelined and superscalar microprocessors modeled at a high level of abstraction. Aries Design Automation has developed an automatic tool flow for formal verification of such designs that scales for very complex and elaborate models. The formal verification is done by efficient translation of a correctness condition to a Boolean formula that can be evaluated with any Boolean Satisfiability (SAT) procedure, such that a satisfying assignment for that formula is a counterexample, i.e., indicates a bug. The research is to investigate methods to automatically analyze counterexamples due to single or multiple design errors - detected when proving safety of pipelined and superscalar microprocessors - in order to localize possible bug sites. Also, a visualization engine will be developed to efficiently display related information in order to help the microprocessor designers to quickly fix the bugs. It is expeced that the resulting methods and tools will significantly increase the designer efficiency and reduce the time for debugging of complex microprocessors by orders of magnitude. Billions of microprocessors are manufactured each year. Most of them function autonomously in safety-critical applications, e.g., controlling complex machines, monitoring the health of patients, and used in military systems. Thus, it is a matter of public safety and national security that microprocessors are designed without errors. However, verification has become the bottleneck in the design of new chips. We have developed formal verification technology that can be used automatically and scales for complex microprocessors. However, the lack of algorithms for automatic analysis of counterexamples prevents our technology from being used in industry. The potential commercial value is up to hundreds of millions of dollars, while companies that use this technology could make billions of dollars from increased designer productivity, reduced time to market for new chips that will be guaranteed to be correct, increased competitive advantage, high profits from early delivery of new designs to the market, and avoided expensive recalls and potentially catastrophic effects from buggy designs. This research will enhance the scientific understanding of how to automatically analyze counterexamples from formal verification of high-level models of computer systems - a novel research area. The technology will also be applicable to automatic formal verification of software.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government