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

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.