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

Research on Development of Formal Logic Design Verifier for Microprocessors

Research Project

Project/Area Number 07558155
Research Category

Grant-in-Aid for Scientific Research (A)

Allocation TypeSingle-year Grants
Section試験
Research Field 計算機科学
Research InstitutionKYOTO UNIVERSITY

Principal Investigator

YAJIMA Shuzo  Kyoto University, Guraduate School of Engineering, Professor, 工学研究科, 教授 (20025901)

Co-Investigator(Kenkyū-buntansha) OGINO Hiroyuki  Kyoto University, Guraduate School of Engineering, Instructor, 工学研究科, 助手 (40144323)
TAKENAGA Yasuhiko  Kyoto University, Guraduate School of Engineering, Instructor, 工学研究科, 助手 (20236491)
HAMAGUCHI Kiyoharu  Osaka University, Feculty of Engineering Science, Lecturer, 基礎工学部, 講師 (80238055)
平石 裕実  京都産業大学, 工学部, 教授 (40093299)
Project Period (FY) 1995 – 1996
Project Status Completed (Fiscal Year 1996)
Budget Amount *help
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 1996: ¥2,200,000 (Direct Cost: ¥2,200,000)
KeywordsFormal design verification / Function level design / temporal logic / First-order Predicate logic / model checking / logic function manipulation / binary decision diagram / マイクロプロセッサ / 調理関数処理 / 二分モーメントグラフ / 三分決定グラフ / 機能レベル検証 / 算術演算回路検証
Research Abstract

The aim of this research is to develop a formal verifier for large sequential circuits, in particular, microprocessors. Although arithmetic circuits such as multipliers are crucial components in microprocessor designs, it was a hard problem to verify them. We developed a new algorithm using binary moment diagrams, and showed that it is possible to verify multipliers, which were typical hard problems in formal verification. Furthermore, we developed a new efficient algorithm for formal verification based on linear time temporal logic, which can describe temporal properties more easily than the other temporal logics. In order to deal with circuits at function level than at logic level, we took a logic known as quantifier-free first-order predicate logic with equality. We introduced temporal operators similar to those of the above linear time temporal logic, and proved that its validity checking problem is decidable. We improved this algorithm in terms of required time and space, and implemented the algorithm to show its effectiveness. Furthermore we showed that the optimal variable ordering problem of binary decision diagrams is NP-complete. We also investigated the computational power of a variant binary decision diagrams which have nondeterministic nodes.

Report

(3 results)
  • 1996 Annual Research Report   Final Research Report Summary
  • 1995 Annual Research Report
  • Research Products

    (5 results)

All Other

All Publications (5 results)

  • [Publications] Kiyoharu HAMAGUCHI: "Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits" Proceedings of IEEE/ACM International Conference on Computer Aided Design (ICCAD-95). 78-82 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Kiyoharu HAMAGUCHI: "Efficient construction of Binary Moment Diagrams for Verifying Arithmetic Circuits" Proceedings of IEEE/ACM International Conference on Computer-Aided Design (ICCAD-95). 78-82 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] K. Hamaguchi: "Efficient Construction of Binary Moment Digarams for Verifying Arithmefic Circuits." 1995 IE^3/ACM International Conference an Computer-Aided Design. 78-82 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] H. Hiraishi: "Towands Verifaccition of Bit-Slice Circuits-Time-Space Model Checlcrg Approach-" IEICE Trans. Information and Systems. E78-D. 791-795 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] H. Hiraishi: "Time-Space Modal Logic for Verification of Biy-Slice Circuits" Proc. 4th Computer-Aidal Design and Computar Graphics. 675-680 (1995)

    • Related Report
      1995 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi