スライド 1

Computer
Computer
Aided
Aided
Design
Design
線形計画法に基づく逐次化を利用した
システムレベル設計での動作並列化
前後での等価性検証手法
松本剛史(1), Thanyapat Sakunkonchak(1),
齋藤寛(2), 小松聡(1), 藤田昌宏(1)
(1) 東京大学, (2) 会津大学
Fujita Lab, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

2
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

3
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
システムレベル設計における等価性検証

Computer
Computer
Aided
Aided
Design
Design
システムレベル設計
仕様からアーキテクチャ決定までの設計を行う
 利点

 柔軟なHW/SW分割
 高速なシミュレーション
 少ない記述量
Cベース設計言語が使われることが多い
 動作の並列化やスケジューリング変更を伴う

 アーキテクチャ変更などの際に

システムレベル設計における等価性検証

動作の等価性を保ったまま変更する場合が多い
 並列化・スケジューリング変更が典型的な例
4
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
本研究の目的

並列化・スケジューリング前後での等価性検証
手法の提案・評価


Computer
Computer
Aided
Aided
Design
Design
記述言語はSpecCを対象とする
研究の特徴

既存のプロパティ検証フレームワークを応用して、並
列動作を逐次化
 依存関係に基づくプロパティ検証により、逐次化可能である
ことを保証する
 検証エンジンとしてILPソルバーを用いる

逐次化された設計間で形式的等価性検証を行う
 記号シミュレーションによる
5
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
SpecC言語における並列・同期
Computer
Computer
Aided
Aided
Design
Design
並列: par 構文で表現
 同期: notify/wait 構文で表現

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); }
}
6
A.main
st1
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
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
関連研究

Computer
Computer
Aided
Aided
Design
Design
FSMDモデル上での検証 [3,4,5]

FSMD中のパスごとに検証  パス数が増加するため、規模が
大きい設計は検証できない
高位合成ツールの情報によって対応付け [5]
 変数名によって対応付け [3]



本研究では、大規模設計における並列化・スケジューリングの
検証を目指す
規則に基づく検証 [2]


事前に定義して等価な変換モデルに該当するかどうかを調べ
る
関数単位での並列化・スケジューリングが対象


7
関数内部の変更は対象としない
本研究では、並列化・スケジューリングに伴う関数内部の変更
も検証できる
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

8
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
ILPソルバーを利用した同期検証 [6]

対象


Computer
Computer
Aided
Aided
Design
Design
並列・同期を含むシステムレベル設計
手法 (概要)
1. 各 statement が実行される時刻が満たす条件式
を設計記述から作成
 2. 検証するプロパティを実行時刻の等式・不等式で
表現

 デッドロックの場合、Twait
< Tnotify
3. プロパティを満たす代入値があるかをILPソルバー
によって求める
 CEGAR (Counter-Example Guided Abstraction
Refinement) を採用しており、1-3 を繰り返す

9
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
同期検証の流れ
behavior A (…) {
void main() {
y = x – 1;
notify e;
if(x==10) z=1;
}
}
Original SpecC
Abstraction
Refinement of
abstraction
Computer
Computer
Aided
Aided
Design
Design
behavior A (…) {
void main() {
…
notify e;
if(c0) …
}
}
Boolean SpecC
(Abstracted)
No
Is the trace feasible?
Yes
Synch.
property
Fail with a trace
Pass
Synch. error is found
10
Extract equalities/inequalities
and solve them by ILP solver
No synch. error
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
記号シミュレーションによる等価性検証 [7]

逐次動作記述に対する等価性検証手法


Computer
Computer
Aided
Aided
Design
Design
本研究では、逐次化された設計記述間での等価性検証に利用
手法 (概要)
設計記述を記号的に実行する
 代入文などから得られる等価関係をEquivalence Class
としてまとめていく
 入力を等価と仮定して記号シミュレーションを行い、出力
が等価であるかどうかを調べる

11
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

12
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
全体の流れ
System-level
Design 1
Computer
Computer
Aided
Aided
Design
Design
System-level
Design 2
Fail
Synchronization check
Pass
Sequentialization
Sync. Error (i.e. deadlock)
Fail
Error
Pass
Sequential
Design 1
Sequential
Design 2
Equivalence checking
13
Result: Eqv. or Ineqv.
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
逐次化可能な場合

逐次化可能な並列動作の条件

条件１: デッドロックがない


既存手法で検証可能
条件２: 任意の実行順序に対して、等価な実行結果が得られる


Computer
Computer
Aided
Aided
Design
Design
SpecC言語では、ある時点で、1つの statement だけが評価・実
行されることになっている
条件２を調べる手法

依存関係のある statement 間で実行順序が常に同じであるか、
を調べる
実行順序が異なっても結果が等価になる場合は、本研究では対
象としない
 依存関係がなければ、並列動作間の実行順序に制約はない

14
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
プロパティの導出 (1)
Computer
Computer
Aided
Aided
Design
Design

依存関係のある statement 間で実行順序が常
に同じであるか？

依存関係のある２つの statement st1, st2 が
P1: T(st1) > T(st2)
⇒「st1 は必ず st2 の後に実行される」
 P2: T(st1) < T(st2)
⇒「st2 は必ず st1 の後に実行される」

15
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
プロパティの導出 (2)

Computer
Computer
Aided
Aided
Design
Design
検証結果による場合分け
P1: T(st1) > T(st2)
 P2: T(st1) < T(st2)

(P1, P2) = (pass, pass)
(P1, P2) = (fail, pass)
(P1, P2) = (pass, fail)
(P1, P2) = (fail, fail)

逐次化
可能
実際の検証はベーシックブロックを単位として
行う

16
起こりえない
必ず st1st2 の順に実行
必ず st2st1 の順に実行
実行順序は一意ではない
ここでは、par/wait/notify/条件分岐を含まない一連
の statement をベーシックブロックとする
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
逐次化の例

Computer
Computer
Aided
Aided
Design
Design
依存関係があり、並列動作するBB
BB1, BB3 … 検証結果: BB1  BB3
 BB2, BB3 … 検証結果: BB3  BB2

BB1
c1 = a1 + b1;
c2 = a2 + b2;
notify e1;
wait e2;
d2 = (c2-c1)/d1;
BB2
17
wait e1; BB3
d1 = c1 * c2;
if(d1 != 0)
notify e2;
else
ERROR();
BB4
逐次化
c1 = a1 + b1;
c2 = a2 + b2;
d1 = c1 * c2;
if(d1 != 0)
d2 = (c2-c1)/d1;
else
ERROR();
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

18
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
例題

IDCT







VocSpec: 仕様。全動作を１つのHWで実現することを想定
VocArch: 動作の一部をDSPに割り当てたもの
VocSched: 各PEでスケジューリングを決定したもの
MP3 Decoder


19
IDCT1: 逐次実行
IDCT2: 行計算・列計算を２並列で実行
IDCT3: 行計算・列計算を８並列で実行
IDCT4: 行計算・列計算内での並列実行を導入
Vocoder


Computer
Computer
Aided
Aided
Design
Design
MP3DEC1: SWと１つの追加HW
MP3DEC2: 負荷の大きいDCT計算に２つの追加モジュールを
割り当てたもの
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
例題規模と実験環境

例題規模

例題は全てSpecC言語で記述
例題
行数
IDCT1
300
0
IDCT2
314
IDCT3
IDCT4

par
同期数
構文数
例題
行数
par
構文数
同期
数
0
VocSpec
9165
10
4
8
0
VocArch
10178
15
14
256
2
0
VocSched
10139
2
14
390
4
10
MP3DEC1
8580
4
6
MP3DEC2
8560
5
10
実験環境



20
Computer
Computer
Aided
Aided
Design
Design
CPU 3.2GHz、メモリ 4GB のPCで実行
依存関係の解析: GrammaTech 社の CodeSurfer を利用
ILPソルバー: ILOG 社の CPLEX を使用
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
実験結果 (逐次化)

Computer
Computer
Aided
Aided
Design
Design
ILPソルバーを用いた逐次化

Vocoder, MP3 ではデッドロックを検出


バグ修正して、実験を続行
ILPベースの検証が不要な場合も多い
依存関係のない部分のみで並列化が行われた場合
 ただし、依存関係がないことは依存グラフ上で調べている


例題
ILP実行時間は非常に短時間
行数行数 ILP 時間
(前) (後) (回数) (sec)
例題
行数
(前)
行数
(後)
ILP 時間
(回数) (sec)
IDCT1 300
300
0
0.7
VocSpec
9165
9165
0
39.0
IDCT2 314
298
0
0.8
VocArch
10178 10164
0
48.5
IDCT3 256
251
0
0.7
VocSched
10139 10132
0
42.0
IDCT4 390
360
48
1.0
MP3DEC1
8580
8580
0
160
MP3DEC2
8560
8560
18
162
21
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
実験結果 (等価性検証)

Computer
Computer
Aided
Aided
Design
Design
記号シミュレーションによる等価性検証
逐次化後に差異のあるビヘイビア(関数)に対してのみ実
行
 いずれも0.1秒以内で等価性を検証できた
 全体を記号シミュレーションにより検証することは現実的
に不可能

逐次化された
変更前設計
逐次化された
変更後設計
差異 (行)
検証時間 (sec)
seq_IDCT1
seq_IDCT2
156
< 0.1
seq_IDCT1
seq_IDCT3
148
< 0.1
seq_IDCT3
seq_IDCT4
224
< 0.1
seq_VocSpec
seq_VocArch
25
< 0.1
seq_VocArch
seq_VocSched
0
-
478
< 0.1
seq_MP3DEC1 seq_MP3DEC2
22
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
発表内容
Computer
Computer
Aided
Aided
Design
Design
研究の背景と目的
 既存検証技術の紹介
 線形計画法ソルバーを利用した逐次化
 実験結果
 まとめと今後の課題

23
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo
まとめと今後の課題

Computer
Computer
Aided
Aided
Design
Design
まとめ
並列化・スケジューリング前後での等価性検証手法
を提案
 ILPベースのプロパティ検証を利用して、逐次化を行
う
 実例題を用いた実験で検証ができることを確認


今後の課題

一意に逐次化できない場合の検証手法
 並列化・スケジューリングの間違いである場合が多いが

高位合成前後における等価性検証への応用
 スケジューリング以外の変更・詳細化に対応する必要
24
Fujita Lab, Department of Electronics Engineering, School of Engineering, University of Tokyo

Download Report