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

1992 Fiscal Year Final Research Report Summary

Research on Computer Aided Formal Verification Based on Temporal Logics

Research Project

Project/Area Number 03650301
Research Category

Grant-in-Aid for General Scientific Research (C)

Allocation TypeSingle-year Grants
Research Field 情報工学
Research InstitutionKyoto Sangyo University

Principal Investigator

HIRAISHI Hiromi  Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)

Co-Investigator(Kenkyū-buntansha) ISHIURA Nagisa  Osaka Univ., Engineering, Lecturer, 工学部, 講師 (60193265)
Project Period (FY) 1991 – 1992
KeywordsLogic Design Verification / Formal Verification / Temporal Logic / Computer Aided Design / Binary Decision Diagram
Research Abstract

Aiming at establishment of fundamental formal verification methodology, we investigated formal design verification of finite state machines using temporal logics and have got the following major results.
1. Branching time regular temporal logic : We proposed a new branching time model temporal logic called BRTL which has more expressive power than the conventional CTL while keeping its verification complex similar to that of CTL. We showed efficient symbolic model checking algorithm of BRTL and developed an experimental verification system. We applied the system to a verification of an 8 bit microprocessor (KUE-Chip 2) and showed its effectiveness.
2. Formal Verification Algorithms : We proposed two original algorithms for verification. One is a vectorized algorithm for manipulation of binary decision diagrams (BDD's) which is essential in symbolic model checking. The vectorized algorithm achieved 20 times vector acceleration ratio. The other one is a bottom-up inverse image computation algorithm which is a key operation of symbolic model checking based on temporal logics. This algorithm achieved up to 40 times speed up in KUE-Chip 2 verification.
3. Formal Verification of Practical Logic Systems : We verified the design of KUE-Chip 2 microprocessor using BRTL and showed that the design contains design errors and that the design is correct except these design errors. In the verification, we abstracted the internal memory as input/output commands to the memory. This abstraction made it possible to verify the correctness of the whole chip. We also verified cache coherency protocol of Future Bus (IEEE standard of hierarchical bus for multi-microprocessor system) using CTL. In this case, we abstracted the shared memory and caches as 1 bit memories and showed that the cache coherency property is well modeled by the abstraction.

  • Research Products

    (22 results)

All Other

All Publications (22 results)

  • [Publications] H.OCHI: "Breadth-First Manipylation of SBDD of Boolean Functions for Vector Processing" Proc.28th Design Automation Conference. 413-416 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] H.HIRAISHI: "Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification" Proc.3rd Workshop on Computer Aided Verification. 1. 279-290 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "Formal Verification of Speed-Depebdent Asynchronus Circuits Using Symbolic Model of Branching Time Regular Temporal Logic" Proc.3rd Workshop on Computer Aided Verification. 2. 478-488 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] H.OCHI: "A Vector Algorithm for Mabipulating Boolean Functions Basedon Shared Binary Decision Diagrams" Proc.International Symposium on Supercomputing. 191-200 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] N.ISHIURA: "Minimization of Binary Decision Diagrams Based on Exchanbges of Variables" Proc.International Symposium on Supercomputing. 472-475 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic" IEICE Tran.Fundamentals of Electronics,Communications and Computer Sciences. E75-A. 1220-1229 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "∞Regular Temporal Logic and Its Model Checking Problem" Theoretical Computer Science. 103. 19-204 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "Design Verification of Asynchronous Sequential Cirocuits Using Symbolic Model Checking" Proc.Interbational Symposium on Logic Synthesis and Microprocessor Architecture. 84-90 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "Design Verification of Microprocessor Using Brabching Time Regular Temporal Logic" Proc.4th Workshop on Computer Aided Verification. 201-212 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.HAMAGUCHI: "Formal Verification of Sequential Circuits Based on Symbolic Model Checking for Branching Time Regular Temporal Logic" Proc.Synthesis an Simulation Meeting and International Interchange. 243-252 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] K.KAWAKUBO: "Formal Verification of Fail-safeness of a Comparator for Redundant System Using Regular Temporal Logic" Proc.1st Asian Test Symposium. 2-7 (1992)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] H.Ochi: "Breadth-First Manipulation of SBDD of Boolean Functions for Vector Processing" Proc. 28th Design Automation Conference. 413-416 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] H.Hiraishi: "Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification" Proc. 3rd Workshop on Computer Aided Verification. Vol.1. 279-290 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "Formal Verification of Speed-Dependent Asynchronous Circuits Using Symbolic Model Checking of Branching Time Regular Temporal Logic" Proc. 3rd Workshop on Computer Aided Verification. Vol1.2. 478-488 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] H.Ochi: "A Vector Algorithm for Manipulating Boolean Functions Based on Shared Binary Decision Diagrams" Proc. International Symposium on Supercomputing. 191-200 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] N.Ishiura: "Minimization of Binary Decision Diagrams Based on Exchanges of Variables" Proc. International Conference on Computer-Aided Design. 472-475 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Regular Temporal Logic" IEICE. Vol.E75-A. 1220-1229 (1992)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "* Regular Temporal Logic and Its Model Checking Problem" Theoretical Computer Science. 103. 191-204 (1992)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "Design Verification of Asynchronous Sequential Circuits Using Symbolic Model Checking" Proc.Intern.Symp.Logic Synthesis and Microprocessor Architecture. 84-90 (1992)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic" Proc. 4th Workshop on Computer Aided Verification. 201-212 (1992)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Hamaguchi: "Formal Verification of Sequential Circuits Based on Symbolic Model Checking for Branching Time Regular Temporal Logic" Proc. Synthesis and Simulation Meeting and International Interchange. 243-252 (1992)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] K.Kawakubo: "Formal Verification of Fail-safeness of a Comparator for Redundant System Using Regular Temporal Logic" Proc. 1st Asian Test Symposium. 2-7 (1992)

    • Description
      「研究成果報告書概要(欧文)」より

URL: 

Published: 1994-03-24  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi