Parallel and Distributed Formal Logic Design Verification for Workstation Cluster System

并行和分布式形式逻辑设计验证算法已被研究。主要结果包括：1.二叉决策图（BDD）的并行处理：提出了一种基于逻辑函数动态余因式分解的BDD分解算法。根据BDD的构建进度进行细化，并在集群机器上并行处理分解的BDD。通过这种并行算法，我们获得了超线性效果.并行优化算法：提出了一种高效的并行优化搜索算法。该算法基于动态任务划分和分配，适合于机群系统上的并行执行。将其应用于最优排序问题，得到了超线性效果.并行系统的设计验证：提出了早期过程变量消除方法，以提高并发过程系统符号模型检验的效率。此外，提出了一种基于任务控制体系结构（TCA）的机器人控制程序无死锁性验证方法。将这两种方法相结合，在验证TCA的无死锁性时，速度提高了100倍以上.并行排序算法：并行双调排序算法已经在集群系统上进行了评估。在由多个交换集线器连接的机群系统中，交换集线器之间的通信成为并行双调排序的瓶颈。另一方面，通过全带宽结构的cLAN网络连接的机群系统，即VIA连接，在并行双调排序中不存在瓶颈

Parallel and distributed formal logic design verification algorithms have been studied. Major results include:1. Parallel processing of Binary Decision Diagrams (BDD): An algorithm for decomposition of BDDs based on dynamic cofactoring of logic functions has been proposed. Refinement of cofactoring occurs according to the progress of construction of BDDs and the decomposed BDDs are processed in parallel on cluster machines. We obtained super-linear effect by this parallel algorithm.2. Parallel optimization algorithm: An efficient parallel optimization and searching algorithm has been proposed. It is based on dynamic job divisions and assignments and is suitable for parallel execution on cluster system. We applied it to optimum ordering problem and obtained super-linear effect.3. Design verification of parallel systems: Early process variable elimination method has been proposed to improve efficiency of symbolic model checking of concurrent process systems. In addition, a new approach to verification of dead-lock free property of robot control programs based on Task Control Architecture (TCA) has been proposed. By combining these two methods, we obtained more than 100 times speed up in verification of dead-lock free property of TCA.4. Parallel sorting algorithm: Parallel bitonic sorting algorithm has been evaluated on cluster system. On cluster system connected by other network using multiple switching hubs, it has been shown that the communication between switching hubs become bottle neck of the parallel bitonic sorting. On the other hand, it has been shown that cluster system connected by cLAN network with full band-width configuration, which is VIA connection, has no bottle neck in parallel bitonic sorting