System-Level Processor Verification Using Refinement

提案编号：0429924INSTUTION：佐治亚州理工学院-GA技术研究所PRINCIPAL调查员：Manolios，Panagiotis TITLE：使用精化进行系统级处理器验证摘要：该提案的目标是开发一种用于术语级微处理器验证的形式化精化方法，并将其应用于复杂设计。最先进的微处理器极其复杂，行业估计的验证成本占开发新产品所需工程工作的百分比从30%到高达70%。即使将这样的资源分配给验证，错误也很常见，更复杂的设计的趋势将加剧问题。目前的验证工作侧重于检查小组件的低级属性。然而，很难想象有一组属性能够捕获系统级的正确性，这就是为什么该项目倡导基于细化的方法，其中指令集体系结构就是规范。这意味着对于外部观察者来说，处理器在安全性和活跃性属性方面都以与指令集体系结构一致的方式运行。该项目提议开发一种系统级验证的改进理论，并将其应用于复杂的术语级设计。基于改进的方法将是设计验证方法的一部分，它补充了设计周期，可以以组合、可扩展的方式实现自动化，并且通常适用于广泛的设计。

PROPOSAL NO: 0429924INSTITUTION: Georgia Tech Research Corporation - GA Institute ofTechnologyPRINCIPAL INVESTIGATOR: Manolios, PanagiotisTITLE: System-Level Processor Verification Using RefinementAbstract:The objective of this proposal is to develop a formal refinement-based methodology for term-level microprocessor verification and to apply it to complex designs. State-of-the-art microprocessors are extremely complex and industry estimates of validation costs, as a percentage of the engineering effort required to develop a new product, range from 30% to as high as 70%. Even with such resources allocated to validation, bugs are common and the trend toward more complex designs will exacerbate the problem. Current validation efforts focus on checking low-level properties of small components. However, it is difficult to imagine a set of properties that captures system-level correctness, which is why the project advocates a refinement-based approach, where the instruction set architecture is the specification. This means that to an external observer, the processor behaves in a fashion that is consistent with the instruction set architecture, with respect to both safety and liveness properties. The project proposes to develop a theory of refinement for system-level verification and to apply it to complex term-level designs. The refinement-based approach will be part of a design-for-verification methodology that complements the design cycle, that can be automated in a compositional, scalable way, and that is generally applicable across a wide spectrum of designs.