線形計画法に基づく逐次化を利用したシステムレベル設計での動作並列化前後での等価性検証手法 松本 剛史(1), Thanyapat Sakunkonchak(1), 齋藤 寛(2), 小松 聡(1), 藤田 昌宏(1) (1) 東京大学, (2) 会津大学

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

システムレベル設計における等価性検証 システムレベル設計 システムレベル設計における等価性検証 仕様からアーキテクチャ決定までの設計を行う 利点 柔軟なHW/SW分割 高速なシミュレーション 少ない記述量 Cベース設計言語が使われることが多い 動作の並列化やスケジューリング変更を伴う アーキテクチャ変更などの際に システムレベル設計における等価性検証 動作の等価性を保ったまま変更する場合が多い 並列化・スケジューリング変更が典型的な例

本研究の目的 並列化・スケジューリング前後での等価性検証手法の提案・評価 研究の特徴 記述言語はSpecCを対象とする 既存のプロパティ検証フレームワークを応用して、並列動作を逐次化 依存関係に基づくプロパティ検証により、逐次化可能であることを保証する 検証エンジンとしてILPソルバーを用いる 逐次化された設計間で形式的等価性検証を行う 記号シミュレーションによる

SpecC言語における並列・同期 並列: par 構文で表現 同期: notify/wait 構文で表現 A.main st1 main() { x = 0; //st0 par { A.main(); B.main(); } } behavior A { main() { wait(e); a = x + 10; //st1 } } behavior B { main() { x = 20; //st2 notify(e); } } st0 B.main st2 Time st2 is always executed followed by st1 Tstart_A = Tstart_B, Tend_A = Tend_B (parより) Tstart_A <= Twait <= Tstart_st1 < Tend_st1 <= Tend_A Tstart_B <= Tstart_st2 < Tend_st2 <= Tnotify <= Tend_B Tnotify < Twait

関連研究 FSMDモデル上での検証 [3,4,5] 規則に基づく検証 [2] 高位合成ツールの情報によって対応付け [5] 変数名によって対応付け [3] 本研究では、大規模設計における並列化・スケジューリングの検証を目指す 規則に基づく検証 [2] 事前に定義して等価な変換モデルに該当するかどうかを調べる 関数単位での並列化・スケジューリングが対象 関数内部の変更は対象としない 本研究では、並列化・スケジューリングに伴う関数内部の変更も検証できる

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

ILPソルバーを利用した同期検証 [6] 対象 手法 (概要) 並列・同期を含むシステムレベル設計 1. 各 statement が実行される時刻が満たす条件式を設計記述から作成 2. 検証するプロパティを実行時刻の等式・不等式で表現 デッドロックの場合、Twait < Tnotify 3. プロパティを満たす代入値があるかをILPソルバーによって求める CEGAR (Counter-Example Guided Abstraction Refinement) を採用しており、1-3 を繰り返す

同期検証の流れ Synch. property Abstraction Refinement of abstraction behavior A (…) { void main() { y = x – 1; notify e; if(x==10) z=1; } } behavior A (…) { void main() { … notify e; if(c0) … } } Abstraction Original SpecC Boolean SpecC (Abstracted) Refinement of abstraction No Extract equalities/inequalities and solve them by ILP solver Synch. property Is the trace feasible? Fail with a trace Yes Pass Synch. error is found No synch. error

記号シミュレーションによる等価性検証 [7] 逐次動作記述に対する等価性検証手法 本研究では、逐次化された設計記述間での等価性検証に利用 手法 (概要) 設計記述を記号的に実行する 代入文などから得られる等価関係をEquivalence Class としてまとめていく 入力を等価と仮定して記号シミュレーションを行い、出力が等価であるかどうかを調べる

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

全体の流れ System-level Design 1 System-level Design 2 Fail Synchronization check Sync. Error (i.e. deadlock) Pass Fail Sequentialization Error Pass Sequential Design 1 Sequential Design 2 Equivalence checking Result: Eqv. or Ineqv.

逐次化可能な場合 逐次化可能な並列動作の条件 条件２を調べる手法 条件１: デッドロックがない 既存手法で検証可能 条件２: 任意の実行順序に対して、等価な実行結果が得られる SpecC言語では、ある時点で、1つの statement だけが評価・実行されることになっている 条件２を調べる手法 依存関係のある statement 間で実行順序が常に同じであるか、を調べる 実行順序が異なっても結果が等価になる場合は、本研究では対象としない 依存関係がなければ、並列動作間の実行順序に制約はない

プロパティの導出 (1) 依存関係のある statement 間で実行順序が常に同じであるか？ 依存関係のある２つの statement st1, st2 が P1: T(st1) > T(st2) ⇒「st1 は必ず st2 の後に実行される」 P2: T(st1) < T(st2) ⇒「st2 は必ず st1 の後に実行される」

プロパティの導出 (2) 検証結果による場合分け 実際の検証はベーシックブロックを単位として行う P1: T(st1) > T(st2) P2: T(st1) < T(st2) 実際の検証はベーシックブロックを単位として行う ここでは、par/wait/notify/条件分岐 を含まない一連の statement をベーシックブロックとする (P1, P2) = (pass, pass) 起こりえない (P1, P2) = (fail, pass) 必ず st1st2 の順に実行 (P1, P2) = (pass, fail) 必ず st2st1 の順に実行 (P1, P2) = (fail, fail) 実行順序は一意ではない 逐次化 可能

逐次化の例 依存関係があり、並列動作するBB BB1, BB3 … 検証結果: BB1  BB3 c1 = a1 + b1; c2 = a2 + b2; d1 = c1 * c2; if(d1 != 0) d2 = (c2-c1)/d1; else ERROR(); BB1 c1 = a1 + b1; c2 = a2 + b2; notify e1; wait e2; d2 = (c2-c1)/d1; wait e1; d1 = c1 * c2; if(d1 != 0) notify e2; else ERROR(); BB3 逐次化 BB2 BB4

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

例題 IDCT Vocoder MP3 Decoder IDCT1: 逐次実行 IDCT2: 行計算・列計算を２並列で実行 VocSpec: 仕様。全動作を１つのHWで実現することを想定 VocArch: 動作の一部をDSPに割り当てたもの VocSched: 各PEでスケジューリングを決定したもの MP3 Decoder MP3DEC1: SWと１つの追加HW MP3DEC2: 負荷の大きいDCT計算に２つの追加モジュールを割り当てたもの

例題規模と実験環境 例題規模 実験環境 例題は全てSpecC言語で記述 CPU 3.2GHz、メモリ 4GB のPCで実行 依存関係の解析: GrammaTech 社の CodeSurfer を利用 ILPソルバー: ILOG 社の CPLEX を使用 例題 行数 par 構文数 同期数 IDCT1 300 IDCT2 314 8 IDCT3 256 2 IDCT4 390 4 10 例題 行数 par 構文数 同期数 VocSpec 9165 10 4 VocArch 10178 15 14 VocSched 10139 2 MP3DEC1 8580 6 MP3DEC2 8560 5

実験結果 (逐次化) ILPソルバーを用いた逐次化 Vocoder, MP3 ではデッドロックを検出 ILPベースの検証が不要な場合も多い バグ修正して、実験を続行 ILPベースの検証が不要な場合も多い 依存関係のない部分のみで並列化が行われた場合 ただし、依存関係がないことは依存グラフ上で調べている ILP実行時間は非常に短時間 例題 行数 (前) 行数 (後) ILP (回数) 時間 (sec) IDCT1 300 0.7 IDCT2 314 298 0.8 IDCT3 256 251 IDCT4 390 360 48 1.0 例題 行数 (前) 行数 (後) ILP (回数) 時間 (sec) VocSpec 9165 39.0 VocArch 10178 10164 48.5 VocSched 10139 10132 42.0 MP3DEC1 8580 160 MP3DEC2 8560 18 162

実験結果 (等価性検証) 記号シミュレーションによる等価性検証 逐次化後に差異のあるビヘイビア(関数)に対してのみ実行 いずれも0.1秒以内で等価性を検証できた 全体を記号シミュレーションにより検証することは現実的に不可能 逐次化された 変更前設計 逐次化された 変更後設計 差異 (行) 検証時間 (sec) seq_IDCT1 seq_IDCT2 156 < 0.1 seq_IDCT3 148 seq_IDCT4 224 seq_VocSpec seq_VocArch 25 seq_VocSched - seq_MP3DEC1 seq_MP3DEC2 478

発表内容 研究の背景と目的 既存検証技術の紹介 線形計画法ソルバーを利用した逐次化 実験結果 まとめと今後の課題

まとめと今後の課題 まとめ 今後の課題 並列化・スケジューリング前後での等価性検証手法を提案 ILPベースのプロパティ検証を利用して、逐次化を行う 実例題を用いた実験で検証ができることを確認 今後の課題 一意に逐次化できない場合の検証手法 並列化・スケジューリングの間違いである場合が多いが 高位合成前後における等価性検証への応用 スケジューリング以外の変更・詳細化に対応する必要