Studies on Formal Logic Design Verification

本文的主要研究成果如下：1.扩展时空模态逻辑：为了处理有限位片电路，我们对时空模态逻辑进行了扩展，引入了位位置计数器。这个计数器产生一个信号，禁止从指定的位位置输出。2.并发进程的验证：介绍了一对新的图像计算算法。它们适用于多个并发过程的验证。其主要思想是过程变量和稳态变量的提前平滑和替换。这种方法获得了10倍以上的速度。3.分布式进程排序算法：在进程排序的基础上，给出了BDD变量的排序方法。提出了一种分布式分支定界进程排序算法。在25台计算机上的实验测试表明，该算法在25台计算机上获得了超线性的速度提升。4.任务控制体系结构（TCA）的验证：作为众多并发进程的一个例子，我们尝试验证TCA的无死锁性。提出了一种不使用公平性约束的无死锁TCA验证方法。这种方法获得了100倍以上的速度。

The major results of this research are as follows :1.Extended Time-Space Modal Logic : In order to treat finite bit-slice circuit, we extend the Time-Space Modal Logic by introducing bit-position counter. This counter generates a signal that disables outputs from the specified bit position.2.Verification of Concurrent Processes : A couple of new image computation algorithms are introduced. They are suitable for verification of many concurrent processes. The main idea is early smoothing and substitution of process variables and stable state variables. This method gains more than 10 times speed up. We also showed a non-deterministic substitution method for state variables.3.Distributed Process Ordering Algorithm : We give BDD variable ordering based on process ordering. A distributed branch-and-bound algorithm for process ordering is proposed. The experimental measurements on 25 computers show that it gains super-linear speed up over 25 computers.4.Verification of Task Control Architecture (TCA) : As an example of many concurrent processes, we tried to verify deadlock free property of TCA.Verification of deadlock free property of concurrent processes requires fairness constraints in general, which is very time-consuming. We introduced a new method for verification of deadlock free property of TCA without using fairness constraints. This method gains more than 100 times speed up.