CISE PostDoc: Verification of Microprocessor Microarchitecture

9805542俄勒冈州朗奇伯里研究所博士后：正在开发博士后研究协会方法下的微处理器微体系结构验证，以验证微处理器微体系结构的并发属性，如活性和顺序等价性。正在根据HAWK微体系结构规范语言对现有的验证技术进行调整、整合和评估。这项研究的目的是证明，设计抽象的使用使得形式验证技术能够用于验证完整微体系结构的重要特性。这项工作与进一步开发Hawk语言实现的并行研究相结合，并使用Hawk来指定商业微处理器的现实模型，以及它们所有的意外复杂性。Hawk语言提供了抽象，显式地提供了此目的所需的大量信息，而Hawk规范的简洁和紧凑为验证问题提供了强大的杠杆作用。特别是，HAWK规范避免了典型的逻辑级规范的许多细节。此外，霍克的陈述性为其提供了极大的形式操纵潜力。通过将适当的时态逻辑与模型检测相结合，正在建立新的混合验证技术。使用时态逻辑来表示感兴趣的并发属性，并通过对Hawk规范的抽象解释来自动构建模型。

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.