Research on formal verification of asynchronous logic circuits with bounded delays
Project/Area Number  09680329 
Research Category 
GrantinAid for Scientific Research (C)

Section  一般 
Research Field 
計算機科学

Research Institution  TOKYO INSTITUTE OF TECHNOLOGY 
Principal Investigator 
YONEDA Tomohiro TOKYO INSTITUTE OF TECHNOLOGY,Graduate School of Information Science and Engineering, Associate Professor, 大学院・情報理工学研究科, 助教授 (30182851)

Project Fiscal Year 
1997 – 1998

Project Status 
Completed(Fiscal Year 1998)

Budget Amount *help 
¥2,400,000 (Direct Cost : ¥2,400,000)
Fiscal Year 1998 : ¥700,000 (Direct Cost : ¥700,000)
Fiscal Year 1997 : ¥1,700,000 (Direct Cost : ¥1,700,000)

Keywords  Formal verification / Asynchronous circuits / Bounded delay model / Time Petri nets / Timed trace theory / Partial order reduction / 形式的検証 / 非同期式回路 / 有限遅延幅モデル / タイムペトリネット / 時間トレース理論 / Partial Order Reduction 
Research Abstract 
Asynchronous circuits are usually modeled with a speed independent model, where the gate delays are unbounded or bounded by an unknown constant. Most of the research on design. synthesis. and verification of asynchronous circuits has been done under this model. Although the speed independent model is quite simple. the possibility of unbounded delay sometimes forces the designer to add additional complexity to the circuit.. Recently. in order to design fast, compact asynchronous circuits, the bounded delay model is often assumed. However. these timed asynchronous circuits can no longer be verified accurately using the untimed verification algorithms. Therefore. in this research, we aim at building a timed model which can properly express those timed circuits. and developing the verification algorithm based on the model, In the first year, we theoretically formalized the verification method based on timed trace theory, and proved the correctness of the implementation of the verification
… More
method using time Petri nets. Then, we tried to apply the partial order reduction technique, which traverses only some subset of successor states as long as the correctness is not affected, to the timed verification method. According to the experimental results obtained by a prototype, the effectiveness of the method was shown. In the second year. for the theoretical part, we proposed several definitions for the correctness based on the timed trace theory, and derived the sufficient conditions that the algorithm to check the correctness is implementable. Further. we proved the correctness of the partial order reduction algorithm that we proposed last year. For the practical part. we implemented the second version of the verification algorithm based on the partial order reduction. By using it, we could verify various timed asynchronous circuits much more efficiently than by using previous method. Further, in order to reduce the memory use in the verification method, we proposed techniques for sharing. compressing. and thinning out the visited state information. These techniques could allow us to reduce the large amount of memory use with a little overhead in the CPU times. We are planning to improve the manmachine interface of the program, and to release it as a tool. Less

Report
(4results)
Research Output
(7results)