@techreport{oai:ipsj.ixsq.nii.ac.jp:00073983,
 author = {原田, 裕基 and 松本, 剛史 and 藤田, 昌宏 and Hiroki, Harada and Takeshi, Matsumoto and Masahiro, Fujita},
 issue = {12},
 month = {May},
 note = {高位設計記述において、シミュレーションや形式的手法によって機能仕様に反する実行例(反例)が発見された場合、その反例や機能仕様を参照しながら、設計記述をデバッグする必要がある。本稿では、このように反例に基づくデバッグ作業を支援する手法を提案する。具体的には、与えられた反例および正しい実行例から、全てのテストパタンを正しく実行するための設計記述修正の候補を形式的に求める。これにより、設計者は、修正すべき箇所と修正方法の候補を得ることができ、より効率的にデバッグ作業を行えることが期待できる。提案手法では、反例入力パタンによって正しい実行結果を得るためには、どの変数値を実行値とは異なる値に置換すれば良いか、を SMT ソルバーを用いて解いている。加えて、効率的に修正候補を求めるために、設計を分割し、部分的にこれを適用する手法を提案する。実験により、提案手法によって、設計中の設計誤りを正す修正を求めることがでることを示す。, When one or more counterexamples are found by either simulation or formal methods in high-level design verification, we need to modify the given design descriptions by seeing the counterexamples and functional specification. In this paper, we propose a method to find design correction candidates to make the design under debugging behave correctly for all input patterns of counterexamples. With those correction candidates, efficiency of debugging will be improved. The proposed method solves which variable values should be replaced by other values from the originally assigned during the execution in order to make the output values correct for all given counterexamples. Also, to improve the efficiency of the method, we propose to divide a design into smaller portions and apply the method locally. Through the experiments, we show that the proposed method can derive the design correction that makes an erroneous design correct.},
 title = {反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法},
 year = {2011}
}