充足可能性判定を利用した最適コード生成手法

• Item type: Journal(1)
• 公開日: 2003-05-15
• タイトル: 充足可能性判定を利用した最適コード生成手法
• タイトル / 言語: en
• タイトル: Optimal Code Generation Based on Boolean Satisfiability
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 特集：システムLSIの設計技術と設計自動化
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: テクニカルノート ハードウェア/ソフトウェア協調設計
• 著者所属: 東京大学工学部電子工学科
• 著者所属: 東京大学工学部電子工学科
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): Department of Electronics Engineering, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Electronics Engineering, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): VDEC, The University of Tokyo
• 著者名: 瀬戸, 謙修; 藤田, 昌宏; 浅田, 邦博
• 著者名(英): Kenshu, Seto; Masahiro, Fujita; Kunihiro, Asada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 充足可能性判定（SAT）を利用した最適なコード生成手法を提案する．まずコード生成問題を有限状態機械（FSM）を利用して定式化する（瀬戸ほか，2002）．次にFSMを組合せ回路へと展開し（Biereほか，1999），最適コード生成問題を充足可能性判定（SAT）問題として解く．最新のSATソルバ（Moskewiczほか，2001）を使用した実験結果から，SATベースのコード生成手法がBDDベースのコード生成（瀬戸ほか，2002）よりも効果的であることが示される．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We present a method for optimal code generationbased on Boolean satisfiability (SAT).First, code generation is formulated based on a finite statemachine (FSM) (Seto, et al., 2002). Next, we unroll the FSM to a combinational circuit (Biere, et al., 1999),so that optimal code generation problem is solved as a SAT problem.Experimental results using a state-of-the-art SATsolver (Moskewicz, et al., 2001) demonstrate that SAT-based optimalcode generation is more effective than BDD-based symbolic approach (Seto, et al., 2002).
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 44, 号 5, p. 1202-1205, 発行日 2003-05-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764