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 Launchbury，约翰俄勒冈研究生院博士后：博士后研究助理方法下微处理器微架构的验证正在开发中，用于验证微处理器微架构的并发属性，例如活性和顺序等效性。现有的验证技术正在 Hawk 微架构规范语言的背景下进行调整、集成和评估。本研究的目的是证明设计抽象的使用使得形式验证技术能够用于验证完整微架构的重要属性。这项工作与进一步开发 Hawk 语言实现以及使用 Hawk 指定商业微处理器的现实模型及其所有意外复杂性的并行研究相结合。 Hawk 语言提供的抽象使此目的所需的大部分信息变得明确，并且 Hawk 规范的简洁性和紧凑性为验证问题提供了强大的杠杆作用。特别是，Hawk 规范避免了典型逻辑级规范的许多细节。此外，Hawk 的声明性性质为其形式操作提供了巨大的潜力。通过将适当的时序逻辑与模型检查相结合，正在构建新的混合验证技术。时序逻辑用于表达感兴趣的并发属性，并通过 Hawk 规范的抽象解释自动构建模型。