アーキテクチャと形式的検証の協調による超ディペンダブル VLSI 戦略的創造研究推進事業ディペンダブル VLSI システムの基盤技術東京大学大学院情報理工学系研究科坂井修一 ( 代表者 ) 五島正裕東京大学大規模集積システム設計教育研究センター (VDEC) 藤田昌宏東京工業大学大学院情

Size: px

Start display at page:

Download "アーキテクチャと形式的検証の協調による超ディペンダブル VLSI 戦略的創造研究推進事業ディペンダブル VLSI システムの基盤技術東京大学大学院情報理工学系研究科坂井修一 ( 代表者 ) 五島正裕東京大学大規模集積システム設計教育研究センター (VDEC) 藤田昌宏東京工業大学大学院情"

しまなおおはし
4 years ago
Views:

1 アーキテクチャと形式的検証の協調による超ディペンダブル VLSI 戦略的創造研究推進事業ディペンダブル VLSI システムの基盤技術東京大学大学院情報理工学系研究科坂井修一 ( 代表者 ) 五島正裕東京大学大規模集積システム設計教育研究センター (VDEC) 藤田昌宏東京工業大学大学院情報理工学研究科吉瀬謙二日本電気 ( 株 ) 若林一敏 2011/7/2 DVLSI-CREST

全体マップ : ディペンダビリティ階層 (1) 形式的検証手法等価性検証ソフトウェアハードソフト協調による検証高速化

テスト段階修復技術テスト容易化検証容易化を実現する設計手法プログラマブル素子自動挿入 (3) 回路技術タイミング制約緩和回路

最新アーキテクチャの検証 Best Effort Design Run Time Recovery 前半 3 年 : 方式検討

超ディペンダブルプロセッサ超ディペンダブルメニコア (5)(6) 新アーキテクチャ形式的検証

2 全体マップ : ディペンダビリティ階層 (1) 形式的検証手法等価性検証ソフトウェアハードソフト協調による検証高速化エミュレータへの応用ボトムアップトップダウン協調検証算術回路合成検証高速化設計解析技術デバッグ支援 (2) テスト技術テスト段階修復技術テスト容易化検証容易化を実現する設計手法プログラマブル素子自動挿入 (3) 回路技術タイミング制約緩和回路 (4) アーキテクチャ技術故障検出回復機構の提案実現耐永久故障 FPGA それぞれの階層で技術開発全体を通した最適化最新アーキテクチャの検証 Best Effort Design Run Time Recovery 前半 3 年 : 方式検討基本設計実験システム構築評価後半 2 年 : プロトタイプ試作と評価要素技術の統合 2011/7/2 耐故障高機能ルータ超ディペンダブルプロセッサ超ディペンダブルメニコア (5)(6) 新アーキテクチャ形式的検証ディペンダブルアーキテクチャ技術自体を形式的に検証既存のアーキテクチャ最新のアーキテクチャを形式的に検証 (7) 各設計階層間のディペンダビリティ役割分担を最適化 DVLSI-CREST

3 形式的検証 ( 藤田若林 )

4 基本戦略 (SoC 内のブロックごと ) 出口戦略 ( 発展テーマ ): 実設計での評価改良検証ツールにおける NEC 他との協調算術演算回路設計検証ツールポストシリコンデバッグツール C ベース設計記述 1 C ベース設計記述 2 設計ライブラリ ( 算術演算回路支援 ) チップの意図通りの正しい動作の保証 ( 向上 ): 仕様 ( 元の C 記述 ) 通りの動作誤設計のチップ製造後のデバッグと修正 ( 元の C 設計上のバグをチップ製造後に修正 ) 等価性検証 CWB の例題 C ベース設計記述 n NEC Cyber Work Bench (CWB) 高位合成設計環境 ( ポストシリコンデバッグ支援機構 ) RTL 設計ポストシリコンデバッグサポート等価性検証 ( チップコアブロック ) SoC 全体へはシミュレーションベース検証と統計的解析技術を導入 DVLSI-CREST 2011/7/2

5 等価性検証ツール (NEC との協調 ) C 記述 vs C 記述の等価性検証をターゲットに評価評価の結果 C vs RTLの等価性検証は現在の提案方式で効率的に検証することには時間がかかる ( 要内部等価点の生成伝達 ) C 記述 vs C 記述の等価性検証の検証に有効性がありそう実用 IP 回路を検証するための課題を洗い出し DES 暗号回路浮動小数点演算回路の検証を試行し縮小データで検証成功演算種類ビット幅に対する耐性が強いものの条件分岐に対して課題あり機能改善アイデアを試行中検証パス数の爆発を抑えるための手法一度の検証範囲を小さくするための手法 void main(){ b_0 = a_0 a_1 a_2; y_0 = x_0; y_1 = x_1; y_2 = x_2; } void main(){ tmp0 = a_0 a_1; b_0 = tmp0 a_2; y_0 = x_0; y_1 = x_1; y_2 = x_2; } 記述の差異のある部分から検証が必要な部分を抽出その部分に絞って検証差異がなく検証不要な部分検証済の部分を階層検証の手法で省略して効率化

6 Post-silicon デバッグ : 製造後機能修正可能なハードウェア技術 C プログラム小規模な製造後修正 ( 仕様変更故障修復等 ) 修正 C プログラム x << x x x << スケジューリング ( 高位合成 ) 配線 ALU ALU MUL SHFT 制御回路特定用途専用ハードウェアパッチ回路 ( 提案方式 ) 整数線形計画法に基づくインクリメンタルスケジューリング ( 提案手法 ) 製造後書き込みパッチ内容回路全体をプログラマブルにするのではなく制御回路を部分的に変更可能にすることで専用ハードウェア並みの効率性能を実現

7 最新成果 : 高位設計記述間の最小差分抽出 C プログラム小規模な設計修正 ( 仕様変更故障修復等 ) 修正後 C プログラムコントロールデータフローグラフ (CDFG) x << x 最小差分抽出 x x 修正後 CDFG 差分 CDFG (Δ CDFG) x << x 変更なし種類変更新規追加除去応用分野インクリメンタル高位合成 ( 既設計の再利用 ) パッチ可能ハードウェア用パッチ生成 (post-silicon 修復 ) 高位設計記述の等価性検証 ( 差異に基づく検証 )

8 シミュレーションベース検証固定値による単純シミュレーションは少数の場合のみを検証記号シミュレーションは網羅的だが初期状態から浅くしか検証できない両者の組合せによるバグを検出する確立が大きく増大各種効率的な処理技術を開発 : State joining, Path pruning, Path abstraction, Path Program, Hybrid concolic approach 固定値シミュレーション記号シミュレーションより効率的な探索 ( 検証カバレッジの向上 ) Hybrid concolic 実行コスト関数 ( カバレッジ ) の導入因果関係解析による時間を遡る方向への記号シミュレーション Hybrid concolic 実行との組合せ 2011/7/2 DVLSI-CREST

9 ディペンダブルアーキテクチャ ( 坂井五島 )

10 耐過渡耐永久故障 FPGA アーキテクチャ使いやすい高信頼 LSI の要求従来 : MIL 規格品低性能, 高価, 低入手性 ( 長納期 ) 提案 : FPGA ベース通常用途と両立することで, 安価で入手性に優れた LSI 置き換え L U T L U T L U T F F F F F F V o t e r 通常用途と両立 L U T L U T F F F F 高信頼化のための追加ロジックを最小化通常用途時高信頼用途時フォールト検出回復 TMR DPR 回復を行う制御回路 : Recovery Manager (RM) 従来手法 Software User Logic Hard-Wired Logic Config Subsystem RM Software User Logic Hard-Wired Logic Config Subsystem RM RM 従来方式 : ハードワイアード単一障害点となる通常用途時には余分な面積コスト提案方式 : ユーザロジック故障時に自分自身を再構成通常用途時には面積コスト 0 通常用途と高信頼用途を両立提案手法オーバヘッドなし Software User Logic Hard-Wired Logic Config Subsystem Software User Logic RM RM Hard-Wired Logic Config Subsystem

11 ばらつきの増大とワーストケース設計 LSI の製造ばらつきプロセスの進化ばらつき大ワーストケース設計は悲観的になり過ぎるワーストケースではなく現物の遅延に合わせる動的タイミングフォールト検出回復トランジスタの個数最悪値の向上典型値の向上トランジスタの速度度プロセス技術の世代速速度の平均値ワーストケース設計における速度ワーストに合わせると速度が上がらない

12 動的タイムボローイングを可能とするクロッキング方式 : ワースト遅延 : 実効遅延動作周波数を決めるのは単相 FF ワースト遅延のワースト静的 TB 二相ラッチワースト遅延の累積 Razor 実効遅延のワースト提案 = Razor 二層ラッチ実効遅延の累積ワースト遅延のワーストの半分動的 TB

13 耐タイミング故障 OoO スーパスカラプロセッサ成果故障検出回復機能付き OoO スーパスカラプロセッサをFPGAで試作, 基本動作を確認 LSQに生じるタイミング故障に対応するコミット方式を提案今後の計画ハイパフォーマンス系の研究成果を詰め込んだ本格的なプロセッサを試作予定本手法を用いた回復機構, コミット機構を実装評価する ROB tp cp hp LSQ コミット tp cp hp tail head RB LRF D$ 新規開発中のプロセッサを実装予定の大容量 FPGA 基盤新コミット方式ブロック図キャッシュと LSQ の間に Retire Buffer を追加仮に LSQ でタイミング故障が発生しても Retire Buffer に正しいステートが保持されている

14 ディペンダビリティ支援ルータ ( 吉瀬 )

15 SmartCore システム超ディペンダビリティ支援高機能ルータグループ高機能ルータを核として送受信パケットのレベルで多重実行を実現するシステム多数のコアと高機能ルータによってディペンダビリティ向上と速度向上を目指す出口戦略マルチコアコア / メニーコアのディペンダビリティ向上方式として確立実用化 : 半導体ベンダーへの方式提供車載システム ( 組込みシステム ) への展開研究を支援する実用的な基盤環境の提供 ( ソフトウェアのウェブ公開 ) Off chip memory modules and switch Memory (1,0) Memory (2,0) Memory (3,0) Memory (n,0) In X In X In Y Arbiter Out X Out X Out Y Conventional I/O Conventional RISC module (0,0) (1,1) (1,2) (2,1) (2,2) (3,1) (3,2) (n,1) (n,1) In Y In INCC ID translation node type V master / mirror ID XBAR Switch Out Y Out INCC 高機能ルータアーキテクチャ冗長実行自動支援のためのパケットの複製同一性検出マージの機能を実現パケットを送信する宛先を調整パケットを比較してエラー検出パケットを複製 2011/7/2 Many core processor chip Core (1, 1) INCC * memory (1, 1) Processing Element (1,m) (2,m) (3,m) Core (1, 2) memory (1, 2) Processing Element (n,m) * Inter Communication Controller 高機能ルータをもつマルチコアシステムアーキテクチャ M-Core INCC DVLSI-CREST

16 SmartCore システムによるメニーコアのディペンダビリティ向上ディペンダビリティ向上 (3,2) のディペンダビリティ向上の為 (4,2) と多重実行 (3, 2): マスター通信をすべてミラーに転送 (4, 2): ミラーマスターと同じ仮想 ID マスターからの通信のみで動作 (3, 2) のルータでCore(3, 2) とCore(4, 2) からのパケットを比較, エラー検出 Core (1, 1) (1, 1) Core (1, 2) (1, 2) (1, 1) (1, 2) Core (2, 1) (2, 1) Core (2, 2) (2, 2) (2, 1) (2, 2) Core (3, 1) (3, 1) (3, 1) (4, 1) Core (3, 2) Core (4, 1) Core (4, 2) (3, 2) (3, 2) (4, 2) 同じバイナリを実行 (4, 1) logical (3, 2) (4, 2) (3, 2) のディペンダビリティ向上のため (3, 2) と (4, 2) で多重実行する様子パケットの受信と転送パケットのチェックと送信マスターミラーマスターミラー Core(3, 2) 仮想 (3, 2) Core(4, 2) (3) 仮想 (3, 2) (3) Core(3, 2) 仮想 (3, 2) Core(4, 2) (1) 仮想 (3, 2) (1) P (1) (2) (3, 2) (4, 2) P (3) (2) (3, 2) (4, 2) (1) (3, 2) にCore(3, 2) が受信するパケットが届く (2) (3, 2) はパケットを複製しCore(4, 2) に送信 (3) 各 Coreが同じパケットを受信 2011/7/2 (1) 各 Coreがパケットを送信 (2) (4, 2) はパケットの送信先を (3,2) に変更 (3) (3, 2) はCore(3, 2) とCore(4, 2) からのパケットを待ち合わせ, 比較. エラーがなければ送信 DVLSI-CREST

CLEFIA_ISEC発表

CLEFIA_ISEC発表 128 ビットブロック暗号 CLEFIA 白井太三渋谷香士秋下徹盛合志帆岩田哲ソニー株式会社名古屋大学目次背景アルゴリズム仕様設計方針安全性評価実装性能評価まとめ 2 背景 AES プロジェクト開始 (1997~) から 10 年 AES プロジェクト攻撃法の進化代数攻撃関連鍵攻撃新しい攻撃法への対策暗号設計法の進化 IC カード, RFID などのアプリケーション拡大