Research on formal verification of asynchronous logic circuits with bounded delays
| Project/Area Number |
09680329
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| 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 Period (FY) |
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 man-machine interface of the program, and to release it as a tool. Less
|
Report
(3 results)
Research Products
(7 results)
