著者

原田 裕基 松本 剛史 藤田 昌宏

雑誌

研究報告システムLSI設計技術(SLDM)

巻号頁・発行日

vol.2011-SLDM-150, no.12, pp.1-6, 2011-05-11

---

高位設計記述において、シミュレーションや形式的手法によって機能仕様に反する実行例(反例)が発見された場合、その反例や機能仕様を参照しながら、設計記述をデバッグする必要がある。本稿では、このように反例に基づくデバッグ作業を支援する手法を提案する。具体的には、与えられた反例および正しい実行例から、全てのテストパタンを正しく実行するための設計記述修正の候補を形式的に求める。これにより、設計者は、修正すべき箇所と修正方法の候補を得ることができ、より効率的にデバッグ作業を行えることが期待できる。提案手法では、反例入力パタンによって正しい実行結果を得るためには、どの変数値を実行値とは異なる値に置換すれば良いか、を SMT ソルバーを用いて解いている。加えて、効率的に修正候補を求めるために、設計を分割し、部分的にこれを適用する手法を提案する。実験により、提案手法によって、設計中の設計誤りを正す修正を求めることがでることを示す。