時相論理に基づく計算機援用形式的設計検証に関する研究

1992 年度 実績報告書

• 研究課題/領域番号: 03650301
• 研究機関: 京都産業大学
• 研究代表者: 平石 裕実 京都産業大学, 工学部, 教授 (40093299)
• 研究分担者: 石浦 菜岐佐 大阪大学, 工学部, 講師 (60193265)
• キーワード: 論理設計検証 / 形式的検証 / 時相論理 / 計算機援用設計

研究概要

本年度は、昨年度得られたBRTLの記号モデル検査アルゴリズムをプログラム化し、実際に8ビットマイクロプロセッサの設計検証に適用して、アルゴリズムの評価改良を行うとともに、より高レベルの設計検証としてマルチマイクロプロセッサ用の階層的バス(Futureバス)のキャッシュコヒレンシープロトコルの設計検証を行い、以下の成果を得た。
1.形式的設計検証アルゴリズムの評価と改良: BRTLを用いた設計検証システムを試作し、8ビットマイクロプロセッサ(KUEチップ)の設計検証を行い、実際の設計の誤りを発見するとともに、それ以外の部分については設計が正しいことを示すことが出来た。さらに、より効率の良い検証アルゴリズムを提案し、全体の検証時間を約1/8に出来ることを示した。
2.設計誤りの解析手法の研究: 記号モデル検査法により設計が正しくないことを発見した場合、設計が仕様を満たさない場合の動作系列を示すアルゴリズムを示し、これが、KUEチップの設計誤りの発見に有効であることを示した。
3.階層的仕様記述と抽象化の研究: KUEチップの検証においては、チップ内部のメモリを切放し、メモリに対する入出力命令のレベルでメモリを扱う手法を用いその有効性を示した。また、Futureバスのキャッシュコヒレンシーの設計検証では、共有メモリと各プロセッサのキャッシュメモリを1ビットで抽象化して検証する手法を示し、その有効性を明らかにした。

研究成果

• [文献書誌] K.Hamaguchi: "Formal Design Verification of Sequontial Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic" IEICE Trams.Fundamentals of Electronics,Communicntions and Computer Sciences. E75-A. 1220-1229 (1992)
• [文献書誌] K.Hamaguchi: "∞ Regular Temporal Logic and Its Model Checking Problem" Theoretical Computer Science. 103. 191-204 (1992)
• [文献書誌] K.Hamaguchi: "Design Verification of Asynchrovous Sequential Circuits Using Sympolic Model Checking" Proc.International Symposium on Logic Synthesis and Microprocessor Architecture. 84-90 (1992)
• [文献書誌] K.Hamaguchi: "Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic" Proc. 4th Workshop on Compnter-Aided Verification. 201-212 (1992)
• [文献書誌] K.Hamaguchi: "Formal Verification of Sequential Circuits Based on Symbolic Model Checking for Branching Time Rogular Temporal Logec" Proc.Synthesis and Simulation Meeling and International Intercharge. 243-252 (1992)
• [文献書誌] K.Kawakubo: "Formal Verification of Fail-safeness of a Comparator for Rodundant System Using Rogular Temporal Logic" Proc.1st Asian Test Symposium. 2-7 (1992)