Project/Area Number  03555074 
Research Category 
GrantinAid for Developmental Scientific Research (B).

Research Field 
情報工学

Research Institution  KYOTO UNIVERSITY 
Principal Investigator 
YAJIMA Shuzo Kyoto University, Faculty of Engineering, Professor, 工学部, 教授 (20025901)

CoInvestigator(Kenkyūbuntansha) 
HIRAISHI Hiromi Kyoto University, Faculty of Engineering, Professor, 工学部, 教授 (40093299)
OGINO Hiroyuki Kyoto University, Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
TAKENAGA Yasuhiko Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (20236491)
TAKAGI Naofumi Kyoto University, Faculty of Engineering, Assoc. Professor, 工学部, 助教授 (10171422)
HAMAGUCHI Kiyoharu Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (80238055)

Project Fiscal Year 
1991 – 1992

Project Status 
Completed(Fiscal Year 1992)

Budget Amount *help 
¥8,300,000 (Direct Cost : ¥8,300,000)
Fiscal Year 1992 : ¥3,500,000 (Direct Cost : ¥3,500,000)
Fiscal Year 1991 : ¥4,800,000 (Direct Cost : ¥4,800,000)

Keywords  logic synthesis / logic design verification / sequential circuits / logic function optimization / state assignment / temporal logic / computeraided logic design / 論理合成 / 論理設計検証 / 順序回路 / 論理関数簡単化 / 状態割当て / 時相論理 / 論理設計支援 
Research Abstract 
We carried out Research on development of logic synthesizer and design verifier for sequential circuits based on Boolean function manipulation as follows: 1. Logic synthesizer for sequential circuits based on Boolean function manipulation For oneshot state assignment and single transition time assignment for asynchronous sequential circuits, we have proposed and implemented algorithms of finding minimum solutions based on Boolean function manipulation. 2. Design verifier for sequential circuits based on Boolean function manipulation We have proposed a design verification algorithm based on Boolean function manipulation, which assumes, as a specification language, branching time regular temporal logic (BRTL), which has higher expressive power as compared with the conventional temporal logics. We have developed a design verifier based on the algorithm and succeeded in design verification of microprocessors. 3. Efficient Boolean function manipulation We have clarified the theoretical properties of shared binary decision diagram (SBDD) to manipulate Boolean functions. We also have proposed and implemented an algorithm of finding input variable ordering such that the diagram becomes small and an algorithm to deal with SBDD of large size on secondary storage efficiently. 4. Graphic interface of logic synthesizer and design verifier We have implemented a multicomputer multiscreen system by using the X window system on workstations and achieved high resolution and highspeed drawing.
