CISE PostDoc: Verification of Microprocessor Microarchitecture

9805542 Launchbury，John俄勒冈州 PostDoc：微处理器微架构验证 根据博士后研究协会的方法正在开发验证并发性能的微处理器微体系结构，如活性和顺序等效。现有的验证技术正在调整，整合和评估的背景下，鹰微体系结构规范语言。本研究的目的是证明，使用设计抽象，使形式验证技术被用来验证完整的微架构的重要属性。这项工作融合了并行研究，进一步发展的鹰语言实现，并使用鹰来指定商业微处理器的现实模型，其所有的意外复杂性。 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.