Researches on Formal Logic Design Verification Based on Regular Temporal Logic

本研究的主要目标是建立基于时间逻辑的形式逻辑设计验证的基本方法。我们得到了以下结果：1。我们提出并系统化了各种类型的规则时间逻辑，包括可以处理时间序列的*规则时间逻辑。在某种意义上，它们在表达上等价于顺序机，并且阐明了它们的各种性质。提出了一种分支时间规则时间逻辑，并给出了其线性时间复杂度的模型检验算法。我们开发了一个基于规则时间逻辑的顺序机形式化验证系统。系统采用的验证算法对顺序机的验证进行了高度调优。它直接检查被验证机器的正确性，大大减少了必要的工作面积。它成功地验证了中等规模的实际顺序机器（转换数量小于10,000左右）。针对时序验证问题，提出了一种扩展的实时时序逻辑。基于这一逻辑，给出了时序机的形式化时序验证算法，即具有门延迟的时序电路模型。为了阐明如何使用当前最强大的超级计算机验证大型顺序机器，我们提出了一种适合在向量处理器上执行的计算树逻辑的矢量化模型检验算法。我们还实现了该算法，一些基准测试结果表明，它可以在几分钟内验证具有超过100万条过渡边的大型实际顺序机。

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.