プログラム可能データパスとSMTソルバーを利用した高位設計デバッグ手法

• Item type: SIG Technical Reports(1)
• 公開日: 2014-03-08
• タイトル: プログラム可能データパスとSMTソルバーを利用した高位設計デバッグ手法
• タイトル / 言語: en
• タイトル: Debugging High Level Designs using Programmable Datapaths and SMT Solvers
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 検証技術
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 東京大学工学系研究科電気系工学専攻
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Dept. of Electrical Engineering and Information Systems, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者名: 松本, 剛史; 城, 怜史; 藤田, 昌宏
• 著者名(英): Takeshi, Matsumoto; Satoshi, Jo; Masahiro, Fujita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 近年、Look-up Table(LUT) のようなプログラム可能回路を利用した論理回路の自動デバッグ手法が提案されている。この手法では、回路中に LUT を挿入し、SAT ソルバーを用いて、回路が仕様を満たすような LUT の論理定義を求めることによって論理修正を行う。この考え方は、LUT の代わりに Uninterpreted Function(UIF) を利用することによって、ワード変数とそれらに対する演算が記述される高位設計に適用することができる。この場合、SAT ソルバーの代わりに、ワード変数や算術演算を含む論理式の SAT 問題を効率良く解くことができる SMT ソルバーが使われる。しかし、一般的に、UIF を利用した手法においては、得られた誤り修正の解を限られた種類の利用可能な演算 (器) で実現することは容易ではない。そこで、 UIF ではなく、プログラム可能なデータパスを利用することにより、利用可能な演算によって実装可能な誤り修正を求める手法を提案する。提案するプログラム可能データパスでは、与えられた演算を最大 N 回まで適用する任意のデータパスが表現可能であり (N は指定された数)、その中に仕様を満たす構成が含まれるかを SMT ソルバーで解く。いくつかの例題に対して、仕様を満たすプログラム可能データパスの構成を求める実験を行い、その性能を評価する。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a method to correct high level designs. Recentrly, methods to rectify logic gate circuits utilizing programmable logics based on look-up tables (LUTs) inserted in the circuits for debugging purposes. The idea can be extended to high level (or word level) designs by using uninterpreted functions (UIFs) instead of LUTs. In such methods, some portions of a design under debugging are replaced with UIFs, and their definitions which can correct the design are explored by formulating them as satisfiability problems and solving them by SMT solvers, which are SAT solvers which can efficiently handle word variables and arithmetic operations. However, in general it is not at all easy to implement them with limited types of available arithmetic circuits. Our proposed method utilizes programmable datapaths, instead of UIFs, which realize any combination of applications of specified types of operations at most N times (N is a user-specified integer). Then, a correction of a given design can be obtained as a configuration of programmable datapaths, which can be solved similarly to the conventional methods using UIFs. We have confirmed that high level designs can be corrected through experiments with several example cases.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA12149313
• 書誌情報: 研究報告組込みシステム（EMB）; 巻 2014-EMB-32, 号 18, p. 1-6, 発行日 2014-03-08
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会