Correctness of Pipelined Machines
Correctness of Pipelined Machines
复制标题
流水线机器的正确性
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
P. Manolios
中科院分区：
文献类型：
--
作者：
P. Manolios
流水线机器的正确性是一个被广泛研究的课题。最近的大多数工作都使用了Burch和Dill正确性概念的变体[4]。当新特征被建模时，例如，中断，正确性的新概念被开发出来。考虑到过多的正确性条件，问题出现了：什么是正确性的合理概念？我们讨论这个问题的长度和机械证明，伯奇和迪尔的正确性概念的变体是有缺陷的。我们提出了一个基于WEBs（良基等价互模拟）的正确性概念[16，19]。简单地说，我们的正确性概念意味着伊萨（指令集架构）和MA（微架构）机器具有相同的可观察无限路径，直到口吃。这意味着这两台机器满足相同的CTL*\X属性和相同的安全性和活性属性（直到口吃）。为了测试这个想法的实用性，我们使用ACL 2来验证Sawada在[22，23]中描述的简单流水线机器的几个变体。我们的变体通过添加异常（处理溢出）、中断和充实的128位ALU（其中一个是用网表语言描述的）来扩展基本机器。在所有情况下，我们证明了相同的最终定理。我们开发了一种具有机械支持的方法，用于验证Sawada的机器。由此产生的证明比原始的要短得多，并且不需要任何中间抽象;事实上，给定定义和一些通用书籍（定理集），证明是自动的。WEBs的一个实际和值得注意的特征是它们的组合性。这使我们能够在可管理的阶段证明更复杂的机器的正确性。
The correctness of pipelined machines is a subject that has been studied extensively. Most of the recent work has used variants of the Burch and Dill notion of correctness [4]. As new features are modeled, e.g., interrupts, new notions of correctness are developed. Given the plethora of correctness conditions, the question arises: what is a reasonable notion of correctness? We discuss the issue at length and show, by mechanical proof, that variants of the Burch and Dill notion of correctness are flawed. We propose a notion of correctness based on WEBs (Well-founded Equivalence Bisimulations) [16,19]. Briefly, our notion of correctness implies that the ISA (Instruction Set Architecture) and MA (Micro-Architecture) machines have the same observable infinite paths, up to stuttering. This implies that the two machines satisfy the same CTL*\X properties and the same safety and liveness properties (up to stuttering).To test the utility of the idea, we use ACL2 to verify several variants of the simple pipelined machine described by Sawada in [22, 23]. Our variants extend the basic machine by adding exceptions (to deal with overflows), interrupts, and fleshed-out 128-bit ALUs (one of which is described in a netlist language). In all cases, we prove the same final theorem. We develop a methodology with mechanical support that we used to verify Sawada's machine. The resulting proof is substantially shorter than the original and does not require any intermediate abstractions; in fact, given the definitions and some general-purpose books (collections of theorems), the proof is automatic. A practical and noteworthy feature of WEBs is their compositionality. This allows us to prove the correctness of the more elaborate machines in manageable stages.