Due to the great advance of semiconductor technology, the integration of VLSI (Very Large Scale Integration) circuits has been increased for many years. This enables to integrate more and more transistors on a chip, which results in that a large whole system can be realized as a single chip so called System-on-a-Chip (SoC). When we design an SoC,it is a serious problem that the design period tends to be very long since the design size of SoCs is much larger than that of the conventional VLSI designs. To use billions of transistors that can be integrated in a chip,the design productivity of SoCs should be much improved.

One solution to improve the design productivity is introducing systemlevel design as a starting point of SoC design. In the most hardware designs, designers start designing from RTL (Register Transfer Level).In RTL, the function executed by combinational circuits for each clock cycle and the hardware resources (for example, adder and multiplier) to execute the function are decided. On the other hand, in system level, the (partial) execution order of the behaviors and the functional units consisting of many memory elements and combinational circuits (for example, filter and inverse discrete cosine transform) to execute the behaviors are decided. Therefore, we can say that system level design is more abstract than RTL design in terms of time and hardware resources.Since SoCs usually implement a system consisting of both hardware and software, it is preferable to use a single design language to describe designs. To satisfy this need, C language or C-based design language is used in system level design, which enables to design both hardware and software seamlessly.

Currently, system-level design is not completely automated by tools.That is, before the final design descriptions that can be processed by behavioral synthesizers and compilers are generated, a number of refinements,changes, and optimizations of design descriptions are carried out by designers. Therefore, it is very important to check the equivalence of the design descriptions when they are modified. This is because, if the bugs inserted in system level are found in the later design steps, for example in RTL or in gate-level, a lot of time and cost will be spent to debug. Therefore, equivalence checking of system-level designs is studied.

In system-level design, there are few formal verification methods that are used widely in industry, and simulation plays a main role to verify designs. This is because large system-level designs cannot be solved by formal methods in practical periods. At the same time, however, simulation has also a serious problem in feeding good test patterns when a design is very large. Currently, state-of-the-art formal verification methods can solve one module of system-level design, which is corresponding to the size that can be synthesized by behavioral synthesizers. If our proposed methods can check the equivalence of two large design consisting of several modules, it can be said that the scalability of formal methods is much improved.

One powerful method to check the equivalence is applying symbolic simulation to both of the designs under verification with generating equivalence classes of variables and expressions. This approach does not need any test patterns, hence, can be classified as formal verification.However, it cannot be applied to large designs since the run time of symbolic simulation increases exponentially to the design sizes. To realize efficient equivalence checking of large system-level design descriptions,in this thesis, several verification methods are proposed.

The proposed verification methods utilize the difference between the design descriptions. In practical, system-level design is proceeded by gradually refining designs step by step. Therefore, the difference between designs of one refinement step is expected to be relatively small. The basic idea of the proposed method is that we can reduce the computation effort of equivalence checking utilizing the difference.

An efficient equivalence checking method is proposed that reduces the number of equivalence checking between variables and expressions utilizing difference. Using the difference and dependence of designs, in this method, equivalence checking of variables and expressions is not carried out when two variables under checking are not affected by any difference. This method enables more efficient verification for designs with the same or similar control structures. However, the verification time by this method increases exponentially to the design size, although it can reduce a large number of equivalence checking between variables and expressions.

A more efficient equivalence checking method using difference is proposed.In the method, symbolic simulation is applied only to the related portions to the difference, while it is applied from the start to the end of each path in the previous method. For each difference between the designs under verification, equivalence checking based on symbolic simulation is performed first only for the difference. If all differences can be proved to be equivalent, the result of the verification is equivalent.When a difference cannot be proved to be equivalent, the verification is repeated extending the verification areas until the equivalence is proved.The extension of the verification areas is carried out along data and control dependence. This local checking approach results in that the equivalence can be proved with small computation effort even if the design itself is very large.

When verifying designs including parallel behaviors, it is impossible to apply equivalence checking to all possible schedulings, since the number of schedulings increases exponentially to the design size. To solve the problem, a sequentialization method is proposed. Given a design description with parallel behaviors, the method generates an equivalent design description without parallel behaviors. In the method, two statements that can be executed in parallel and dependent to each other are checked whether or not the execution orders of them is always the same. If the statements are always executed in the same order due to synchronization, they can be sequentialized into an equivalent two sequential statements. Otherwise, they cannot be sequentialized, since the executions of the statements may occur different results depending the execution orders. Using this sequentialization method, equivalence checking of two parallel behaviors can be reduced to equivalence checking of only a pair of two sequential behaviors, instead of checking many pairs of all possible scheduling.

When verifying designs including parallel behaviors, it is impossible to apply equivalence checking to all possible schedulings, since the number of schedulings increases exponentially to the design size. To solve the problem, a sequentialization method is proposed. Given a design description with parallel behaviors, the method generates an equivalent design description without parallel behaviors. In the method, two statements that can be executed in parallel and dependent to each other are checked whether or not the execution orders of them is always the same. If the statements are always executed in the same order due to synchronization, they can be sequentialized into an equivalent two sequential statements. Otherwise, they cannot be sequentialized, since the executions of the statements may occur different results depending the execution orders. Using this sequentialization method, equivalence checking of two parallel behaviors can be reduced to equivalence checking of only a pair of two sequential behaviors, instead of checking many pairs of all possible scheduling.When symbolic simulation is applied to loops, they are unrolled to avoid the execution paths with infinite length. This results in the increase of verification time especially when the number of unrolling is large. As a solution of the problem, an equivalence checking method of loops without loop unrolling is proposed. It identifies the symbolic values of loop iterators that are required to compute an arbitrary index of the output arrays. After the required symbolic values of the iterators are extracted, symbolic simulation is applied only to the values for equivalence checking. As a result, the number of statements to be symbolically executed does not increase even if the number of iterations is actually large.

The several experiments conducted in this thesis confirm that the proposed methods enable to verify the equivalence of large system-level designs between practical design refinements.

本論文は、Efficient Formal Equivalence Checking Methods for System-Level Design Descriptions(システムレベル設計記述に対する効率的な形式的等価性検証手法に関する研究)と題し、C言語ベース設計に基づく、システムレベル設計における2つ設計記述間の形式的な等価性検証手法の提案を行うとともに、実験結果によりその有効性を示しており、8章から構成される。なお、開発された技術は、等価性検証ツールとしてまとめられ、産業界においても実設計による評価が始まろうとしているなど、実用性の面からも注目されている。

第1章は、Introduction(序章)であり、研究の背景と目的を述べている。特に、システムレベル設計とC言語ベース設計の現状についてもまとめている。

第2章は、Fundamental Techniques and Related Works(基盤技術と関連研究)であり、従来から研究・開発されてきている、電子機器設計のためのC言語をベースとしたシステムレベル設計手法、特にその中で重要な位置を占める形式的等価性検証手法の現状を説明している。また、システムレベルの形式的等価性検証を行う上での基盤技術である記号シミュレーションとそれを効率よく実現するための関連技術を整理している。さらに、システムレベル設計段階で行われる各種設計最適化技術と等価性検証の関係を説明している。

第3章は、Sequentialization Method of Parallel Behaviors (並列動作の順序化)であり、設計対象の並列動作を検証するために、並列動作から等価な動作をする順序動作への自動変換手法について、議論している。以前提案された、整数線形計画法を用いた並列動作間の実行順序を解析する技術をベースとし、並列動作プロセス間の個々の動作の実行順序関係を解析することで、与えられた並列動作を等価な順序動作に自動変換する手法を提案し、評価している。並列動作間のスケジューリングによって実行結果が変化するような場合、設計の動作が一意に決定しないことになるため、設計エラーであると判定する。そうでない場合には、並列動作と同じ実行結果が得られる順序動作が生成される。実験の結果、扱える規模も実用レベルであることが示されている。この技術により、等価性検証は、順序動作同士の間でのみ行えばよいことになり、検証効率が大きく向上する。

第4章は、Efficient EqvClasses Generation During Symbolic Simulation Utilizing

Differences between Designs (記号シミュレーションによる等価性クラス生成における設計間の差異を利用した効率化)であり、記号シミュレーションによる形式的等価性検証手法の効率化手法を提案・実装し、評価している。等価性検証は、記号シミュレーションを設計記述の最初から最後まで順次適用することで実現できるが、このようにすると設計記述が大規模な場合には記号シミュレーション処理が終了しなくなる。そこで、比較する2つの設計記述間で異なる部分が少ない場合には、その差異を予め抽出しておき、記号シミュレーションは記述の先頭から行うが、実際に等価かどうかの判定を行うのは記述の差異の部分だけにすることで、検証時間を大幅に短縮することができる。このことを利用した等価性判定手法の有効性が実験によって確認されている。

第5章は、Efficient Equivalence Checking by Applying Symbolic Simulation Locally to the Difference between Designs (記号シミュレーションの設計の差異部分へ適用による等価性検証の効率化)であり、4章の手法をさらに発展させ、記述間の差異部分のみを記号シミュレーションで解析することで、等価性を形式的に検証する手法を提案している。本手法により、比較している設計記述間の差異が比較的小さい場合には、設計規模によらず、形式的な等価性検証が可能であることが示されている。実際の設計現場における等価性検証では、設計を一部修正したものとの等価性検証がほとんどであることから、実用的価値が極めて高い技術であと言える。

第6章は、Equivalence Checking for Loop Optimization without Unrolling (ループの展開をしない等価性検証)であり、等価性検証を行う際、従来技術ではいつも展開していたループ処理に対し、展開せずにそのまま等価性を検証する手法を提案・実装し、評価によってその有効性を実証している。記号シミュレーションは基本的に設計記述を1つずつ評価していくため、ループ処理については、ループを抜けるまでシミュレーションを行う必要があるが、一般にループの終了条件は不定になるケースも多いため、従来はループはすべて展開して等価性検証を行っていた。しかし、ループを回る回数が多い場合に完全に展開してしまうと、展開結果が膨大となり処理不能になってしまう。そこで、一定の条件を満たすループ処理については、提案している新規手法を利用することで、展開せずに等価性が形式的に検証できることを示している。例題への適用から、多くの場合に提案手法が適用できることが示されており、価値の高い検証手法となっている。

第7章は、Tool Implementation and Case Study(ツール実装と例題による評価)と題し、提案している各手法の評価に加え、C言語ベース設計に対する形式的等価性検証ツールとしての評価を行っている。MPEGエンコーダなどの実際的な例題を用いた評価であり、ツールとしての実用性を示している。結果として、この等価性検証ツールは産業界からも注目されており、産業界において実設計での評価を行う段階になっている。

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

以上、本論文はC言語ベースの電子機器に対するシステムレベル設計において、従来ほとんど研究されてこなかった形式的等価性検証手法に関し、実設計記述の特性に着目した新規検証手法を考案・実装し、大規模設計にも適用可能であることを実際的な例題で実証し産業界からも注目されており、電子工学発展に寄与する点は大きい。

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