Studies on Formal Logic Design Verification

点击翻译按钮获取中文摘要

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.