System-Level Processor Verification Using Refinement

提案编号：0429924机构：格鲁吉亚技术研究公司- GA技术研究所主要研究员：Manolios，PanagiotisTitle：系统级处理器验证使用精炼摘要：本提案的目的是开发一个正式的精炼为基础的方法，用于术语级微处理器验证，并将其应用于复杂的设计。最先进的微处理器非常复杂，行业估计验证成本占开发新产品所需工程工作的比例从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.