********************************************************************** DAS/SWEST共同基調講演テーマ：C言語ベース設計に対する高位設計検証技術講師：藤田昌宏先生（東京大学大規模集積システム設計教育センター）座長：小野寺先生（京都大学）日時：2007/8/27 15:00～16:20 参加人数：開始時約100 人，　終了時約100 人 ********************************************************************** ■ 発表の概要 ○slide 1：タイトルスライド「C言語ベース設計に対する高位設計検証技術」ということで， DAシンポジウムでの基調講演だと思っていたのですが， SSWESTと共同ということで，一部ソフトウェアのことも含めて話そうと思います．主なことはC言語ベースでハードウェア設計をする場面において検証する話です．（ソフトウェアとしての）C言語の検証ではありません． ○slide 2：目次ハードウェア設計の流れについて説明して，形式的件検証技術がどれくらいできるか，どういうところに集中して研究しているか，復習．モデルチェッキング，等価性検証の２つについて話します． ○slide 3：設計の各段階において利用される変数・関数本発表の内容は形式検証．シミュレーションは用いない．数学的に証明する．まずハードウェアの数学的表現について復習します． AND，NANDなどは2値（boolean）関数．それに対しハードウェア設計では，現状，（今の過半数）レジスタ転送レベル（RTL）設計では，同期回路で，クロックサイクルごとの動作を有限状態機械で書く．状態遷移をあらわすところから制御信号が，演算器やマルチプレクサなどに入って, 計算をする．制御部はboolenan関数だが，掛け算器は，16bit掛ける16bitとかは，ワード数を一括して変数で表す．これをワード変数という．ワード変数はa0, a1, ... とbooleanに展開してできるが，時間がかかる．高位レベルすなわちシステムレベルでは，while文とかを使う．ただしハードウェアを書くので，ハードウェアに不向きな記述はしない．複雑なことはしない再帰的アルゴリズムは無理で，非再帰的なループに変換する if文などの条件式はboolean，ワード変数，等価かどうかを調べるのはboolenan． ○slide 4: 上位レベル設計の流れ現在，日本も含めて，SoC作っているフローは，上から・Conception ・Functional Decomposition C言語で機能的にシミュレーションを作る）C,C＋＋で書いて，実現できるかどうかを確かめる（システムレベル設計）なぜシステムレベル設計と呼ぶか？：どこをHW/SWは決定されていない．少なくともC言語上で明示しない．・Architectural Exploration: どこをHW/SWを決める，どこで既設計のものを再利用するか，を試行錯誤するところ・SW/HW分割：SWは好きに作ってください（HW屋さんはおもってる）・機能としては十分，HWの1ブロックならできるが，複数ブロックに分けてどう通信するか,は考えられていない場合がある．・Structural Decomposiion: TLMなど．個々のタスクは計算をしている，それらが通信している,というふうに分割・HW2: 動作合成（HLS）ツールを用いて，CからRTLに落ちる自動化ツールを使う．さらに性能が気に入らないなら手変換でチューニング． C言語ベース設計とよぶのは，このフローのほぼすべて（例外は，最後のRTLのみ） ○slide 5-8: 段階的詳細化 A，B，Cをやって終了という逐次処理を，少し詳細化するとa1,b1,c1，．．となり，さらに解析すると，a1,a2,は並列化できそうだとわかったりする．個々のタスクは並列実行するけど，タスク間には依存関係があるからnotifyやwaitという構文を用いて依存関係を示す．そこからさらに詳細化することもある．それらの詳細化のそれぞれにおいて，等価性検証を行う必要がある． ○slide 9: 設計詳細化のための各種変換１．アルゴリズムの変更たいていはイメージが決まっている２．当初は数学の式．値の範囲は連続値（無限大とか）．これを浮動小数点演算に変換する（これも精度解析などが必要），場合によっては固定小数点にする．などの最適化がある．等価ではないが，誤差の範囲内かどうかを確認する３．コンパイラがやるような，定数伝播，共通式削除などデータフロー最適化，ループ展開とか４．高位合成スケジューリング（いつどのサイクルで実行するか），アロケーション，バインディング（どの掛け算器を使うか？）自動ツールがある５・ハードウェア化の場合，処理のパイプライン化（ループ融合なども）６．メモリシステムの設計（階層化，キャッシュ） ○slide 10: 数式の簡単化，データフローグラフ変換掛け算器の数を減らすために掛け算数を減らすなど（共通項のくくりだし） ○slide 11: スカラー倍 4x + 5y + 6，affine変換などの処理．スカラー積は「シフト＋足し算」化する（ただし有限ビット幅では，オーバフローの扱いの管理が必要）． ○slide 12: 各種変換（実行順も変化することも）リタイミング, パイプライニング, スケジューリング，演算器の共有 ○slide 13-14: パイプライン化のためのループ融合もともとのC言語記述では，ループはばらばらに（細かく分かれて）書かれていることがある．一般に,個々のループは短いことがある．これらをまとめるのがループ融合． ○slide 15: 例題：画像処理で60段パイプライン化２つの forループを，１つの forループに変換するコード例． ○slide 16: 高位設計と検証問題機能中心で書いたものから，構造も考慮した記述に変換．合成ツールで自動合成するところに来たら，合成する．動作レベルからの合成においては，高位合成ツールを使う人と使わない人（手変換）がいる．レジスタ転送レベルRTL（いつ処理をするか，などが決定されている）にくると，たいてい論理合成ツールを使う．ただし，とても高速なハードウェアを設計する人は，今でも手設計，手変換している． ○slide 17: 上位設計と下位設計の違いの例メモリ：上位では配列アクセス．下位ではread,writeトランザクションさらに下位では，アクセスに何サイクルか（1以上）かかることを考えなければならない． ○slide 18: 下位設計にのみ現れるもの RTL以下の設計では，・故障テスト用回路（スキャンチェイン）：C言語ではあまり書かない・スリープモード・クロックゲーティング（必要ない場所のクロックを止める：低消費電力向け技術）・キャッシュメモリ・バス調停つきバス通信・ハンドシェイクなど通信プロトコル RTL以下で検証すべきこともある ○slide 19：形式的検証の流れ「設計の正しさを数学的（客観的）に証明する」デザイン（設計）とスペック（仕様）が与えられる．デザインはここではC言語．モデルチェッキングなどでは，仕様（スペック）として満たすべきプロパティが書かれている．等価性検証のときは，スペックもデザイン（デザインがスペックになる）．利用される数学モデル・Boolean関数・1回述語言語，サブセット・高階論理（定理証明）：基本的に対話的．人が自分で考える言語のフロントエンドも重要・検証ツール開発者からすると，入力言語を内部モデルに変換する処理が重要．・フロントエンドのほうが内部の検証処理よりも実行時間が長かったりするかもしれない・全体性能を決めてしまう場合も多い ○slide 20：解析手法 Boolean解析手法：基本的に2値(0/1)関数を扱う BDD (Binary Decision Diagram: 2値決定グラフ) SATソルバー（2000年以降，2値を扱うので，ワード変数を用いることはできない．ワード変数は，2値に展開する必要がある．実用化もされてきている．）ワード変数やその関数　無限ビット幅　（Infinite precisoion) ・Uninterpreted functions with equality や，その拡張　変数や関数について，中身は考えずに，　同じ名前の変数／関数は同じ，違う名前の変数／関数は違うとみなす検証をする手法も出てきている（十分条件のみ判定）　有限ビット幅（固定ビット幅）：オーバーフローを考慮したい場合・SMTソルバー（SATソルバーを含む．定理証明ツールのなかで，自動で動く範囲だけを取り出してつかえるようにしたツール）　真偽判定が有限時間で行えるものを集めたもの．ユーザは簡単に扱える．・決定グラフ（ワード変数を使うもの）　modulo演算のオーバフロー ○slide 21：決定グラフ（半分スキップ） Boolean関数：入力変数で場合わけ． Binary Decision Diagrams (BDD,FDD，KFDD, etc.) 算術関数ワード変数対応 ○slide 22 Taylor Expansion Diagram 多項式をテーラー展開したものをグラフ表現（関数fを微分可能な連続関数とする） Horner Expansion Diagram（スキップ） ○slide 23：Satisfiability (SAT, 充足可能性判定）問題 SAT（充足可能性判定）問題（fがCNF式で与えられる） fを１とするような各変数への値の割当は存在するか？存在するならその例を示し，存在しないならそれを証明する　例；(a+b)(!a+c)(a+!b) が１となるのは，a=c=1 DPLL：だれでも考え付くアルゴリズム　各変数について，0/1で場合わけをしていく．　ある場合について充足（１）したら終了．充足しない（０）なら，充足するまで場合分けとバックトラックを繰り返す． ○slide 24： SAT手法の歴史 1960年 DP 　　数十変数 1996年 GRASP 　数千変数　：場合わけで，同じことは2回しない（これを思いつくのに30年くらい） 2001 Chaff 　数万変数　： 2005-6 Minisat 数十万変数今では数百万変数扱える．だからSATが使われるようになってきている． ○slide 25: SATは最近急速に進歩している！ NP完全問題（変数の数に対して指数的に難しくなっていく問題）を扱うにもかかわらず，対数グラフ上で指数的に上昇している，と思わせるくらいの向上率を示すグラフ（最近は上昇率低下中）ランダムに論理式を生成して解かせると，40年前と今とで性能は変わらない． C言語から変換した論理式というのを対象とすれば，速い． ○slide 26：最近のSATソルバー基本：DPLLアルゴリズム，効率的BCP，矛盾解析によるLearning（同じことを2度しない）を使う平均性能は上がっている．最悪性能は上がらない． ○slide 27: SATツールの性能最近，性能が飛躍的に向上（最近では下火）性能：数百万変数で数百万項 ○slide 28: C言語記述から論理式への変換１．SSA形式（Static Single Assignment form: 代入文ごとに新しい変数を導入）に変換　　論理式では代入という概念がないため，代入は不可能．２．論理式に変換．問題：ワード変数や算術演算をBooleanに変換する必要代入ごとに新しい変数を導入する必要がある． →　SATで扱えるものは限られる数百行，1千，2千行くらいのCプログラムなら扱えるだけど，y1,y2,y3などをひとつずつBoolean展開するのはいや．（SSA変換は避けられない） ○slide 29：Uninterpreted Functions with Equality 等価な例：設計１：if a= b then X <- a*c else X<-b*c 設計２：X <-b*c SATでは解けないが，thenとelseで場合わけすれば，解ける -> SMTソルバ（見ればわかる，というスタンス） SMT(Satisfiavility Modulo Theory)ソルバー：定理証明ツールの自動化できる部分を取り出したもの例：Z3(Microsoft)，CVC3など自動化できる部分：Linear arithmetic, Inequality, Presburger logic,... uninterpreted とは，「* (かける)というのは，記号の上で同じであれば等価」とみなすこと．（+, - でもOK） SATはまじめに中身をinterpretしているから時間がかかる ○slide 30：算術演算（DSP）向き検証技術（スキップ） ○slide 31： Horner Expansion （スキップ） ○slide 32：例題例題：Anti-aliasing: F = 1/ 2sqrt(a**2+b**2) = 1/1sqrt(x) ・一時定数までテーラー展開・固定ビット幅で実装 x^6 の係数は同じだが，x^5, x^4,... の係数はまったく違う関数 F1, F2 F1 != F2 over Z　　　：x が整数ならば等価でない（見た目にも明らか） F1[15:0] = F2[15:0]　：x が 16ビット幅固定では，等価これをどう検証する？SATソルバーならできる．しかし有限時間で計算が終了しない． ○slide 33： Smarandache関数 30年ほど前に，Smarandacheという数学者が考案した Smarandache関数これが特別だという話ではない． Smarandache関数というトリックを使うと，簡単に解ける． Smarandache関数 S(b)は，「正数でありその階乗がbで割り切れるものの最小値」を返す関数． 1!, 2!, 3!は8で割り切れないが,4!は割り切れるので，連続する４つの正数の積は8で割り切れる → x(x+1)(x+2)(x+3) = 0 mod 8 ○slide 34：Modular-HED (M-HED)（スキップ） ○slide 35：実験結果複数の例題（多項式）で，ランタイムが０．０１で解ける．SATなら1週間ある特定の状況ではうまく判定できるというものを集めてきたのがSMTソルバーでも，そういうものがない場合には，SATを使うしかない．ワードレベルツールの性能 >> Booleanツールの性能 ○slide 36：スタティックチェッキングとモデルチェッキング・モデルチェッキングは初期状態から出発し，実行可能パスを全部調べ，到達可能な状態を「網羅的」に調べる（調べようとする）・しかし任意の状態からはじめることも可能・設計を一度抽象化してから解析を始めることも可能・研究者は，途中からはじめることを考える（バウンダリモデルチェッキング）・スタティックチェッキングは，検証項目に密接に関係した記述部分から解析を始め, かつ解析自体部分的（ローカルな解析）・Lintを高尚にしたやつ・しかし解析する範囲は拡張可能・研究者は解析範囲をローカルから全体へ広げようとしている． ○slide 37：状態空間探索例：Safetyプロパティ初期状態から初めて，到達可能な状態の中にバギーな状態があったら，悪いところから逆にたどっていって,初期状態に到達するかどうかを調べる．・明示的プロパティ検証　　個々の状態をひとつづつたどっていく・シンボリックプロパティ検証状態空間を論理関数で表現 BDDやSAT手法を応用 ○slide 38：モデルチェッキングアルゴリズム（スキップ） ○slide 39：バグ発見手法としてのモデル・スタティックチェッキング UNIXのとあるバグを見つけた例・配列の最後のを超えたアクセス・for文の中だけを見れば発見できる長さ10の配列 channel_bands に対し，cによって要素 channel_bands[10] を参照している while(((channel_bands[c] >>1) - 24) < freq && c < BAND_NUM){} しかしそのバグには到達しないかもしれない＝バグではないかも．初期状態から到達可能かどうかの判定が必要・モデルチェッキング：判定する・スタティックチェッキング：判定しない（バグでないものまでたくさん報告） ○slide 40：スタティックチェッキングで発見できる典型的な例例：別のLinuxのソース(drivers/net/wireless/hostap/hostap_hw.c: l.931--939) ------------------------------ if(res){ ....; return res;} if(res == -110) prism2_hw_reset(dev); ------------------------------ 最初のif文内に return があるので，2番目のif文に入るのは，res == 0 のときのみ．このとき，if(res == -110) は成立しない．よって内部の prism2_hw_reset(hw) は決して実行されない普通の意味でバグだが，そのままでも正しく動作する可能性は大．下手に直さないほうがよい？・スタティックチェッキングからの経験　検証しすぎるということはないか？　修正不要なバグを修正しろという．すると，次のバグを挿入してしまうかもしれない．　バグをどんどん報告されると困る？ ○slide 41：検証例 ○slide 42：コントロールフローグラフ（CDG）を生成 CFG上を作成， ○slide 43：CDG上を探索 CFG上を探索，実行可能パス上を探索（実際にパスを通る，ということは示す） ○slide 44：パスを解析（SAT/SMTソルバ）データフロー解析を併用 ○slide 45：実行の false path 問題実行されることのないパス ○slide 46：実際の false path 解析 ○slide 47：記号シミュレーション・C言語記述から，その動作を抽出する基本手法・intといわれたら32bit．だが，整数は変数のまま（a など）にすることも多い ○slide 48-49：記号シミュレーション例（絶対値計算） i の初期値を i0（記号値）と仮定して，分岐などでは条件式それぞれについて，もし～だったら，と順番に解析していく最後に分岐双方から得たiの状態を混ぜて，チェック ○slide 54：記号シミュレーションの問題点現状では最も効率的な解析手法であるが，シミュレーションが進むにつれて記号式が膨大になってしまうという問題点がある．記号式を共有して数を減らすために，Maximally Shared Graph と呼ばれるグラフを用いることで，式を最大限共有して管理し，数の増大をかなり防げるようになってきている．この考え方は，ハードウェア設計において，資源を最大限共有して回路規模を抑える話と基本的に同一． ○slide 55： Maximally Shared Graph SSA変換されたC言語記述をグラフ化．演算（に相当するノード）を共有している． ○slide 56：Maximally Shared Graph による記号式の管理（スキップ） ○slide 57：設計の抽象化による大規模プログラムの検証：Predicate abstraction Maximally Shared Graphの問題点：状態の数，変数の数が多すぎる代入のたびに新しい変数が生成される（SSA）同じ複数の状態を1個の状態にまとめる何らかの方法で少数のPredicatesを選ぶ ○slide 58-63：Predicate abstraction 手法例 predicate: x >0, x>y 何個変数があろうが，predicatesが2個なら，抽象状態は４個 ○slide 64：C言語記述を抽象状態空間へ変換 C言語記述は，BooleanProgramと呼ばれる，各Predicateに対するBoolean変数のみを利用するものに変換可能． ○slide 65：変換例 p: x>0, q:x>y x++は次のようになる if(p&&q){ //もともとx>0, x>yなら，２つの predicate は変わらない． }else if(p && !q){ // !q つまり x <= y なら，x++; によって x > y になるかもしれないし， // ならないかもしれない（x,yによる） q = non-deterministic(0,1); }else if(!p && q){ // !p つまり x <= 0 なら，x++; によって x > 0 になるかもしれないし， // ならないかもしれない（x による） p = non-deterministic(1,0); }else{ //!p && !q つまり x <= 0 かつ x <= y なら，x++ によって p も q も変化 // しうる（x,yによる） p = non-deterministic(1,0); q = non-deterministic(0,1); } ものすごく大雑把に解析（predicateの真偽のみを用いる．中身は忘れる） ○slide 66-69： predicate p:i > 0の場合のabs()の例条件式の中身（iがかかわるところ）を，pで表現 ○slide 70：Predicate abstraction の特徴（スキップ） ○slide 71：進歩が著しい分野 CBMC(Clarke, Kroening, Yorav, 2003 CMU) ANSI C を検証できる初めての検証ツール（C用Boundary Model Checker）数千行規模までものすごく正直にC言語をBooleanに変換してSATを解く． Calysto(Babic, Hu, 2007 UBC) 性能がいい（最新の技術を導入） ○slide 72： Calysto の性能抽象化などを利用して，数万～数十万行（の下のほう）のプログラムを検証可能 ○slide 73：形式的等価性検証（ここで時間がなくなってきた）藤田先生：「時間がないので，（これ以降の説明は）やめようかどうか考えている．質問があればやめます，質問がなければ続けますが…」質問： Q（座長：小野寺先生）：いま，等価性検証などをするためのC言語記述は，どんなC記述でもいい？検証しやすいCへの制約などは？ A. 等価性検証では，２つの記述に差があった場合，等価かどうかを検証する．ほとんど差がない記述が望ましい．　モデルチェッキングでは，あまり変数を使わない,など．ほか，質問なし（質問がないので続く） ○slide 74：状態空間の探索による等価性検証等価性検証では，可能なすべての入力シーケンスに対して，対応する出力が同じかどうかを調べる ○slide 75：C言語ハードウェア設計における等価性検証問題スケジューリングの違いなどがある．たとえばRTLでは，各クロックサイクルの動作が決定している． C言語レベルでは，順序は決まっているが処理時刻は部分的にしか決まっていない（メモリアクセスなど）組み合わせ回路の等価性検証とは異なり，設計者が時間的な情報を指定してあげる必要がある：しかし設計者がわかってない場合が多い ○slide 76：トランザクショントランザクションとは，上位設計における計算の単位．実行終了時には，同期タイミングに到達 ○slide 77：トランザクションレベルでの等価性検証同期する状態ごとに懸賞問題を分割できる ○slide 78：C言語記述に対する等価性検証の基本（スキップ） ○slide 79：簡単な例（スキップ） ○slide 80：問題点とわれわれのアプローチ大規模記述に記号シミュレーションは適用できない記述間の際に注目し，記号シミュレーションしなければならない範囲をできるだけ限定するだめなら範囲を広げる等価な場合は（検証速度が）速いが，非等価な場合には破綻したりする．等価だと確信して使うならよい． ○slide 81: Equivalence Checking Flow (スキップ) ○slide 82: 検証領域とその入出力（スキップ） ○slide 83-85: 例（スキップ） ○slide 86: 等価性検証環境FLEC（スキップ） ○slide 87: FLECの特徴これまでSTARCとの5年，これからCRESTの元で5年予定 ○slide 88: 扱える記述（スキップ） ○slide 89: ツールの構成（スキップ） ○slide 90: 取り扱うSpecC記述（スキップ） ○slide 91-92: ExSDG (Extended System Dependence Graph) （スキップ） ○slide 93: 等価性指定（スキップ） ○slide 94: 並列記述の扱い（スキップ） ○slide 95: 並列記述の順序化（スキップ） ○slide 96: ケーススタディ１：MPEG4 （スキップ） 2記述の差：IDCT内の定数伝播，共通式抽出など記述量 SpecCで約6,300行 ExSDGで約50,000ノード（生成時間780秒） ○slide 97: ケーススタディ２：Elevator Controller （スキップ） 2記述の差：制御系コードの最適化記述量 SpecCで約3,300行 ExSDGで約20,000ノード（生成時間178秒） ○slide 98：まとめ・シミュレーションだけでは検証しきれない設計者1人に対して検証エンジニア2人・SAT/SMTソルバーの研究が進んでいる・スタティックチェッキング数百万行で扱え，また全自動 FalseWarningの問題：バグ報告数が多いと誰も見ない．バグだが直そうとすると，かえってバグを混入させてしまう・デバッグ支援が必須シミュレーション，エミュレーションによる長い反例がでてもさっぱり・ ○slide 90：反例を短くしたい（予備スライド：講演された）ランダムシミュレーションから得られる反例は，一般的に非常に長く，なぜ悪いのか設計者は理解できない．これを，意味から考えて短くしたい（例：FIFOがいっぱいになって発生する）． ○slide 91：記号シミュレーションで反例を短くする方法（予備スライド：講演された）・ループを回っているのは無駄．ループを取り除く．・ショートカットを探す機能シミュレーションとSMTソルバーで短縮（研究レベル）：数100分の1の長さになりうる ■ 質疑（全発言）（講演途中の質問時間：再掲） Q（小野寺先生）：いま，等価性検証などをするためのC言語記述は，どんなC記述でもいい？検証しやすいCへの制約などは？ A. 等価性検証では，２つの記述に差があった場合，等価かどうかを検証する．ほとんど差がない記述が望ましい．モデルチェッキングでは，あまり変数を使わない,など．（講演最後の質問時間） Q. FalseWarningがあるといわれたが，ひとつのバグに複数のWarningを見ないといけないか？ A. 最初の３つくらいに解決したいバグに対応するものがあれば，設計者は見てくれる．無いと，あきらめる. ■ まとめモデルチェックの歴史，概要を解説された．モデルチェックや等価性検証のための計算量はまだまだ大きい．しかし，使いどころを工夫すれば，所望の結果を短時間で得ることも可能になる．課題としては，まだまだ，処理に時間のかかるSATソルバー（Boolean関数を対象）が必要となる場面が多いこと．また，形式的検証はデバッグのために使われるもののはずだが，出力されるバグ情報が（解決したいバグ以外にも出力されるため）多すぎて，開発者に対して逆に混乱をもたらす可能性があるところである．以上.