权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Researches on Formal Logic Design Verification Based on Regular Temporal Logic

基于正则时序逻辑的形式逻辑设计验证研究

基本信息

批准号：
01550285
负责人：
HIRAISHI Hiromi
金额：
$ 1.47万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1989
资助国家：
日本
起止时间：
1989 至 1990
项目状态：
已结题

项目摘要

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.

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