Research on Computer Aided Formal Verification Based on Temporal Logics

为了建立基本的形式化验证方法，我们利用时序逻辑对有限状态机的形式化设计验证进行了研究，取得了以下主要成果：1.基于时态逻辑的有限状态机形式化设计验证。分支时间规则时态逻辑：我们提出了一种新的分支时间模型时态逻辑BRTL，它在保持与CTL相似的验证复杂性的同时，具有比传统的CTL更强的表达能力。给出了有效的BRTL符号模型检测算法，并开发了一个实验验证系统。我们将该系统应用于一个8位微处理器(KUE-Chip 2)的验证，并显示了其有效性。形式化验证算法：我们提出了两种新颖的验证算法。一种是二叉决策图(BDD)操作的矢量化算法，这在符号模型检测中是必不可少的。矢量化算法获得了20倍的矢量加速比。另一种是自下而上的逆图像计算算法，这是基于时序逻辑的符号模型检测的关键操作。该算法在Kue-Chip 2验证中获得了高达40倍的速度。实际逻辑系统的形式化验证：我们使用BRTL对Kue-Chip 2微处理器的设计进行了验证，结果表明该设计存在设计错误，并且除了这些设计错误之外，设计是正确的。在验证过程中，我们将内存抽象为对内存的输入/输出命令。这种抽象使得验证整个芯片的正确性成为可能。我们还使用CTL验证了Future Bus(IEEE多微处理器系统分层总线标准)的高速缓存一致性协议。在这种情况下，我们将共享内存和缓存抽象为1位内存，并证明了该抽象很好地模拟了缓存一致性属性。

Aiming at establishment of fundamental formal verification methodology, we investigated formal design verification of finite state machines using temporal logics and have got the following major results.1. Branching time regular temporal logic : We proposed a new branching time model temporal logic called BRTL which has more expressive power than the conventional CTL while keeping its verification complex similar to that of CTL. We showed efficient symbolic model checking algorithm of BRTL and developed an experimental verification system. We applied the system to a verification of an 8 bit microprocessor (KUE-Chip 2) and showed its effectiveness.2. Formal Verification Algorithms : We proposed two original algorithms for verification. One is a vectorized algorithm for manipulation of binary decision diagrams (BDD's) which is essential in symbolic model checking. The vectorized algorithm achieved 20 times vector acceleration ratio. The other one is a bottom-up inverse image computation algorithm which is a key operation of symbolic model checking based on temporal logics. This algorithm achieved up to 40 times speed up in KUE-Chip 2 verification.3. Formal Verification of Practical Logic Systems : We verified the design of KUE-Chip 2 microprocessor using BRTL and showed that the design contains design errors and that the design is correct except these design errors. In the verification, we abstracted the internal memory as input/output commands to the memory. This abstraction made it possible to verify the correctness of the whole chip. We also verified cache coherency protocol of Future Bus (IEEE standard of hierarchical bus for multi-microprocessor system) using CTL. In this case, we abstracted the shared memory and caches as 1 bit memories and showed that the cache coherency property is well modeled by the abstraction.