等式論理による機能レベル設計の形式的検証に関する研究

集積回路技術の発達にともなって、より大規模の回路設計が行われるようになってきており、このため、設計の正しさを保証することが困難となってきている。設計検証のための技術としては、シミュレーションが広く利用されてきているが、より網羅的かつ厳密な手法として、設計工程のいくつかの場面では、形式的検証技術の利用が進んでいる。現在、実用が進んでいる形式的設計検証の技術は論理回路設計を扱っているが、より大規模な回路を扱うためには、より抽象度の高い、機能レベルの記述を直接扱う必要性がある。本研究では、算術演算などを論理回路レベルで扱わず、記号のまま直接取り扱うために、等号付第一階述語論理を取り上げて、論理回路より上位の機能レベルで記述された設計に対する設計検証手法について研究を行った。機能レベル設計の設計検証問題は、この論理体系における恒真性判定問題に帰着することができるが、一般の等号付第一階述語論理を設計検証に用いた場合、恒真性判定問題が決定不能となるため、検証工程を自動化することができない。しかし、限量子を含まない論理式のみを考えた場合には決定可能となる。具体的に、本研究では、二分決定グラフによる論理関数処理を用いた恒真性判定アルゴリズムを考案したほか、限量子のない等号付第一階述語論理に、時間に関する性質を表現するための時相演算子を加えた論理体系をとりあげ、まず、恒真性判定問題の決定可能性を証明し、次に、これに基づいて効率的な恒真性判定アルゴリズムを構築・実装して、機能レベル設計の検証に有効であることを示した。

集積回路技術の発達にともなって、より大規模の回路設計が行われるようになってきており、このため、設計の正しさを保証することが困難となってきている。設計検証のための技術としては、シミュレーションが広く利用されてきているが、より網羅的かつ厳密な手法として、設計工程のいくつかの場面では、形式的検証技術の利用が進んでいる。現在、実用が進んでいる形式的設計検証の技術は論理回路設計を扱っているが、より大規模な回路を扱うためには、より抽象度の高い、機能レベルの記述を直接扱う必要性がある。本研究では、算術演算などを論理回路レベルで扱わず、記号のまま直接取り扱うために、等号付第一階述語論理を取り上げて、論理回路より上位の機能レベルで記述された設計に対する設計検証手法について研究を行った。機能レベル設計の設計検証問題は、この論理体系における恒真性判定問題に帰着することができるが、一般の等号付第一階述語論理を設計検証に用いた場合、恒真性判定問題が決定不能となるため、検証工程を自動化することができない。しかし、限量子を含まない論理式のみを考えた場合には決定可能となる。具体的に、本研究では、二分決定グラフによる論理関数処理を用いた恒真性判定アルゴリズムを考案したほか、限量子のない等号付第一階述語論理に、時間に関する性質を表現するための時相演算子を加えた論理体系をとりあげ、まず、恒真性判定問題の決定可能性を証明し、次に、これに基づいて効率的な恒真性判定アルゴリズムを構築・実装して、機能レベル設計の検証に有効であることを示した。