WEKO3
-
RootNode
アイテム
反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法
https://ipsj.ixsq.nii.ac.jp/records/73983
https://ipsj.ixsq.nii.ac.jp/records/73983b58f42aa-f5f8-4241-b5eb-7461acff655d
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SLDM11150012.pdf (260.8 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-05-11 | |||||||
| タイトル | ||||||||
| タイトル | 反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Efficient High-Level Design Correction Support Based on Counterexamples and Design Division | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 検証技術 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 東京大学大学院工学系研究科電気系工学専攻 | ||||||||
| 著者所属 | ||||||||
| 東京大学大規模集積システム設計教育研究センター | ||||||||
| 著者所属 | ||||||||
| 東京大学大規模集積システム設計教育研究センター／科学技術振興機構戦略的創造研究推進事業CREST | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Electrical Engineering and Information Systems, The University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| VLSI Design and Education Center, The University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| VLSI Design and Education Center, The University of Tokyo / CREST, Japan Science and Technology Agency | ||||||||
| 著者名 |
原田, 裕基
松本, 剛史
藤田, 昌宏
× 原田, 裕基 松本, 剛史 藤田, 昌宏
|
|||||||
| 著者名(英) |
Hiroki, Harada
Takeshi, Matsumoto
Masahiro, Fujita
× Hiroki, Harada Takeshi, Matsumoto Masahiro, Fujita
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 高位設計記述において、シミュレーションや形式的手法によって機能仕様に反する実行例(反例)が発見された場合、その反例や機能仕様を参照しながら、設計記述をデバッグする必要がある。本稿では、このように反例に基づくデバッグ作業を支援する手法を提案する。具体的には、与えられた反例および正しい実行例から、全てのテストパタンを正しく実行するための設計記述修正の候補を形式的に求める。これにより、設計者は、修正すべき箇所と修正方法の候補を得ることができ、より効率的にデバッグ作業を行えることが期待できる。提案手法では、反例入力パタンによって正しい実行結果を得るためには、どの変数値を実行値とは異なる値に置換すれば良いか、を SMT ソルバーを用いて解いている。加えて、効率的に修正候補を求めるために、設計を分割し、部分的にこれを適用する手法を提案する。実験により、提案手法によって、設計中の設計誤りを正す修正を求めることがでることを示す。 | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11451459 | |||||||
| 書誌情報 |
研究報告システムLSI設計技術（SLDM） 巻 2011-SLDM-150, 号 12, p. 1-6, 発行日 2011-05-11 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
