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

1991 Fiscal Year Final Research Report Summary

Research on Efficient Manipulation of Boolean Functions Using Shared Binary Decision Diagrams and Its Application to Computer Aided Logic Design

Research Project

Project/Area Number 02452162
Research Category

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

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

Principal Investigator

YAJIMA Shuzo  Kyoto University, Faculty of Engineering, ProFessor, 工学部, 教授 (20025901)

Co-Investigator(Kenkyū-buntansha) OGINO Hiroyuki  Kyoto University, Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
TAKENAGA Yasuhiko  Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (20236491)
ISHIURA Nagisa  Osaka University, Faculty of Engineering, Lecturer, 工学部, 講師 (60193265)
TAKAGI Naofumi  Kyoto University, Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (10171422)
HIRAISHI Hiromi  Kyoto University, Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (40093299)
Project Period (FY) 1990 – 1991
KeywordsBoolean Function / Binary Decision Diagram / Boolean Function Manipulation / computer Aided Design / Symbolic Simulation / Timing Verification / Logic Design Verification / Computational complexity
Research Abstract

We have carried out researches on efficient representation and manipulation of Boolean functions, and applied them to computer aided logic design.
1. Efficient Representation and Manipulation of Boolean Functions
We have carried out researches on the efficient representation of Boolean functions using Shared Binary Decision Diagrams (SBDDs). For efficient manipulation of SBDDS, we have proposed attributed edges. We have developed a vector algorithm for manipulating SBDDs. We have also investigated variables ordering methods for minimizing SBDDs.
2. Computer Aided Logic Design Using Shared Binary Decision Diagrams
We have applied Boolean function manipulation to fault diagnosis and timing verification of logic circuits. On fault diagnosis, we have developed efficient fault simulation methods for multiple faults and novel methods of generating compact test sets. On timing verification, we have developed methods for simulating logic circuits with nondeterministic delays.
3. Formal Verification of Logic Design Using Shared Binary Decision Diagrams
We have proposed a method to represent state transition diagrams using SBDDs. Based on the method, we have developed a formal verification algorithm on branching time regular temporal logic, and implemented a formal verification system for sequential machines.
4. Computational Complexity of Boolean Function Manipulation
We have clarified the class of functions efficiently expressed by BDDs. We have also developed a paranelization methods for manipulating BDDs and clarified the computational complexity.
5. Systems for Computer Aided Logic Design
We have developed a package software so as to make it easy to manipulate SBDDs on tools for computer aided logic design.

  • Research Products

    (24 results)

All Other

All Publications (24 results)

  • [Publications] 平石 裕実: "有限オ-トマトンと表現等価な正則時相論理とその論理設計検証への応用" 情報処理学会論文誌. 31. 1134-1145 (1990)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 松本 忍: "ブ-ル式処理による不完全指定順序機械の最小化" 情報処理学会論文誌. 32. \1644-1652 (1990)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 湊 真一: "論理関数の共有二分決定グラフによる表現とその効率的処理手法" 情報処理学会論文誌. 32. 77-85 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Y.Deguchi: "Coded Time-Symbolic Simulation:Simulation of Logic Ciucuits with Nondetermimistic Delays Based on Boolean Function Monipulation" Proceeding of the Synthesis and Simulation Meeting and International Interchange. 149-156 (1990)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] N.Takahashi: "Fault Simulation for Multiple Faults using Shaved Binary Decision Diagrams" Proceeding of the Syntesis and Simulation Meeting and International Interchange. 157-164 (1990)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] N.Ishiura: "A Class of Logic Functions Expressible by Polynomial-Size Binary Decision Diagrams" Proceeding of the Synthesis and Simulation Meeting and International Interchange. 48-54 (1990)

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

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Y.Deguchi: "Probabilistic CTSS:Analysis of Timing Error Probability in Asynchronous Logic Circuits" Proceedings of 28th ACM/IEEE Design Automation Conference. 650-655 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] H.Hiraishi: "Vectorized Symbolic Model Checking of Computation Tree Logic" Procceedings of the Workshop on Computer-Aided Verification. 279-290 (1991)

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

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

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] N.Takahashi: "Fault Simulation for Multiple Faults Using Shaved BDD Representation of Fault Sets" Proceedings of IEEE International Conference on Computer-Aided Design. 550-553 (1991)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Hiromi Hiraishi: ""Regular Temporal Logic Expressively Equivalent to Finite Automata and Its Application to Logic Design Verification"" Transactions of Information Processing Society Japan. 31. 1134-1145 (1990)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Shinobu Matsumoto: ""Minimization of Incompletely Specified Sequential Machines"" Transaction of Information Processing Society Japan. 31. 1644-1652 (1990)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Shin-ichi Minato: ""Shared Binary Decision diagrams for Efficient Boolean Function Manipulation"" Transaction of Information Processing Society Japan. 32. 77-85 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Yutaka Deguchi: ""Coded Time-Symbolic Simulation : Simulation of Logic Circuits with Nondeterministic Delays Based on Boolean Function Manipulation"" Proceedings of the Synthesis and Simulation Meeting and International Interchange. 149-156 (1990)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Noriyuki Takahashi: ""Fault Simulation for Multiple Faults Using Shared Binary Decision Diagrams"" Proceedings of the Synthesis and Simulation Meeting and International Interchange. 157-164 (1990)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Nagisa Ishiura: ""A Class of Logic Functions Expressible by Polynomial-Size Binary Decision Diagrams"" Proceedings of the Synthesis and Simulation Meeting and International Interchange. 48-54 (1990)

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

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Yutaka Deguchi: ""Probabilistic CTSS : Analysis of Timing Error Probability in Asynchronous Logic Circuits"" Proceedings of 28th ACM/IEEE Design Automation Conference. 650-655 (1991)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Hiromi Hiraishi: ""Vectorized Symbolic Model Checking of Computation Tree Logic"" Proceedings of the Workshop on Computer-Aided Verification. 279-290 (1991)

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

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

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Noriyuki Takahashi: ""Fault Simulation for Multiple Faults Using Shared BDD Representation of Fault Sets"" Proceedings of IEEE International Conference on Computer-Aided Design. 550-553 (1991)

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

URL: 

Published: 1993-03-16  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi