• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Research on formal verification of asynchronous logic circuits with bounded delays

Research Project

Project/Area Number 09680329
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionTOKYO 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)
KeywordsFormal 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)
  • 1998 Annual Research Report   Final Research Report Summary
  • 1997 Annual Research Report
  • Research Products

    (7 results)

All Other

All Publications (7 results)

  • [Publications] T.Yoneda, B.Zhou, H.Schlingloff: "Verification of bounded delay asynchronous Circuits with timed traces" Proceedings of AMAST'98. LNCS1548. 59-73 (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] 周 斌, 米田 友洋: "有限遅延幅モデルにおける非同期式回路の検証について" 電子情報通信学会和文論文誌D-I分冊. 印刷中. (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] Tomohiro Yoneda, Hiroshi Ryu: "Timed trace theoretic verification using partial order reduction" Proceedings of ASYNC'99. 印刷中. (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] T.Yoneda, B.Zhou, H.: "Schlingloff, Verification of bounded delay asynchronous circuits with timed traces" Proceedings of AMAST'98, LNCS. 1548. 59-73 (1999)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] Bin Zhou: "Tomohiro Yoneda, Verification of asynchronous circuits with bounded delay model" Trans.of IEICE. (to appear). (1999)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] Tomohiro Yoneda: "Hiroshi Ryu, Timed trace theoretic verification using partial order reduction" Proceedings of ASYNC'99. (to appear). (1999)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1998 Final Research Report Summary
  • [Publications] 周 斌,米田友洋: "有限遅延幅モデルにおける非同期式回路の検証について" 電子情報通信学会和文論文誌. (掲載予定). (1999)

    • Related Report
      1998 Annual Research Report

URL: 

Published: 1997-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi