Research on Computer Aided Formal Verification Based on Temporal Logics

本文以建立基本的形式化验证方法为目标，研究了基于时序逻辑的有限状态机的形式化设计验证问题，取得了以下主要成果.分支时间规则时序逻辑：我们提出了一种新的分支时间模型时序逻辑BRTL，它比传统的CTL具有更强的表达能力，同时保持其验证复杂性与CTL相似。给出了有效的BRTL符号模型检测算法，并开发了一个实验验证系统。并将该系统应用于一个8位微处理器（KUE-Chip 2）的验证中，验证了该系统的有效性.形式验证算法：我们提出了两个原始的验证算法。一个是一个向量化的算法操纵的二元决策图（BDD的），这是必不可少的符号模型检查。矢量化算法实现了20倍的矢量加速比。另一种是基于时序逻辑的符号模型检测的关键操作--自底向上的逆像计算算法。该算法在KUE-Chip 2验证中实现了高达40倍的加速.实用逻辑系统的形式验证：我们使用BRTL验证了KUE-Chip 2微处理器的设计，并表明该设计包含设计错误，并且除了这些设计错误之外，该设计是正确的。在验证中，我们将内部存储器抽象为存储器的输入/输出命令。这种抽象使得验证整个芯片的正确性成为可能。我们还使用CTL验证了Future Bus（IEEE多微处理器系统层次总线标准）的Cache一致性协议。在这种情况下，我们将共享内存和高速缓存抽象为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.