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

这项小型企业创新研究(SBIR)第一阶段研究建议研究在高抽象级别建模的流水线和超标量微处理器的形式验证中用于反例分析的自动方法的可行性。Aries Design Automation已经开发了一套用于此类设计的正式验证的自动工具流程，该流程可适用于非常复杂和精细的模型。形式验证通过将正确性条件有效地转换成可用任何布尔可满足性(SAT)过程来评估的布尔公式来完成，使得对该公式的令人满意的赋值是反例，即指示错误。这项研究是为了研究自动分析由于单个或多个设计错误而导致的反例的方法-在证明流水线和超标量微处理器的安全性时检测到-以便定位可能的错误位置。此外，还将开发一个可视化引擎来高效地显示相关信息，以帮助微处理器设计人员快速修复错误。预计由此产生的方法和工具将显著提高设计者的效率，并将复杂微处理器的调试时间减少数量级。每年制造数十亿个微处理器。它们中的大多数在安全关键应用中自主运行，例如控制复杂的机器、监测患者的健康，并用于军事系统。因此，微处理器的设计没有错误，这是一个公共安全和国家安全的问题。然而，验证已经成为新芯片设计的瓶颈。我们已经开发了可自动使用并可扩展到复杂微处理器的正式验证技术。然而，缺乏自动分析反例的算法阻碍了我们的技术在工业中的应用。潜在的商业价值高达数亿美元，而使用这项技术的公司可以从以下方面获得数十亿美元的收入：提高设计师的生产率，缩短保证正确的新芯片的上市时间，增加竞争优势，通过提前向市场交付新设计获得高额利润，避免代价高昂的召回，以及避免有缺陷的设计带来的潜在灾难性影响。这项研究将加强对如何从计算机系统高级模型的形式验证中自动分析反例的科学理解--这是一个新的研究领域。该技术还将适用于软件的自动正式验证。

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.