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

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

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.