卒論発表

Size: px

Start display at page:

Download "卒論発表"

きょうすけひめい
5 years ago
Views:

1 0 年度 ( 平成年度 ) 広島市大卒業研究実現するアルゴリズムの証明に注目した ASIP のシステム検証広島市立大学情報科学部情報工学科錦織光輝 ( 高橋隆一指導 ) Mitsuki Nishikori

2 研究背景 0 年代には Verilog HDL によって仕様を記述し, 論理合成によって回路を実現するスタイルが普及した検証技術が論理合成に続く技術として期待されている満たすべき性質をアサーションとして記述することによるシミュレーションでの検証 (ABV) が普及しつつある特定用途向け専用プロセッサ (ASIP) が注目されているアサーションの記述方法は必ずしも確立されていない本研究では, 実現するアルゴリズムに注目した ASIP の ABV を模索する

3 高橋研究室での従来研究アサーションの構成方法アルゴリズムで普遍的に成り立っている性質に注目処理対象の性質に注目データ構造 ( スタック ) に注目データ構造 ( ヒープ ) に注目データ構造 ( キュー ) に注目背景のマトロイドに注目事例 x と y の拡張ユークリッドの互除法において余りは常に ax+by の形であることを検証バブルソートにおいて連続するつの要素に対する操作を検証クイックソートにおいてスタックポインタが下がる前には POP 命令が読まれていることなどを検証ヒープソートにおいて親のノードの値が子のノードの値よりも小さいことなど検証幅優先探索における ENQUEUE DEQUEUE などを検証クラスカルのアルゴリズムにおいて連結成分に閉路がないことを検証

4 特定応用分野向きプロセッサ application specific instruction-set processor(asip) 特定の応用分野に適したアーキテクチャを持つプロセッサハードウェア積和演算器 (Multiplier accumulator (MAC)) を内蔵したデジタル信号処理プロセッサ (digital signal processor(dsp)) は ASIP の代表格汎用プロセッサ (general purpose processor(gpp)) と特定用途向き集積回路 (application specific integrated circuit (ASIC)) の間を埋める手段

5 ASIP の位置付け汎用性 (Flexibility) GPP DSP ASIP ASIC 特定の用途での性能 (Performance) デジタル信号処理プロセッサ (DSP)) は ASIP の代表格

6 二部グラフ頂点集合をV, V に分割したとき, すべての枝が V の頂点とV の頂点を結ぶようにできるグラフを二部グラフという V V

7 二部グラフにおけるマッチング枝集合で互いに端点を共有しない組マッチング V V

8 二部グラフにおける最大マッチング枝数が最大のマッチング ( 枝の集合 ) V V 赤がマッチング

9 二部グラフにおける交互経路の例マッチングの枝とマッチングでない枝が交互に現れる経路を交互経路という交互経路

10 二部グラフにおける増加経路の例マッチングの枝の端点を飽和点, マッチングでない枝の端点を不飽和点という両端点が不飽和点である交互経路を増加経路という飽和点増加経路不飽和点不飽和点 0

11 現在のマッチングと増加経路の対称差現在のマッチング M と増加経路の対称差をとることで枝の増えた新たなマッチング M が得られる = 現在のマッチングM 増加経路新たなマッチングM M AUGMENT_PATH=M

12 二部グラフの最大マッチングを求めるアルゴリズム開始現在のマッチングにおける増加経路を探す現在のマッチング増加経路新たなマッチングを現在のマッチングとする増加経路が存在するか false 終了 true 現在のマッチングと増加経路との対称差をとる M AUGMENT_PATH=M 対称差をとる新たなマッチング

13 設計した ASIP の計算機構成 bit Instruction Memory Unit bit Verilog 行数 : LUT 数 :(Xilinx Spartan) bit bit Data Memory Unit Flag Register A_BUS B_BUS Progra m Counter Prefetch Unit Instruction Register IR ready bit Decode Unit bit Operands Decoded OPcode Decoded OPcode ready bit bit Augment Path Investigator Central Processing_Unit REG0 REG REG C_BUS Execution Unit

14 検証の前提三段パイプラインの正当性は検証済みパイプラインインターロックは正しく設計されているフォワーディングも正しく行われているフォワーディングに対するアサーションが満たされている作りこみ品質は高い問題点があるとすれば増加経路の取り扱い Augment Path Investigator

15 アルゴリズムの証明アルゴリズムの根拠 M: 現在のマッチング増加経路が存在しない M は最大マッチングである必要性対偶十分性対偶 Mは最大マッチングである増加経路が存在しない増加経路が存在する Mは最大マッチングでない自明増加経路が存在しない Mは最大マッチングである Mが最大マッチングでない増加経路が存在する最大でないマッチングと枝数の多いマッチングとの対称差をとることで存在が証明ができる

16 現在のマッチングと新たなマッチングの対称差最大ではないマッチングと枝数の多いマッチングの対称差をとると増加経路が現れる = 最大ではないマッチング枝数の多いマッチング増加経路

17 証明に注目した検証現在のマッチングと新たなマッチングとの対称差が増加経路になることを検証 M M =AUGMENT_PATH M: 現在のマッチング M : 新たなマッチング AUGMENT_PATH: 増加経路 core_dmu_mmx: assert property CLOCK) (LAST==0)##(LAST==) ->CHECKPATH); 証明に注目したアサーション ( 満たされるべき性質の記述 )

18 検証時のアクセス assertion_for_dm.sv core_dmu_mmx: assert property CLOCK) (LAST==0)##(LAST==) ->CHECKPASS); 証明に注目したアサーションマイクロアーキテクチャはポートを通してメモリにアクセスする (Verilog HDL) アサーションはメモリ内部を直接検証する (SystemVerilog でバインド )

19 バインド (bind) アサーションをモジュール内に置く手段 Verilog HDL RISC_B imu.v dmu.v alu.v ru.v exu.v pfu.v du.v cpu.v dmu:data memory unit dmu の下にアサーションを置くことになる bind.sv 実行ユニット execution unit (exu) SystemVerilog 特有 assertion_for_fr.sv assertion_for_dm.sv リンクリストを検証アサーションはメモリ内部のリンクリストを直接調べる実行ユニットはバスを介してメモリにアクセスする

20 ABV の結果 M M =AUGMENT_PATH アサーションは通らなかった増加経路の取り扱いに問題がある最大でないマッチングと増加経路の対称差をとるハードウェアの問題 M: 現在のマッチング M : 新たなマッチング AUGMENT_PATH: 増加経路 M AUGMENT_PATH=M 増加経路を求めるハードウェアの問題 0

21 バグの特定 core_dmu_num: assert property CLOCK) (LAST==0)##(LAST==) ->CHECKNUM); 新たなマッチングの枝数が現在のマッチングの枝数より多いことを検証最大でないマッチングと増加経路の対称差をとるハードウェアに問題が見出された

22 バグの特定 core_dmu_v: assert property CLOCK) (LAST==0)##(LAST==) ->CHECKV); 増加経路の端点が不飽和点になっていることを検証増加経路を求めるハードウェアに問題が見出された

23 まとめと今後の課題まとめ実現するアルゴリズムの証明に注目した ABV で設計した ASIP のバグを見出せることを示した今後の課題他のアルゴリズムに対しても同様な手法が適用できるかを確認すること

Verilog HDL による回路設計記述

Verilog HDL による回路設計記述 Verilog HDL 3 2019 4 1 / 24 ( ) (RTL) (HDL) RTL HDL アルゴリズム動作合成論理合成論理回路配置配線ハードウェア記述言語シミュレーションレイアウト 2 / 24 HDL VHDL: IEEE Std 1076-1987 Ada IEEE Std 1164-1991 Verilog HDL: 1984 IEEE Std 1364-1995