2026-03-09T15:52:07Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00011221 2025-01-23T02:20:33Z 581:651:659

テクニカルノート ハードウェア/ソフトウェア協調設計 充足可能性判定を利用した最適コード生成手法 Optimal Code Generation Based on Boolean Satisfiability 瀬戸, 謙修 藤田, 昌宏 浅田, 邦博 Kenshu, Seto Masahiro, Fujita Kunihiro, Asada 特集：システムLSIの設計技術と設計自動化 充足可能性判定（SAT）を利用した最適なコード生成手法を提案する．まずコード生成問題を有限状態機械（FSM）を利用して定式化する（瀬戸ほか，2002）．次にFSMを組合せ回路へと展開し（Biereほか，1999），最適コード生成問題を充足可能性判定（SAT）問題として解く．最新のSATソルバ（Moskewiczほか，2001）を使用した実験結果から，SATベースのコード生成手法がBDDベースのコード生成（瀬戸ほか，2002）よりも効果的であることが示される． 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). journal article 2003-05-15 application/pdf 情報処理学会論文誌 5 44 1202 1205 1882-7764 AN00116647 https://ipsj.ixsq.nii.ac.jp/record/11221/files/IPSJ-JNL4405003.pdf jpn