定理証明方式に基づく非同期式回路の検証に関する研究

本研究では,定理証明法を用いて,データ長nに依存した回路(パラメタライズ回路)の検証を特定の小さなnの回路(基本回路)の検証に帰着させ,従来の非同期式回路の検証技術を用いて基本回路を検証するというアプローチを取ることを目指した.本研究の現状は以下の通りである.(1)定理証明器としては,米国SRIが試作・無料配布しているPVSというシステムを検討し,簡単な回路の検証等を通し,使用方法・方式等を理解し,本研究に用いることを決定した.(2)当初,定理証明器では『基本回路が,nを含まない使用(基本使用)に対して正しい』ことを表す補助定理を用いて,主にnに関する帰納法により,パラメタライズ回路の動作がパラメタライズ仕様に含まれることを証明しようとした.検証対象とした非同期式回路が,比較的規則的な構造をしている場合は,この方式がうまく働くことがわかったが,データパス部に制御信号が複雑に入り込んだ回路の場合,補助定理がほとんど自明の命題となり,大部分の証明は帰納法による部分で行わなければならないことがわかった.(3)回路によってはこの部分の証明は容易ではないので,データを『コード』,『スペ-サ』,『変化途中の状態』,および『不正なデータ』に抽象化し,時間に対する帰納法を用いることを考案した(抽象化の正しさは別途証明する).同期式回路の場合,共通のクロックが存在するため,それに対する帰納法を用いれば比較的容易に証明を行えるが,非同期式回路の場合,クロックが存在しないため状態遷移を考える必要がある.現在,やや複雑な非同期式回路を例に取り,この手法を試用中である.証明はほぼ可能であるが,まだ,一般の回路に適応できる共通の手法としてまとめ上げるには至っていない.証明手法を解析し,ある程度一般的な証明戦略としてまとめることが今後の課題である.

本研究では,定理証明法を用いて,データ長nに依存した回路(パラメタライズ回路)の検証を特定の小さなnの回路(基本回路)の検証に帰着させ,従来の非同期式回路の検証技術を用いて基本回路を検証するというアプローチを取ることを目指した.本研究の現状は以下の通りである.(1)定理証明器としては,米国SRIが試作・無料配布しているPVSというシステムを検討し,簡単な回路の検証等を通し,使用方法・方式等を理解し,本研究に用いることを決定した.(2)当初,定理証明器では『基本回路が,nを含まない使用(基本使用)に対して正しい』ことを表す補助定理を用いて,主にnに関する帰納法により,パラメタライズ回路の動作がパラメタライズ仕様に含まれることを証明しようとした.検証対象とした非同期式回路が,比較的規則的な構造をしている場合は,この方式がうまく働くことがわかったが,データパス部に制御信号が複雑に入り込んだ回路の場合,補助定理がほとんど自明の命題となり,大部分の証明は帰納法による部分で行わなければならないことがわかった.(3)回路によってはこの部分の証明は容易ではないので,データを『コード』,『スペ-サ』,『変化途中の状態』,および『不正なデータ』に抽象化し,時間に対する帰納法を用いることを考案した(抽象化の正しさは別途証明する).同期式回路の場合,共通のクロックが存在するため,それに対する帰納法を用いれば比較的容易に証明を行えるが,非同期式回路の場合,クロックが存在しないため状態遷移を考える必要がある.現在,やや複雑な非同期式回路を例に取り,この手法を試用中である.証明はほぼ可能であるが,まだ,一般の回路に適応できる共通の手法としてまとめ上げるには至っていない.証明手法を解析し,ある程度一般的な証明戦略としてまとめることが今後の課題である.