CISE PostDoc: Verification of Microprocessor Microarchitecture

CISE 博士后：微处理器微架构验证

基本信息

批准号：
9805542
负责人：
John Launchbury
金额：
$ 6.6万
依托单位：
Oregon Graduate Institute of Science & Technology
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
1998
资助国家：
美国
起止时间：
1998-04-15 至 2000-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=9805542&HistoricalAwards=false
关键词：
CISE PostDoc Verification Microprocessor Microarchitecture

项目摘要

9805542 Launchbury, John Oregon Graduate Institute PostDoc: Verification of Microprocessor Microarchitectures Under the Post-Doctoral Research Associateship methods are being developed for verifying concurrent properties of microprocessor microarchitectures, such as liveness and sequential equivalence. Existing verification techniques are being adapted, integrated and evaluated in the context of the Hawk microarchitectural specification language. The objective of this research is to demonstrate that the use of design abstraction enables formal verification technology to be used to verify significant properties of complete microarchitectures. This work blends with parallel research on further developing the Hawk language implementation, and on using Hawk to specify realistic models of commercial microprocessors, with all their accidental complexity. The Hawk language provides abstractions that make explicit much of the information that is needed for this purpose, and the cleanliness and compactness of Hawk specifications provides powerful leverage on the verification problem. In particular, Hawk specifications avoid much of the detail of typical logic-level specifications. Further, Hawk's declarative nature provides it with great potential for formal manipulation. New, hybrid verification technology is being built by combining an appropriate temporal logic with model checking. The temporal logic is used to express the concurrent property of interest, and models are constructed automatically by abstract interpretation of Hawk specifications.

9805542 John Oregon Institute Postdoc发射公司：正在开发了博士后研究协会方法下的微处理器微构造方法的验证，以验证微处理器微结构的并发性质，例如livice和顺序等价。现有的验证技术正在根据鹰微体系规范语言进行调整，集成和评估。这项研究的目的是证明设计抽象的使用使形式验证技术可用于验证完整微体系结构的重要特性。这项工作融合了有关进一步开发鹰式语言实施的并行研究，并使用鹰来指定商业微处理器的现实模型，以及它们的所有意外复杂性。 Hawk语言提供了抽象，以明确为此目的所需的大量信息，并且鹰规范的清洁度和紧凑性为验证问题提供了强大的杠杆作用。特别是，鹰规格避免了典型逻辑级规范的大部分细节。此外，霍克的声明性质为其提供了正式操纵的巨大潜力。通过将适当的时间逻辑与模型检查相结合，正在建立新的混合验证技术。时间逻辑用于表达感兴趣的并发属性，模型是通过对Hawk规范的抽象解释自动构建的。