Studies on Formal Logic Design Verification

本研究的主要成果如下：1.数据分析。扩展时-空模态逻辑：为了处理有限位片电路，我们通过引入位计数器扩展了时-空模态逻辑。这个计数器产生一个信号，该信号禁止从指定的位位置输出。并发进程的验证：介绍了几种新的图像计算算法。它们适用于验证许多并发进程。主要思想是过程变量和稳态变量的早期平滑和代入。这种方法可以提高10倍以上的速度。我们还展示了一种状态变量的非确定性替换方法。分布式流程排序算法：基于流程排序给出BDD变量排序。提出了一种用于过程排序的分布式分支定界算法。在25台计算机上的实验测量表明，该方法比25台计算机获得了超线性速度。任务控制体系结构（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.