ニューラルネットワーク実時間組み込みソフトウェアの検証

学部電気電子工学科
本郷
大学院工学系・電気系工学専攻
藤田昌宏研究室(Prof. Masahiro Fujita)
Fujita Laboratory
URL:http://www.cad.t.u-tokyo.ac.jp
浅野キャンパス武田先端知ビル 4F
Asano-Campus Takeda Bldg. 4F
Cyber Physical System とは？
Cyber Physical System とは、社会の様々な場所で活用されて
いる実時間組込みシステムから得られる情報とコンピューティング
を組み合わせ、より高度な社会を実現するための枠組みのことです。
藤田研究室では、Cyber Physical System を支える情報機器―
VLSI, 組込みソフトウェア―を設計・検査する技術を開発したり、
集約した情報を効率的に活用するための計算手法・実装手法を
研究しています。
VLSI 設計支援
実時間システムに搭載される LSI チップなどの半導体
製品は、ソフトウェアと異なり後から修正することが非常
に難しいため、厳密な検証やテストや間違いを製造後に修正す
る技術などが高い信頼性を保つために重要になります。当研究室
では、システムレベルからポストシリコンまでの各ポイントにおける
合成・検証・テスト技術をカバーし、ディペンダブルな LSI の設計を支
援しています。
䕺6SHFLILFDWLRQ
ニューラル
ネットワーク
䕺5HSODFHDQ(25ZLWK/87
25ZLWK/87
2-input
LUT
FPGA
(UURQHRXVSRUWLRQ
仕様分析
システムに対する要求を分析し、
設計するシステムの動作や仕様
を決定する。
論理回路のデバッグ
システム設計
システム全体の動作をC言語ベー
スの言語で行う。HW/SW分割や
アーキテクチャ決定を行う。
ゲートレベル設計
回路を論理式として表し、
その
式をもとに、
論理ゲートを用い
て回路を設計する。
RTL設計
ハードウェア上で用いる演算器や、
演算の順番を定め、
レジスタ間の
データ転送を設計する。
レイアウト設計
セルやトランジスタとして表現さ
れた回路を実際に配置配線する
VLSI の設計フロー
ニューラルネットワークとは脳の機能を数学的に表した
モデルです。本研究室では、プログラム可能な回路である
FPGA 上に高度にパイプライン化された回路を構築し、256 ス
パイク型ニューロンのネットワークを生体比 320 倍で動作させる
ことに成功しています。この回路はさらに大きな神経回路網にも対
応できるように設計されており、現在は複数の FPGA チップを使っ
た数万ニューロンの大規模化について研究中です。
実時間組み込み
ソフトウェアの検証
ニューラルネットワークのモデル式
差分方程式化後
1
2
0.8
2
8v (t) + 4v(t) − n + I0 + Istim
(v(t) < 0)
v(t + ∆t) =
−8v 2 (t) + 4v(t) − n + I0 + Istim
(v(t) ≥ 0)
2
− n(t) (v(t) < r)
2v (t) + v(t) + 14 v(t) − 16728
n(t) + ∆t
15
τ
2
n(t + ∆t) =
2560
2
n(t) + ∆t
(t)
−
v(t)
+
−
n(t)
(v(t) ≥ r)
16v
τ
215
Is (t) + ∆tα (1 − Is (t)) (v(t + ∆t) > 0)
Is (t + ∆t) =
Is (t) − ∆tβIs (t)
(v(t + ∆t) ≤ 0)
4
v(t) +
v(t) +
0.6
0.4
0.2
0
-0.2
実時間システムの安全性を担保するには、搭載されるソ
フトウェアの検査・検証も重要です。近年、実時間システム
が高性能化・高機能化するに従ってソフトウェアの複雑化も
進んでおり、より高度な検証技術の開発が望まれています。当研究
∆tϕ
τ
∆tϕ
τ
-0.4
-0.6
-0.8
0
10
20
30
40
50
60
70
学習回数と
ニューラルネットワークの応答波形
室では、実時間システムに特徴的な割り込み処理の自動検証技術の開
発などを行っています。
最適化後のクロックごとの計算概要（上）
最適化前のクロックごとの計算概要（下）
a>1
1 int func(int a,int b){
if(a>1){
2
T
f
if(a<b){
3
func3();
if(a*b<0){
4
T
f
a<=1
func1();
5
}else{
6
T
f
func2();
7
a>1 ∧ a>=b
func1();
}
func2();
8
}
9
}else{
10
×a>1 ∧ a<b ∧ a*b<0
func3();
11
a>1 ∧ a<b ∧ a*b>=0
}
12
Symbolic Execution
13 }
ソフトウェアテスト手法
a<b
藤田研究室と
実時間・高速計算システム
a*b<0
Acceptance Test
受け入れテスト
SW Requirements
SW要求定義
Component Test
統合テスト
SW Basic Spec
SW基本設計
SW Detail Spec
SW詳細設計
インスリンポンプ
インスリンを自動注入する医療機器
Requirements
要求定義
Acceptance Test
受け入れテスト
Architecture
基本設計
Unit Test
単体テスト
System Test
システムテスト
Detail Design Integrated Test
詳細設計
統合テスト
Implementation
実装
Coding
プログラム
組込みシステム・組込みソフトウェアの設計フロー
Cyber
Physical
よりスマートな実時間システム・スーパーコンピュータ
級の高速計算システムを実現するには、数学的な解析が欠か
せません。
当研究室は、そのような数学や論理学の基礎理論を応
用した VLSI 設計・検証の研究において高い評価を受けています。
また、そのような理論を用いて設計された専用ハードウェアシス
テムは汎用計算機より高性能かつ低消費電力化が可能であり、
様々な分野で利用可能です。当研究室に興味のある方はご連絡下
さい。
設計技術
System
Cyber Physical System
東京都文京区弥生 2-11-16
東京大学武田先端知ビル 407 号室
Tel: 03-5841-6673
www.cad.t.u-tokyo.ac.jp
池之端門
駅
根津
C
武田先端知ビル
BUS
学 01/07
弥生門
東大前駅 N
< アクセス >
東京メトロ千代田線根津駅
徒歩 4 分
鉄門
工3
竜岡門
工２
正門
赤門
M
本郷 3 丁目駅
E
武田先端知ビル
藤田研究室では、Cyber Physical System を支える情報機器―VLSI, 組込みソフトウェア―を設計・検査する
技術を開発したり、集約した情報を効率的に活用するための計算手法・実装手法を研究しています。

Download Report