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

Award Information
National Science Foundation
Award Year:
Phase I
Agency Tracking Number:
Solicitation Year:
Solicitation Topic Code:
Solicitation Number:
Small Business Information
Aries Design Automation
6157 North Sheridan Road, Suite 16M, Chicago, IL, 60660
Hubzone Owned:
Minority Owned:
Woman Owned:
Principal Investigator:
Miroslav Velev
(773) 856-6633
Business Contact:
Miroslav Velev
(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.

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