1994 Fiscal Year Annual Research Report

時相論理に基づく論理設計の型式的検証システムの試作研究

Research Project

Project/Area Number	05558030
Research Institution	KYOTO UNIVERSITY
Principal Investigator	矢島脩三京都大学, 工学部, 教授 (20025901)
Co-Investigator(Kenkyū-buntansha)	平石裕実京都産業大学, 工学部, 教授 (40093299) 荻野博幸京都大学, 工学部, 教務職員 (40144323) 武永康彦京都大学, 工学部, 助手 (20236491) 浜口清治京都大学, 工学部, 講師 (80238055)
Keywords	時相論理 / 論理設計 / 形式的検証 / 論理開数処理 / 二分決定グラフ / モデルチェッキング / 仕様記述
Research Abstract	交付申請書に記載の通り、平成5年度に引続き、次の研究を行った。 (1)論理設計の型式的検証システムの試作 (a)仕様記述能力の改善:従来形式的検証に用いられてきた分岐時間モデルに基づく時相論理に比べ表現能力が高く、また直観的な記述が可能な線形時間時相論理を取り上げ、論理関数処理に基づく検証アルゴリズムの開発・実装を行い、実例を検証し、その有効性を示した。(b)対象の抽象化:大規模回路中の部分回路を抽象化するためには、部分回路ごとの検証がまず必要となるが、マイクロプロセッサなどでは、従来法を適用すると、ビット数に対して指数時間の検証時間を要する乗算器などが部分回路として含まれているため、問題となっていた。本研究では、二分モーメントグラフと呼ばれるデータ構造を用いることで、多項式時間での検証が可能であることを実験的に示すことに成功した。また、配列構造に着目した抽象化手法を開発しており、今後これらを融合していくことが課題となっている。 (2)論理関数処理の高速化に関する研究 (a)二分決定グラフの種々の拡張:従来、論理関数処理に用いられて来た二分決定グラフの拡張とみなすことのできる、V節点を含む二分決定グラフや分岐プログラムの種々のクラスについてその表現能力を明らかにした。(b)大規模な二分決定グラフの処理技法:二次記憶を用いて大規模な二分決定グラフを処理する手法を開発し、実装・実験を行ってその有効性を示した。 (3)システムのユーザインターフェースに関する研究従来から開発してきたマルチスクリーン・マルチコンピュータシステムにXウィンドウ上での描画機能を実装し、二分決定グラフや論理回路図の描画を可能とした。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] Shuzo YAJIMA: "Breadth-First Manipulation of Very Large Binary Decision Diagraws" Rroc.of 1993 IEEEIACM Int.Canf.on Computer Aicled Design. 48-55 (1993)
[Publications] Kiyoharu HAMAGUCHI: "The Complexity of the Optimol Varicble Ordering Problems of Shared Binary Desision Dlagrams" Proc.of 4th Jnt.Symp on Algorithms and Camputation. 389-398 (1993)
[Publications] Kiyoharu HAMAGUCHI: "Another Look at LTL Model Checking" Proc of Cont.on Computer-Aided Veritication,Lecture Notes. 818. 415-427 (1994)
[Publications] YasuhikoTAKENAGA: "Computational Complexity of Manipulationg Binary Decision Oiagrams" IEICE Trans.Information e Systems. E77-D. 642-647 (1994)
[Publications] Yasuhiko TAKENAGA: "On the Size of Ordered Binary Decision Diagrams Pepresention Threshold Functions" Proc.of 5th Int.Syinp.on Algorithms and Computation. 584-592 (1994)
[Publications] Hiromi HIRAISHI: "Time-Space Modal Model Checking toward Verification of Bit-Slice Architecture" Proc.of 3rd Asian Test Symposium. 287-291 (1994)

1994 Fiscal Year Annual Research Report

時相論理に基づく論理設計の型式的検証システムの試作研究

Principal Investigator

矢島 脩三 京都大学, 工学部, 教授 (20025901)

Research Products

[Publications] Shuzo YAJIMA: "Breadth-First Manipulation of Very Large Binary Decision Diagraws" Rroc.of 1993 IEEEIACM Int.Canf.on Computer Aicled Design. 48-55 (1993)

[Publications] Kiyoharu HAMAGUCHI: "The Complexity of the Optimol Varicble Ordering Problems of Shared Binary Desision Dlagrams" Proc.of 4th Jnt.Symp on Algorithms and Camputation. 389-398 (1993)

[Publications] Kiyoharu HAMAGUCHI: "Another Look at LTL Model Checking" Proc of Cont.on Computer-Aided Veritication,Lecture Notes. 818. 415-427 (1994)

[Publications] YasuhikoTAKENAGA: "Computational Complexity of Manipulationg Binary Decision Oiagrams" IEICE Trans.Information e Systems. E77-D. 642-647 (1994)

[Publications] Yasuhiko TAKENAGA: "On the Size of Ordered Binary Decision Diagrams Pepresention Threshold Functions" Proc.of 5th Int.Syinp.on Algorithms and Computation. 584-592 (1994)

[Publications] Hiromi HIRAISHI: "Time-Space Modal Model Checking toward Verification of Bit-Slice Architecture" Proc.of 3rd Asian Test Symposium. 287-291 (1994)

矢島脩三京都大学, 工学部, 教授 (20025901)