Researches on Formal Logic Design Verification Based on Regular Temporal Logic

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

The major goal of this research is to establish fundamental methods for formal logic design verification based on temporal logic. We have got the following results :1. We proposed and systematized various classes of regular temporal logic including * regular temporal logic which can handle omega sequences of time. They are expressively equivalent to sequential machines in a sense, and their various properties are clarified. We also proposed a branching time regular temporal logic and showed its model checking algorithm of linear time complexity.2. We developed a formal verification system for sequential machines based on regular temporal logic. The verification algorithm adopted in the system is highly tuned for verification of sequential machines. It checks the correctness of a machine under verification directly, which reduces necessary work area drastically. It succeeded to verify practical sequential machines of medium size (the number of transitions is less than around 10,000).3. Aiming at timing verification, we proposes an extended real time temporal logic. Based on this logic, the formal timing verification algorithm for timed sequential machines, which is a model of sequential circuits with gate delays, is shown.4. In order to clarify how large sequential machines can be verified by using the current most powerful supercomputers, we showed a vectorized model checking algorithm of computation tree logic, which is suitable for execution on vector processors. We also implemented the algorithm, and some benchmark results show that it can verify large practical sequential machines with more than 1 million transition edges in a few minutes.