ハードウェアの機能レベル設計に対する形式的検証手法に関する研究

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10780189
• Research Institution: Osaka University
• Principal Investigator: 濱口 清治 大阪大学, 基礎工学研究科, 講師 (80238055)
• Keywords: 形式的設計検証 / 機能レベル検証 / 第一階述語論理 / 順序機械 / 時相論理

Research Abstract

本研究では,論理レベルよりも高位の記述,特に機能レベルの設計記述に対する形式的検証の自動化手法について研究を行っている.機能レベルの設計記述としては,算術演算回路などを抽象的に記述するため,第一階述語論理の部分クラスの利用を検討している.この部分クラスでは,恒真性判定が決定可能となることから,人手による介入のない自動検証可能な部分を拡大できると期待される.
本年度は,まず第一階述語論理の部分クラスを遷移関数の記述に用いることができるよう拡張した順序機械について基本的な性質について解析し,その記述手法および等価性判定手法の開発を行った.さらに,部分仕様の記述手法として,第一階述語論理の部分クラスに時相演算子を加えた論理体系を示して,検証の基礎となる恒真性判定が決定可能であることを示した.従来,第一階述語論理の部分クラスによる記述を許す場合には,時間展開などを利用することにより,基本的には組合せ回路に対する検証手法に帰着する方法が用いられていたが,本研究により順序機械の形式的設計検証に対して,第一階述語論理の部分クラスの適用が可能になるものと考える.さらにまた,機能レベル設計の検証において重要となるデータパスの論理設計の検証手法に関連して,算術演算を表現するための二分モーメントグラフのサイズの理論的解析を行った.本年度は,設計検証のための基礎的理論を重視し,主として理論面について研究を行ったが,11年度には,順次プログラムとして実装し,実験を行っていく予定である.

Research Products

• [Publications] M.Nakanishi: "An Exponential Lower Bound on the Size of Binary Mamont Diagram Representing Integer Division" IEICE Trans.on Fundamentals of Electronics,Communications,and Computer Sciences.発売予定. (1999)
• [Publications] K.Hamaguchi: "A partially Explicit Method for Efficient Symbolic Checking of Language Containment" Synthesis and Simulation Meeting and International Interchange. 109-114 (1998)