学位論文要旨



No 124577
著者(漢字) 高,尚
著者(英字)
著者(カナ) コウ,シャンカ
標題(和) 通信指向ハードウェア合成とその形式的検証
標題(洋) Communication-Oriented Hardware Synthesis and Its Formal Verification
報告番号 124577
報告番号 甲24577
学位授与日 2009.03.23
学位種別 課程博士
学位種類 博士(工学)
学位記番号 博工第7011号
研究科 工学系研究科
専攻 電子工学専攻
論文審査委員 主査: 東京大学 教授 藤田,昌宏
 東京大学 教授 浅田,邦博
 東京大学 教授 近山,隆
 東京大学 准教授 中山,雅哉
 東京大学 准教授 池田,誠
内容要旨 要旨を表示する

As VLSI process technology advances, the gap between gate delay and (global) interconnect delay is getting wider and wider. This makes interconnect delays (especially global interconnect delays) one of the most important factors that can affect performance. Under such situation, many state-of-the-art researches in high level synthesis try to consider the effect of interconnect delays. These researches indeed achieve better performance compared with traditional ones that ignore interconnect delays. However, when applications contain large loops (e.g., digital signal processing algorithms), there is still much room to improve performance, since usually, such applications contain computations that can be executed concurrently, they offer the possibilities of exploiting the parallelism.

In this work, we, for the first time, propose the idea to utilize pipelining techniques and take interconnect delays into account together into high level synthesis so as to improve its quality. This is not an easy task, since interconnect delays are unknown at the stage of high level synthesis. Usually they are not understood until after placement and routing.

In order to facilitate the estimation of interconnect delays, we propose a novel architecture, called regular distributed-register architecture for dynamic routing (RDR-dr). It divides a chip into a two dimensional array of islands, and the interconnect delay can be roughly estimated from the location of related islands.

Then, with the estimated interconnect delay information, we try to solve the problem of integrating both the effect of interconnect delay and pipelining techniques into high level synthesis by using exact solution methods such as Integer Linear Programming (ILP) and Boolean Satisfiability (SAT). We formulate the problem in the form of ILP/SAT, and then utilize commercial existing ILP/SAT solvers to find the solutions. As a result, for small examples, the exact methods can solve. But for relatively large examples, the exact methods can not solve within eighteen hours.

In order to improve the efficiency, we then propose a heuristic pipeline scheduling algorithm for array based architectures considering interconnect delays, and develop corresponding interconnect-aware pipeline synthesis system. The proposed method has the following two characteristics: 1) it separates the consideration of interconnect delay from computation delay, and allows concurrent data transfer and computation; 2) it belongs to modulo scheduling framework, in the sense that all iterations have identical schedules, and are initiated periodically. We evaluate the proposed heuristic method from different points of view and the experimental results show that: (a) our proposed interconnect-aware pipeline synthesis outperforms the existing works in high level synthesis which consider the effect of interconnect delays or utilize pipelining techniques; (b) the quality of our heuristic method is almost the same as that of exact methods; (c) our proposed algorithm is able to solve large practical problems, and for an example with 883 nodes, it takes only 2 seconds.

Since the pipeline synthesis with interconnect delay considered needs complicated algorithms, the synthesizer may contain bugs. To check the correctness of the synthesizer, we propose an approach which applies a combination of induction method and symbolic simulation technique. Based on this approach, we develop a prototype equivalence checker. The inputs to the checker are a loop in high level description and a pipelined loop. In the experiment, we verify several loop examples before and after pipeline synthesis including ones that bugs are intentionally inserted. The results show that: 1) for the examples in which we intentionally insert bugs, our prototype equivalence checker detects the not-equivalence in very short runtime; 2) for the examples obtained from automatic interconnect-aware pipeline synthesis, our developed prototype equivalence checker judges that the loops before and after pipeline synthesis are equivalent. This result demonstrates that our developed interconnect-aware pipeline synthesizer works correctly.

As a conclusion, an efficient interconnect-aware pipeline synthesizer is developed. At the same time, its correctness is confirmed. If introducing the synthesizer with existing design flow which starts design from RTL level, one can get a higher performance chip in shorter turn-around time. We are sure that the tool is more useful in future as process technology advances.

審査要旨 要旨を表示する

本論文は、Communication-oriented hardware synthesis and its formal verification(通信指向ハードウェア合成とその形式的検証)と題し、VLSI設計における高位設計において、配線遅延など通信に要する時間を考慮した自動合成手法を提案し評価するとともに、自動合成結果の正しさを形式的に検証する手法も合わせて提案し評価しており、7章から構成される。

第1章は、Introduction(序章)であり、研究の背景と目的を述べている。特に、VLSI高位設計においても、配線など通信時間を考慮した最適化が、チップの高性能化の点で非常に重要であることが示されている。

第2章は、Fundamental Techniques and Related Works(基盤技術と関連研究)であり、従来から研究・開発されてきている、高位からのVLSI自動設計における配線や通信時間の考慮法について説明している。従来手法では、一旦回路構造を生成してから、配線遅延を評価し、必要に応じて回路構造の再合成/修正を繰り返しており、設計を収束させるための労力が非常に大きい。そこで、物理構造をもった並列計算モデルをあらかじめ用意して、それに自動的にマッピングする形で自動合成を行う手法も研究されているが、現在までのところ、パイプライン実行などが無い、単純な計算に対してしか適用できていない。また、本章では、整数線形計画法、論理関数の充足可能性判定手法、それに記号シミュレーション技術など、本研究で利用する基盤技術についても、概要を説明している。

第3章は、A New Regular Distributed-Register Architecture for Dynamic Routing: RDR-dr(動的経路変更可能な分散レジスタアーキテクチャRDR-drの提案)であり、従来から提案されている分散レジスタアーキテクチャRDRに対し、個々の配線経路を動的に変更可能とする新規アーキテクチャRDR-drを提案し評価している。経路を動的に変更可能とするためには、配線網内にスイッチを一定間隔で挿入する必要があるが、そのためのVLSI内での面積は配線網内に隠蔽できるため、経路を動的に変更可能としても、VLSI内の面積は増大しない。実験結果により、提案アーキテクチャとすることで、必要となる配線経路数が大幅に現状でき、結果として配線/通信遅延が減少し、回路面積と計算速度の両面で有効であることが示されている。

第4章は、Exact Methosyas for Interconnect-Aware Pipeline Synthesis (通信を考慮したパイプライン合成の最適解法)であり、与えられたデータフローグラフに基づく設計記述から、それをパイプライン動作により並列処理するハードウェアを前章で提案したアーキテクチャにマッピングすることで実現する手法に関し、最適解を求めるアルゴリズムの提案とその評価を行っている。整数線形計画法と論理関数の充足可能性判定問題にそれぞれ帰着して最適解を求めている。実験結果により、比較的小さいデータフローグラフでは最適解を実際に求められることが示されている。

第5章は、An Efficient Method for Interconnect-Aware Pipeline Synthesis(通信を考慮したパイプライン合成の効率的な解法)であり、前章で示された最適解を求める手法に対し、ヒューリスティックに基づく効率的な解法が提案され、実験によりその有効性が示されている。まず、基礎となる一般的なパイプライン合成手法を示し、それを配線/通信時間を考慮できるように拡張する。次にそれを用いて、ハードウェア合成の各ステップであるスケジューリング、演算器の割当て、配線経路の割当てを通信時間も考慮しながら順次行うことで、一貫したハードウェア設計手法となっている。実験結果により、大規模設計でも処理可能であることが示されるとともに、小さい例題に対しては、前章の最適解を求める手法と合成されたハードウェアの性能がほとんど変わらないことが示されている。

第6章は、Formal Verification of the Correctness of the Synthesis(合成結果の形式的検証)であり、前章までで示された合成手法に基づき生成されたハードウェアの動作がもとの設計記述と等価であることを形式的に検証する手法が提案され、実験を通して評価されている。自動合成されたハードウェアでも、自動合成プログラムに誤りがある場合もあるため、その動作と元の設計記述の等価性検証は、一般的に行われている。そこで、本章では、合成手法の特徴を利用して、その等価性検証を形式的に効率よく行う手法が提案されている。自動合成手法に沿った検証手法であるため、大規模設計でも効率よく形式的に検証できることが、実験により示されている。

第7章は、Conclusion and Future Work(結論と今後の課題)と題し、本論文の研究成果をまとめるとともに、今後の発展方向について議論している。

以上、本論文は高位設計記述からパイプライン化された高性能ハードウェアを生成する際に、配線/通信時間を考慮しながら同時にレイアウトも行う自動合成手法を提案し、評価結果から大規模設計にも効率よく適用でき、その有効性が示されるとともに、自動合成結果の形式的検証手法も確立しており、電子工学発展に寄与する点は少なくない。

よって本論文は博士(工学)の学位請求論文として合格したものを認められる。

UTokyo Repositoryリンク