权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Research on Computer Aided Formal Verification Based on Temporal Logics

基于时态逻辑的计算机辅助形式验证研究

基本信息

批准号：
03650301
负责人：
HIRAISHI Hiromi
金额：
$ 1.79万
依托单位：
Kyoto Sangyo University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1991
资助国家：
日本
起止时间：
1991 至 1992
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-03650301/
关键词：
Logic Design Verification Formal Verification Temporal Logic Computer Aided Design Binary Decision Diagram 計算機援用設計ベクトル計算機

项目摘要

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.

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