(57)【要約】【課題】タイミング起因のデッドロック誘発性のあるＦＳＭ記述をＲＴＬ記述中から検出することができる回路検証方法を提供する。【解決手段】レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述からステートマシンを検出し、ステートマシンの複数の状態から、回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出し、非同期信号の変化後の最初のクロックの有効エッジと非同期信号の変化のタイミングに依存して、非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断し、可能性があると判断したとき、検証対象記述にはデッドロックを発生させる可能性があると判断する。【選択図】  図１
2015130104.tif 000002
【特許請求の範囲】
【請求項１】
レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述からステートマシンを検出し、
前記ステートマシンの複数の状態から、前記回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出し、
前記非同期信号の変化後の最初の前記クロックの有効エッジと前記非同期信号の変化のタイミングに依存して、前記非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断し、
前記可能性があると判断したとき、前記検証対象記述にはデッドロックを発生させる可能性があると判断する
ことを特徴とする回路検証方法。
【請求項２】
前記複数の状態中に前記非同期遷移状態を含む前記ステートマシンを、前記状態が列挙型の状態値で定義された列挙型ステートマシン、又は前記状態が定数型の状態値で定義された定数型ステートマシンに分類し、
前記列挙型ステートマシン及び前記定数型ステートマシンの各々の前記状態値の属性として、前記状態値を構成する複数のビットのうち１ビットを除き他のビットが偽であるようにコード化されたエンコード型が指定されているか否かに基づいて、前記可能性を判断する
ことを特徴とする請求項１に記載の回路検証方法。
【請求項３】
前記検証対象記述中で、前記列挙型ステートマシンの状態値の属性として前記エンコード型が指定されていない場合、前記列挙型のステートマシンには前記可能性があると判断する
ことを特徴とする請求項２に記載の回路検証方法。
【請求項４】
前記検証対象記述中で、前記列挙型ステートマシンの状態値の属性として前記エンコード型が指定されている場合、
セーフ又はグレイのいずれかが属性として指定されているときは、前記列挙型のステートマシンには前記可能性があると判断し、
セーフ又はグレイのいずれも属性として指定されていないときは、前記列挙型のステートマシンには前記可能性がないと判断する
ことを特徴とする請求項３に記載の回路検証方法。
【請求項５】
前記検証対象記述中で、前記定数型ステートマシンの状態値の属性として前記エンコード型が属性として指定されている場合、前記定数型のステートマシンには前記可能性があると判断する
ことを特徴とする請求項２に記載の回路検証方法。
【請求項６】
前記定数型ステートマシンの状態値の属性として前記エンコード型が指定されていない場合、
前記列挙型ステートマシンの前記状態値の、前記非同期信号の変化の前後において変化する変化ビットの数に基づき、前記列挙型ステートマシンの前記可能性を判断する
ことを特徴とする請求項５に記載の回路検証方法。
【請求項７】
前記定数型ステートマシンの状態値の属性として前記エンコード型が指定され、かつ前記変化ビットの数が２以上である場合、
前記変化ビットの内の複数のビットの各々を真又は偽と仮定して構成した仮想状態値の全てが、前記ステートマシンの前記状態値に含まれるか否かに基づき、前記列挙型ステートマシンの前記可能性を判断する
ことを特徴とする請求項６に記載の回路検証方法。
【請求項８】
前記ステートマシンの状態が、前記非同期信号の変化前の状態から前記非同期リセットの変化後の状態へ遷移するための条件式が前記検証対象記述に含まれるか否か、及び、
前記条件式に含まれるフリップフロップの出力状態に基づいて、
前記複数の状態に前記非同期遷移状態が含まれるか否かを判断する
ことを特徴とする請求項１乃至７のいずれかに記載の回路検証方法。
【請求項９】
レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述を検証するコンピュータを、
前記検証対象記述からステートマシンを検出する手段と、
前記ステートマシンの複数の状態から、前記回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出する手段と、
前記非同期信号の変化後の最初の前記クロックの有効エッジと前記非同期信号の変化のタイミングに依存して、前記非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断する手段と、
前記可能性があると判断したとき、前記検証対象記述にはデッドロックを発生させる可能性があると判断する手段
として機能させるための回路検証プログラム。
【請求項１０】
請求項９に記載の回路検証プログラムがインストールされ、
前記検証対象記述の前記可能性を判断する
ことを特徴とする回路検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウェア記述言語を用いたディジタル回路の開発支援に関し、特に非同期の信号変化に起因する問題に対応する回路検証方法、及び回路検証プログラムに関する。
【背景技術】
【０００２】
近年、ＬＳＩ（Large Scale Integration）、ＳＯＣ（System-On-a-Chip）、ＦＰＧＡ（Field Programmable Gate Array）等のディジタル回路の開発において、レジスタ−トランスファー・レベル（Register Transfer Level。以下、「ＲＴＬ」という。）のハードウェア記述言語（Hardware Description Language。以下、「ＨＤＬ」という。）が一般的に使用されている。ＨＤＬの代表的なものとして、ＶＨＤＬ（Very high speed integrated circuit ＨＤＬ）、Verilog-ＨＤＬ等がある。以下、ＲＴＬのＨＤＬによって回路が記述されたものを、単に「ＲＴＬ記述」という。本明細書では、主に、ＶＨＤＬを用いたＲＴＬ記述例を示すが、本発明の適用範囲はＲＴＬ記述に用いられる具体的なＨＤＬの種類には限定されない。
【０００３】
ところで、上記のようなディジタル回路には、非同期リセットの解除タイミングにおける信号間のレーシングに起因して、有限ステートマシン（Finite State Machine。以降、「ＦＳＭ」という。）回路のデッドロックが発生することがある。
【０００４】
以降、デッドロックが発生する可能性があることを、「デッドロック誘発性がある」という。そして、信号の変化タイミングによって発生するデッドロックを、「タイミング起因のデッドロック」といい、タイミング起因のデッドロックが発生する可能性があることを、「タイミング起因のデッドロック誘発性がある」という。
【０００５】
「ＦＳＭ」とは、過去の出力及び入力の、状態及び順序に依存する有限の内部状態をもち、内部状態によってその時点の出力が決定される回路をいう。従って、フリップフロップ（Flip-Flop。以下、「Ｆ／Ｆ」という。）も、最も小規模なものとしてＦＳＭに含まれる。
【０００６】
ＥＤＡ（Electronic Design Automation。電子的設計自動化）ツールのベンダーが提供するフロントエンド系ＥＤＡツールには、「ＦＳＭ回路の検出」を行うことができるものがある。特に、最近では、Formal Verification（形式的検証。以下、「Formal検証」という。）が論理検証の方法としてトレンドである。Formal検証は、テストパターンを必要することなく機能検証を行うことが可能であり、その検証精度は設計者のスキルに依存しない。
【０００７】
Formal検証ツールには、静的な「ＦＳＭ回路のデッドロックの検出」が可能なものがある。そのようなツールでは、静的デッドロックの検出機能によって、設計者の意図しない状態遷移に陥り、デバイスが正常に動作しないという問題を回避することができる。さらに、「非同期リセットの検出」を自動的に行い、リセット信号の極性をチェックするFormal検証ツールもある。
【０００８】
図１２は、一般的なFormal検証ツールによるＦＳＭ回路の解析手順を示すフローチャートである。このように、一般的なFormal検証ツールが備えるＦＳＭ回路の解析機能には、大きく分けて２種類ある。一つは、ＦＳＭ回路がＲＴＬ記述上の全ての状態に遷移することができるか否かをチェックする「リーチャビリティ・チェック（Reachability Check）」である。そしてもう一つが、ＦＳＭ回路がある状態に遷移した場合、”論理的に”その状態から抜け出すことができるか否か、すなわち、他の状態に遷移することができるか、をチェックする「デッドロック・チェック（Deadlock Check）」である。現在のFormal検証ツールには、上記の両方の機能を具備するものが多い。
【０００９】
ただし、上記の「デッドロック・チェック」とは、上述した通り、あくまでも”論理的に”当該状態から抜け出せるか否か、すなわち「論理起因のデッドロック」の発生の有無をチェックするのみである。そのため、非同期リセットの解除タイミングと、クロックの有効エッジ（以下、単に「クロック・エッジ」という。）のレーシングのような、タイミング起因のデッドロックを検出することはできない。
【００１０】
「論理起因のデッドロック状態」と「タイミング起因のデッドロック状態」について詳細に説明する。
【００１１】
図１３Ａ、図１３Ｂに、「論理起因のデッドロック状態」が生じるＦＳＭ回路の、ＶＨＤＬによるＲＴＬ記述例（以降、「デザイン１」という。）を示す。
【００１２】
Line68-75には、STATE3の状態が記述されている。デザイン１の記述の場合、NEXT_STATE信号がSTATE3に遷移してしまうと、NEXT_STATE信号はSTATE3の状態から抜け出すことができない。これは、Line68-75に、STATE3から抜け出す「論理的な記述」が存在しないためである。
【００１３】
この問題を改善したＲＴＬ記述例（以降、「デザイン２」という。）を図１４Ａ、図１４Ｂに示す。本記述例では、Line70の記述が変更されている。これにより、NEXT_STATE信号はSTATE3からSTATE1に遷移できるようになり、論理上はデッドロックが起こりえないように見える。実際に、一般的なFormal検証ツールは、デザイン１に対してはデッドロック誘発性を検出することができるが、デザイン２に対してはそれを検出することができない。
【００１４】
ところが、デザイン２は、タイミング起因のデッドロック誘発性がある。その理由は後述する。このように、一般的なFormal検証ツールでは、タイミング起因のデッドロック誘発性を検出することができない。
【００１５】
タイミング起因のデッドロックには、例えば、「非同期リセット解除時のリセット信号とクロック信号のレーシング」により発生するデッドロックがある。すなわち、タイミング起因のデッドロック非同期リセット信号がデアサートされるタイミングとクロック信号のアクティブエッジのタイミングが非常に近いことが原因でデッドロックが発生することがある。
【００１６】
デザイン２がタイミング起因のデッドロックに陥る原因は、非同期リセットの解除タイミングと、ＲＴＬ記述内の状態値のエンコーディング・タイプとの関係にある。「状態値」とは、ＦＳＭの各状態を特定する値で、「状態変数」とも呼ばれる。
【００１７】
図１５に、デザイン２の回路において、非同期にリセットが解除されたとき（以下、「非同期リセット解除時」という。）の、「ＲＴＬ記述設計者が期待する」状態遷移を示すタイミング・チャートを示す。
【００１８】
図１４Ａの記述から明らかなように、デザイン２では、リセット期間中は、図１４ＡのLine34の通り、CURRENT_STATE信号はSTATE0状態を維持する。そして、リセットが解除された次のクロック・エッジ（立ち上がりエッジ）のタイミングで、図１４ＡのLine36、図１４ＢのLine44の通りCURRENT_STATE信号はSTATE1状態に遷移する。以上がＲＴＬ記述設計者が期待する回路の振る舞いである。
【００１９】
しかし、非同期リセットの場合、リセットのアサート／デアサート・タイミングは任意であるため、必ずしも図１５のタイミングでリセットが解除されるとは限らない。
【００２０】
図１６に、デザイン２の回路における、非同期リセット解除時の、解除タイミングとクロック・エッジのタイミングが非常に近い場合の状態遷移を示すタイミング・チャートを示す。図１６の非同期リセットの解除タイミングでは、リセットとクロックとの間でレーシングを起こす可能性がある。
【００２１】
図１４ＡのLine21-25の通り、CURRENT_STATE信号は５ビットのone-hotエンコード・タイプで構成されている。すなわち、デザイン２の記述例で定義されたＦＳＭの状態値は、５ビットである。そのため、図１６のようなリセット解除タイミングの場合、レーシングの影響で５ビット分のＦ／Ｆのすべてが同時にリセット解除されるとは限らない。従って、リセット解除されるＦ／Ｆとリセット解除されないＦ／Ｆが混在する可能性がある。
【００２２】
具体的には、CURRENT_STATE信号は、リセット解除のタイミングで、STATE0（“00001”）→STATE1（“00010”）に変化することが期待される。このとき、CURRENT_STATE信号を構成する５ビットの信号のうち、CURRENT_STATE[4:2]は、値が変化しない(‘0’のまま)ため、レーシングの影響を受けない。なぜなら、これらの信号は、リセット解除の如何によらず、'0'のままであるからである。
【００２３】
CURRENT_STATE[1:0]に関しては、リセット解除後に値が変わることが期待されている（CURRENT_STATE [1]は'0'から'1'へ、 CURRENT_STATE [0]は'1'から'0'へ）。ところが、レーシングの影響で、CURRENT_STATE[1:0]に関しては、リセット解除後の値がどちらになるかは確定しない。つまり、期待した値にならない可能性がある。
【００２４】
ただし、リセット解除後のCURRENT_STATE信号の各ビットが取りうる値の候補を推測することは可能である。
【００２５】
図１７は、図１６の内容に、レーシング発生時のCURRENT_STATE信号が取り得る値、すなわち状態値と、その状態値に対応する遷移後の状態を追記したタイミング・チャートである。
【００２６】
上述の通り、CURRENT_STATE信号がレーシングの影響を受けるのはbit1、bit0の２ビットである。従って、リセット解除タイミングでCURRENT_STATE信号が取り得る状態値は、全部で、ａ）“00001”、ｂ）”00010”、ｃ）”00000”、ｄ）”00011”の４通りであると推測できる。
【００２７】
図１７を用いて、CURRENT_STATE信号がこの４通りのそれぞれの状態値をとった場合について、状態の遷移タイミングと遷移後の状態について検証する。
【００２８】
この結果、デザイン２の回路の、リセット解除時の振る舞いは、CURRENT_STATE信号の値によって以下の通りとなる。
【００２９】
ａ）：当該タイミングの次のクロック・エッジでリセットが解除される。
【００３０】
ｂ）：当該タイミングでリセットが解除される。
【００３１】
ｃ）、ｄ）：その他の状態（設計者によって定義されいない状態）へ遷移する。
【００３２】
このように、CURRENT_STATE信号がａ）、ｂ）の値を取れば、デッドロックは発生しない。
【００３３】
CURRENT_STATE信号が、ｃ）あるいはｄ）の値を取った場合について、さらに詳細に検討する。
【００３４】
図１４ＡのＲＴＬ記述上のLine21-25で定義しているエンコード・リストには、ｃ）、ｄ）の値共に存在しない。すなわち、CURRENT_STATE信号がｃ）、ｄ）の値を取った場合については、設計者が状態を定義していない。
【００３５】
ただし、このＲＴＬ記述の設計者は、CURRENT_STATE信号がｃ）あるいはｄ）の値を取ったとしても、Line41から始まるprocess文の中で、Line84のothers文にジャンプすることを期待している。すなわち、CURRENT_STATE信号が未定義の値になった場合は、CURRENT_STATEはSTATE0に遷移するように、設計者はＲＴＬ記述を作成している。実際に、一般的な論理シミュレータでデザイン２の検証を行うと、期待通りothers文にジャンプするため、デッドロックに陥ることはない。
【００３６】
ところが、実際のデバイスにデザイン２のＲＴＬ記述の回路をインプリするために論理合成ツールを用いた場合、others文によるデッドロックの防止が有効に働かない場合がある。その理由を以下に説明する。
【００３７】
論理合成ツールは、ＲＴＬ記述をゲートレベルのネットリストに変換する。その際に、一般的な論理合成ツールのデフォルト設定では、ＦＳＭ回路と認識されたＲＴＬ記述のothers文は論理合成されず、削除されてしまう。なぜなら、ＦＳＭ回路のothers文の機能をインプリしてしまうと回路規模が非常に大きくなってしまうからである。以上のように、デフォルト設定では、others文の機能はデバイスには実装されない。
【００３８】
そのため、others文で記述された機能をケアするためには、設計者サイドでＲＴＬ記述中にattribute記述を挿入するか、あるいは、論理合成ツール上でothers文をケアするオプションを有効にする必要がある。
【００３９】
設計者がこの措置を怠ってしまうと、図１７を用いて説明したように、CURRENT_STATE信号がｃ）やｄ）の値を取った場合、実デバイス上ではCURRENT_STATE信号が未定義状態になる。そのため、ＦＳＭ回路が、デッドロックに陥ってしまう可能性がある。
【００４０】
非同期信号に起因する問題の検証や、ステートマシンのデッドロックの検出を行うための各種の技術が公開されている。
【００４１】
例えば、非同期回路に起因する障害を回避するために、非同期回路に特徴的な動作をシミュレーションにおいて発生させる技術がある（例えば、特許文献１）。特許文献１の非同期回路検証方法では、非同期動作を行う回路に、シミュレーション段階で遅延を発生させ、非同期回路に起因する障害を発生させる。それにより、非同期回路の動作検証を精度良く行うことができる。
【００４２】
ステートマシンに関するフォーマル検証を効率化する論理回路設計装置もある（例えば、特許文献２）。特許文献２の装置は、ステートマシンの状態数を減らし、フォーマル検証によるデッドロックの検証を効率化する。
【００４３】
あるいは、ステートマシンのデッドロックを検出し、回路の品質を向上させる回路設計の検証方法もある（例えば、特許文献３）。特許文献３の検証方法では、遷移しないステートに遷移している可能性の有無を判断し、デッドロックを検出する。
【先行技術文献】
【特許文献】
【００４４】
【特許文献１】特開２００５−２８４４２６号公報  （第８−９頁、図１）
【特許文献２】特開２００８−３０４９６０号公報  （第５−６頁、図２−３）
【特許文献３】特開２０１１−１３４２４２号公報  （第４−５頁、図２）
【発明の概要】
【発明が解決しようとする課題】
【００４５】
特許文献１−３の技術には、タイミング起因のデッドロック誘発性がある記述を、検証対象のＲＴＬ記述中から検出することができないという問題がある。
【００４６】
特許文献１の非同期回路検証方法では、非同期回路に起因する障害を、対象回路のシミュレーションにおいて発生させる。つまり、シミュレーションを行わなければ、非同期回路の検証を行うことができない。一般的に、開発の効率化のためには、後戻り工数を極力少なくすることが望ましく、回路の検証は、極力、開発の上流段階で行うことが望まれる。ところが、特許文献１の方法には、ＲＴＬ記述段階での検証には対応できないという問題がある。
【００４７】
特許文献２の論理回路設計装置や特許文献３の検証方法では、時間の概念のない検証を行う。ところが、上記のように、ＲＴＬ記述には、論理的には正しく、同期回路では問題が発生しなくても、非同期信号に対してはデッドロックが発生する記述が含まれることがある。従って、特許文献２、３の技術では、タイミング起因のデッドロック発生の有無を検証することにはできない。
【００４８】
以上のように、特許文献１−３の技術では、タイミング起因のデッドロック誘発性がある記述を、検証対象のＲＴＬ記述中から検出することができない。
【００４９】
タイミング起因でデッドロックに陥ってしまうようなＦＳＭの記述を、ＲＴＬ記述中から自動的に検出することができない場合、設計者自身が、実装したデバイスの振る舞いからこの問題を探し出すといった方法が考えられる。ところが、この方法では非常に長い開発ＴＡＴ（Turn Around Time。所要時間）を要し、開発費用もかさんでしまう。
【００５０】
そのため、ＲＴＬのコーディングスタイルをマニュアル化し、設計者がそのマニュアルに従って回路を設計するという設計手法で回避することもある。しかし、この方法でも、デッドロック誘発性の回避のための対策が設計者のスキルに依存し、コーディングの品質にバラつきが出るという問題がある。
【００５１】
そこで、本来は、タイミング起因のデッドロック誘発性がある記述を検証ツールを用いてＲＴＬ記述中から発見できることが望ましいが、特許文献１−３の技術はそのような要求に対応することができない。
（発明の目的）
本発明は上記のような技術的課題に鑑みて行われたもので、タイミング起因のデッドロック誘発性のあるＦＳＭ記述をＲＴＬ記述中から検出することができる回路検証方法、及び回路検証プログラムを提供することを目的とする。
【課題を解決するための手段】
【００５２】
本発明の回路検証方法は、レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述からステートマシンを検出し、ステートマシンの複数の状態から、回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出し、非同期信号の変化後の最初のクロックの有効エッジと非同期信号の変化のタイミングに依存して、非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断し、可能性があると判断したとき、検証対象記述にはデッドロックを発生させる可能性があると判断することを特徴とする。
【００５３】
本発明の回路検証プログラムは、レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述を検証するコンピュータを、検証対象記述からステートマシンを検出する手段と、ステートマシンの複数の状態から、回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出する手段と、非同期信号の変化後の最初のクロックの有効エッジと非同期信号の変化のタイミングに依存して、非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断する手段と、可能性があると判断したとき、検証対象記述にはデッドロックを発生させる可能性があると判断する手段として機能させることを特徴とする。
【発明の効果】
【００５４】
本発明の回路検証方法、及び回路検証プログラムは、タイミング起因のデッドロック誘発性のあるＦＳＭ記述をＲＴＬ記述中から検出することができるという効果がある。
【図面の簡単な説明】
【００５５】
【図１】本発明の回路検証方法の処理手順を示すフローチャートである。
【図２】本発明の回路検証機能が追加されたFormal検証ツールによるＦＳＭ回路の解析手順を示すフローチャートである。
【図３Ａ】本実施形態の回路検証方法の処理手順の、詳細なアルゴリズムの例を示すフローチャートの前半部である。
【図３Ｂ】本実施形態の回路検証方法の処理手順の、詳細なアルゴリズムの例を示すフローチャートの後半部である。
【図４】非同期のリセット入力をもつＦＳＭ回路の構成例を示すブロック図である。
【図５】同期化されたリセット入力をもつＦＳＭ回路の構成例を示すブロック図である。
【図６】エンコード・タイプのアトリビュート宣言が記載されたＦＳＭのＲＴＬ記述例である。
【図７Ａ】本発明の回路検証方法における、デッドロック誘発性の有無を判断する論理展開を示すための、エンコーディング・デザイン例である。
【図７Ｂ】本発明の回路検証方法における、第１のエンコーディング・デザインの場合の、デッドロック誘発性の有無を判断する手順を示すフローチャートである。
【図７Ｃ】本発明の回路検証方法における、第２のエンコーディング・デザインの場合の、デッドロック誘発性の有無を判断する手順を示すフローチャートのである。
【図８】エンコード・タイプのアトリビュート宣言に加え、アトリビュート定義が記載されたＦＳＭのＲＴＬ記述例である。
【図９Ａ】本発明の回路検証方法における、リセット解除後の最初のクロック・エッジでの状態遷移の有無を判断する手順を示すフローチャートの前半部である。
【図９Ｂ】本発明の回路検証方法における、リセット解除後の最初のクロック・エッジでの状態遷移の有無を判断する手順を示すフローチャートの後半部である。
【図１０Ａ】図１４Ａ、図１４Ｂ（デザイン２）のＦＳＭ回路のＲＴＬ記述に、リセット解除状態へ遷移するための条件式を追加した第１のＲＴＬ記述例（デザイン３）の前半部である。
【図１０Ｂ】デザイン３の中間部である。
【図１０Ｃ】デザイン３の後半部である。
【図１１Ａ】デザイン２のＦＳＭ回路のＲＴＬ記述に、リセット解除状態へ遷移するための条件式を追加した第２のＲＴＬ記述例（デザイン４）の前半部である。
【図１１Ｂ】デザイン４の中間部である。
【図１１Ｃ】デザイン４の後半部である。
【図１２】一般的なFormal検証ツールによるＦＳＭ回路の解析手順を示すフローチャートである。
【図１３Ａ】論理起因のデッドロック状態が生じるＦＳＭ回路のＲＴＬ記述例（デザイン１）の前半部である。
【図１３Ｂ】デザイン１の後半部である。
【図１４Ａ】タイミング起因のデッドロック状態が生じる可能性があるＦＳＭ回路のＲＴＬ記述例（デザイン２）の前半部である。
【図１４Ｂ】デザイン２の後半部である。
【図１５】非同期リセット解除時に期待される状態遷移を示すタイミング・チャートである。
【図１６】非同期リセット解除によるレーシング発生時の状態遷移を示すタイミング・チャートである。
【図１７】非同期リセット解除によるレーシング発生時の、遷移後に取り得る状態値とその状態値に対応する遷移後の状態を示すタイミング・チャートである。
【発明を実施するための形態】
【００５６】
本発明の実施形態について、詳細に説明する。図１は、本発明の回路検証方法の処理手順を示すフローチャートである。
【００５７】
本発明の回路検証方法の処理手順では、初めに、レジスタ−トランスファー・レベルのハードウェア記述言語を用いて回路が記述された検証対象記述からステートマシンを検出する（ステップＳ１）。
【００５８】
次に、前記ステートマシンの複数の状態から、前記回路の動作を同期させるクロックに対して非同期に変化する非同期信号を使用して遷移条件が定義された非同期遷移状態を検出する（ステップＳ２）。
【００５９】
そして、前記非同期信号の変化後の最初の前記クロックの有効エッジと前記非同期信号の変化のタイミングに依存して、前記非同期遷移状態から、定義されていない非定義状態遷移へ遷移する可能性の有無を判断する（ステップＳ３）。
【００６０】
最後に、前記可能性があると判断したとき、前記検証対象記述にはデッドロックを発生させる可能性があると判断する（ステップＳ４）。
【００６１】
図２は、図１２のFormal検証ツールに、本発明の回路検証手順が追加されたときの解析手順を示すフローチャートである。
【００６２】
本実施形態の回路検証方法では、図１２の一般的なFormal検証ツールの機能である「リーチャビリティ・チェック」、「デッドロック・チェック」に、本発明の回路検証方法を用いた「レーシング・デッドロック・チェック（Racing Deadlock Check）」が追加されている。レーシング・デッドロック・チェックでは、ＲＴＬ記述のソースファイルを入力情報とし、非同期リセット解除時のレーシングが原因でデッドロックになる可能性、すなわち、デッドロック誘発性のあるＦＳＭ回路を検出する。
【００６３】
レーシング・デッドロック・チェックの処理手順の概要は以下の通りである。
１）ＲＴＬ記述から非同期リセット付きＦＳＭ回路の記述を検出する。
【００６４】
本処理は、一般的なFormal検証ツールの機能で実現することができる。
２）１）のリセット解除前後の状態遷移を把握する。
３）２）の状態遷移がリセット解除時のレーシングでどのように変化するかを推測する。
４）３）で推測された全ての状態遷移が、ＲＴＬ記述の条件分岐に記載されているか否かをチェックする。
５）条件分岐に記載されていない状態遷移が見つかった場合、対象ＲＴＬ記述はデッドロックに誘発性があると判断する。
【００６５】
本発明では、これらのプログラムを設計する際に必要なFormal検証ツールのアルゴリズムを提供する。
【００６６】
図３Ａ、図３Ｂは、本実施形態の回路検証方法の処理手順の、詳細なアルゴリズムの例を示すフローチャートである。具体的には、図３Ａ、図３Ｂは、検証対象のＲＴＬ記述内に、非同期リセットが解除されたときにレーシングによりデッドロックが発生するＦＳＭ回路が存在するか否かを検証するアルゴリズムを示す。以下に、本実施形態の回路検証方法の処理手順を説明する。
（ステップＳ０１）
初めに、ＲＴＬ記述中からＦＳＭ回路を検出する。
（ステップＳ０２）
検出されたＦＳＭ回路が非同期リセットを使用しているかどうかをチェックする。本処理は、処理対象のＲＴＬ記述に使用されている言語により具体的なチェック方法が異なる。
【００６７】
代表的なＲＴＬ記述用言語である、ＶＨＤＬ、Verilog-ＨＤＬの場合については以下の通りである。
ａ）ＶＨＤＬの場合
以下の（１）〜（３）が全て成り立つことをチェックする。
【００６８】
（ｉ）当該process文の引数に複数の信号が定義されている
（ii）process宣言直後のif文にevent文が来ない
（iii）（ii）の後のelsif文でevent文が宣言されている
ｂ）Verilog-ＨＤＬの場合
以下が成り立つことをチェックする。
【００６９】
（ｉ）当該always文の引数に複数の信号が定義されている
ただし、ａ）、ｂ）の場合ともに、ステップＳ２の処理では、既存のFormal検証ツール等を用いて、クロック、リセットのバック・トレースを行い、当該リセットが当該クロックに同期していないことを確認する必要がある。
【００７０】
例えば、図４のような構成のＦＳＭ回路１０１が、図１４Ａ、図１４Ｂのデザイン２のＲＴＬ記述で定義されている場合、ＦＳＭ回路１０１に入力されるクロック、リセットはそのまま外部入力となっている。そのため、リセット解除のタイミングはクロックに同期していないと考えてよい。従って、ＦＳＭ回路１０１は、一旦、検証対象の候補となる。
【００７１】
ところが、図５のように、図４のＦＳＭ回路１０１の外部にシンクロナイザ１０２を備える場合、ＦＳＭ回路１０１に入力されるリセットは、上位階層のシンクロナイザ１０２から出力された信号である。シンクロナイザ１０２は、非同期リセットの解除タイミングを当該クロックに同期させる機能を有する（Ｓ０２：Ｎｏ）。そのため、このような回路が付加されている場合は非同期のリセット解除タイミングでレーシングが発生することがなく、ＦＳＭ回路１０１はデッドロックに陥ることがない。従って、この場合、ＦＳＭ回路１０１は、以降の検証対象から除外される。
【００７２】
当然ながら、リセットを同期化する回路が付加されていないとき（Ｓ０２：Ｙｅｓ）は、ＦＳＭ回路１０１は、以降の検証処理の対象となる。
（ステップＳ０３）
リセット解除後の最初のクロック・エッジで状態遷移が発生するか否かをチェックする。具体的には、図９Ａ、図９Ｂに示された手順でチェックを実施する。詳細な説明は後述する。
（ステップＳ０４）
ＦＳＭ回路の各状態が、列挙型の状態変数を用いて記述されているか、定数型の状態変数を用いて記述されているかをチェックする。以降、各状態が、列挙型の状態値を用いて記述されているＦＳＭを「列挙型ＦＳＭ」、定数型の状態値を用いて記述されているＦＳＭを「定数型ＦＳＭ」という。
【００７３】
以下の処理は、ＲＴＬ記述に含まれるＦＳＭが列挙型ＦＳＭか、定数型ＦＳＭかによって異なる。以下に、ＦＳＭの型ごとに検証方法を説明する。対象ＦＳＭが列挙型ＦＳＭである場合は、図３ＡのステップＳ１１へ進む。対象ＦＳＭ回路が定数型ＦＳＭである場合は、図３Ｂに示した「定数型ＦＳＭ用処理」のステップＳ２１へ進む。定数型ＦＳＭ用処理については後述する。
（１）列挙型ＦＳＭの場合
（ステップＳ１１）
当該ＦＳＭが列挙型ＦＳＭの場合、ＲＴＬ上で状態値のアトリビュート（属性）としてエンコード・タイプが宣言されているか否かをチェックする。具体的には、ＲＴＬ上のattribute記述の有無を確認する。
【００７４】
当該記述がない場合（Ｓ１１：Ｎｏ）、状態値をどのようなエンコード・タイプのアトリビュートとして回路が合成されるかは論理合成ツールに依存するため、「当該ＦＳＭ回路はデッドロック誘発性がある」と判断される。
【００７５】
図６のＲＴＬ記述例の場合、Line27にエンコード・タイプとして”one-hot”が宣言されている。このように、ＲＴＬ上で状態値のアトリビュート（属性）としてエンコード・タイプが宣言されている場合（Ｓ１１：Ｙｅｓ）、この時点では、当該ＦＳＭ回路はデッドロック誘発性があるとは判断されない。
（ステップＳ１２）
ステップＳ１１のattribute記述の内容をチェックする。
ａ）エンコード・タイプに”gray”（グレイ・コード）が宣言されている場合
この場合は、「当該ＦＳＭ回路はデッドロック誘発性がない」と判断する。
【００７６】
そのように判断することができる理由を図７Ａ、図７Ｂ、図７Ｃに示す。詳細な説明は、図中に示したため、ここでの説明は省略する。結論としては、状態値がグレイ・コードである場合、状態値の各ビットの内、レーシングの影響を受けるビットは１ビットのみである。従って、この場合は、デッドロックを起こすことはない。
ｂ）”safe”（Safe State Machine）が宣言されている場合
この場合、ＦＳＭ回路のothers／default文の記述は、論理合成時に回路に実装されるため、やはり「当該ＦＳＭ回路はデッドロック誘発性がない」と判断される。
ｃ）”gray”、”safe”以外のエンコード・タイプが宣言されている場合
”gray”、”safe”以外のエンコード・タイプがattributeで宣言されている場合は、デッドロックを起こす可能性がある。例えば、図６のＲＴＬ記述の場合、エンコード・タイプとして”one-hot”と宣言されており、図１４Ａ、図１４Ｂ（デザイン２）と同様のエンコード・タイプであるため、「当該ＦＳＭ回路はデッドロック誘発性がある」と判断される。
（２）定数型ＦＳＭ回路の場合
（ステップＳ２１）
図３ＡのＳ０４の判定で、当該ＦＳＭが定数型ＦＳＭであると判断された場合、初めにアトリビュートとしてエンコード・タイプがＲＴＬ上で宣言されているか否かをチェックする。
【００７７】
本来、定数型でエンコード（ビット・アサイン）が宣言されているときはattributeは不要である。それにも関わらず、図８のように、あえてアトリビュート定義が記載されている場合（Ｓ２１：Ｙｅｓ）は、論理合成ツールによっては定数型のエンコード記述を無視してattributeを優先することがある。
【００７８】
そのため、この場合は、エンコード・タイプによらずデッドロックを起こす可能性があるものとみなし、「当該ＦＳＭ回路はデッドロック誘発性がある」と判断する。
（ステップＳ２２）
リセット期間中の状態値とリセット解除後の状態値の各ビットの排他的論理和を取る。図１４Ａ、図１４Ｂ（デザイン２）のＲＴＬ記述の場合、
リセット期間中：STATE0（“00001”）
リセット解除後：STATE1（“00010”）
となることから、STATE0 とSTATE1のビットごとの排他的論理和（EXOR_VALUE）は
EXOR_VALUE ＝ “00011”
となる。
（ステップＳ２３）
EXOR_VALUEの各ビットで、’1’が立っているビットの総数を数える。デザイン２の場合、’1’が立っているビットの総数（HIGH_BIT_COUNT）は、
HIGH_BIT_COUNT ＝ 2
となる（EXOR_VALUEのbit0とbit1に’1’が立っているため）。
（ステップＳ２４）
HIGH_BIT_COUNTが２以上かどうかをチェックする。
【００７９】
HIGH_BIT_COUNTが１以下であれば（Ｓ２４：Ｎｏ）、「当該ＦＳＭ回路はデッドロック誘発性がない」と判断する。
【００８０】
その理由を図７Ｃに示す。Ｓ１２の処理における図７Ｂについての説明と同様に、結論としては、レーシングの影響を受けるのが１ビット分の場合、デッドロックを起こさない。
【００８１】
HIGH_BIT_COUNTが２以上であれば（Ｓ２４：Ｙｅｓ）、この時点では、当該ＦＳＭ回路はデッドロック誘発性がないとは判断されない。
（ステップＳ２５）
EXOR_VALUEに’1’が立っているビットに対して、’0’及び’1’の両方の値を取り得る場合のEXOR_VALUEの値を推測し、メモリ上に格納する。図１４Ａ、図１４Ｂ（デザイン２）のＲＴＬ記述の場合、EXOR_VALUEは以下の４通りの値を取り得るので、これらをメモリ領域（ARRAY_EXOR_VALUE）上に格納する。
【００８２】
EXOR_VALUE ＝ “00001”
“00010”
“00000”
“00011”
（ステップＳ２６）
メモリ領域ARRAY_EXOR_VALUEからEXOR_VALUEを順番に取り出す。取り出した値をtmp_EXOR_VALUEとする。
（ステップＳ２７）
tmp_EXOR_VALUE値が、ＲＴＬ記述上のＦＳＭ回路内のcase文の条件分岐に記述されているか否かをチェックする。
【００８３】
以上のように、tmp_EXOR_VALUE値が、ＲＴＬ記述上のＦＳＭ回路内のcase文の条件分岐に記述されていない場合（Ｓ２７：Ｙｅｓ）は、「当該ＦＳＭ回路はデッドロック誘発性がある」と判断される。tmp_EXOR_VALUE値が、ＲＴＬ記述上のＦＳＭ回路内のcase文の条件分岐に記述されている場合（Ｓ２７：Ｎｏ）は、次の処理へ移る。
（ステップＳ２８）
Ｓ２７での検査対象のtmp_EXOR_VALUE値が、ARRAY_EXOR_VALUEから取り出した最後のデータであるか否かを確認する。
【００８４】
検査対象のtmp_EXOR_VALUE値が、ARRAY_EXOR_VALUEから取り出した最後のデータである（Ｓ２８：Ｙｅｓ）ことは、Ｓ２５で格納された全てのtmp_EXOR_VALUE値が、ＲＴＬ記述内の条件分岐に記述されていることを意味する。この場合、状態はothers文へもdefault文へも遷移する可能性がないため、「当該ＦＳＭ回路はデッドロック誘発性がない」と判断される。
【００８５】
検査対象のtmp_EXOR_VALUE値が、ARRAY_EXOR_VALUEから取り出した最後のデータでない場合（Ｓ２８：Ｎｏ）は、Ｓ２７の処理へ戻る。
【００８６】
以上のように、Ｓ２７、Ｓ２８は、全てのtmp_EXOR_VALUE値がＦＳＭ回路内のcase文の条件分岐に記述されているか、あるいは、ＦＳＭ回路内のcase文の条件分岐に記述されていないtmp_EXOR_VALUE値があるかをチェックする処理である。
【００８７】
Ｓ２５で格納されたtmp_EXOR_VALUE値に、１つでもＲＴＬ記述内の条件分岐に記述されていない場合（Ｓ２７：Ｙｅｓ）は、「当該ＦＳＭ回路はデッドロック誘発性がある」と判断される
図１４Ａ、図１４Ｂ（デザイン２）の場合について、上記のEXOR_VALUEの４つの値を上から順に、メモリ領域ARRAY_EXOR_VALUEから取り出したときの、Ｓ２７、Ｓ２８の処理は以下の通りである。なお、Line番号は図１４Ａ、図１４ＢのＲＴＬ記述における行番号である。
１）tmp_EXOR_VALUE ＝ “00001”を読み出す
そして、Line43に、STATE0=”00001”との記述を確認する（Ｓ２７：Ｎｏ）。２）tmp_EXOR_VALUE ＝ “00010”を読み出す
そして、Line46に、STATE1=”00010”との記述を確認する（Ｓ２７：Ｎｏ）。
３）tmp_EXOR_VALUE ＝ “00000”を読み出す
このとき、図１４Ａ、図１４ＢのＲＴＬ記述中にはSTATE1=”00000”との記述がない（Ｓ２７：Ｙｅｓ）ので、ＲＴＬ記述としては、状態はothers文の定義箇所に遷移することになる。
【００８８】
状態がothers文の定義箇所に遷移する可能性があることが判明したので、「当該ＦＳＭ回路はデッドロック誘発性がある」との旨をレポートし、処理を終了する。
【００８９】
図７Ｃに、上記のＳ２２〜Ｓ２８の処理内容をさらに詳細に示す。詳細な説明は、図中に示したため、ここでの説明は省略する。
【００９０】
次に、前述の図３ＡのＳ０３の処理である、「リセット解除後の最初のクロック・エッジでの状態遷移の有無の判断」の手順について説明する。
【００９１】
図９Ａ、図９Ｂは、上記判断手順の例を示すフローチャートである。以下に、処理対象のＲＴＬ記述として、図１４Ａ、図１４ＢのＲＴＬ記述（デザイン２）、及びデザイン２のＲＴＬ記述に条件式を追加した、図１０Ａ、図１０Ｂ、図１０ＣのＲＴＬ記述（デザイン３）、図１１Ａ、図１１Ｂ、図１１ＣのＲＴＬ記述（デザイン４）を用いて、処理手順を順に説明する。
（１）デザイン２の場合
（ステップＳ３１）
ＲＴＬ記述に、リセット解除後（クロック・エッジ発生後）に、リセット解除状態へ遷移するための条件式（以降、単に「条件式」という。）があるか否かを判断する。
【００９２】
デザイン２では、Line43-44に条件式がない（Ｓ３１：Ｎｏ）。従って、リセット解除後の最初のクロック・エッジで無条件にSTATE1に遷移すると判断し、処理を終了する。
【００９３】
この場合は、図１７を用いて説明した理由により、「当該ＦＳＭ回路はデッドロック誘発性がある」可能性があると判断し、図３ＡのＳ０４の処理へ移る。
（２）デザイン３の場合
（ステップＳ３１）
デザイン３の場合、Line44に条件文がある（Ｓ３１：Ｙｅｓ））ので、次の処理に移る。
（ステップＳ３２）
条件式にＦ／Ｆの出力信号が含まれるか否かを判断する。
デザイン３の場合、Line44の条件式の要素には、入力信号であるINDATA信号は含まれるが、Ｆ／Ｆの出力信号は含まれない（Ｓ３２：Ｎｏ）。
（ステップＳ３６）
INDATA信号は外部から入力されるため、INDATA=’1’となるタイミングは不明である。そのため、アルゴリズム的には非同期リセット解除タイミングでINDATA=’1’となる可能性がある。従って、「当該ＦＳＭ回路はデッドロック誘発性がある」可能性があると判断する。そのため、図３ＡのＳ０４の処理へ移る。
（３）デザイン４の場合
（ステップＳ３１）
デザイン４の場合、Line44に条件文がある（Ｓ３１：Ｙｅｓ））ので、次の処理に移る。
（ステップＳ３２）
デザイン４の場合、Line44の条件式の要素であるINDATA信号は入力端子、cnt信号はＦ／Ｆ出力信号であり、条件式にＦ／Ｆの出力信号が含まれる（ステップＳ３２：Ｙｅｓ）。
（ステップＳ３３）
条件式の要素がＦ／Ｆの出力信号のみであるか否かを判断する。
【００９４】
デザイン４の場合、条件式にＦ／Ｆの出力信号以外にINDATA信号が含まれる（ステップＳ３３：Ｎｏ）。
【００９５】
条件式の要素がＦ／Ｆの出力信号のみである場合（ステップＳ３３：Ｙｅｓ）は、後述のステップＳ３８の処理へ移る。
（ステップＳ３４）
Ｆ／Ｆ出力信号が偽であると仮定したとき、Ｆ／Ｆ出力信号以外の要素の真偽に関わらず、条件式が必ず偽になるか否かを判断する。
【００９６】
デザイン４の場合、Line44にある「cnt=”100”」が偽であると仮定した場合、Line44の条件式はINDATA信号がどのような値をとっても必ず偽となる（ステップＳ３４：Ｙｅｓ）。
（ステップＳ３７）
非同期リセット解除のタイミングでの条件式の真偽は、Ｆ／Ｆ出力信号の論理によって決まると判断する。
【００９７】
この判断は、デザイン４の場合では、cnt信号が非同期リセット解除タイミングで取る値にのみ依存し、INDATA信号には依存せず、Line44の条件式の真偽が決定されることを意味する。
【００９８】
この場合、以降、Ｆ／Ｆ出力信号以外の要素（デザイン４の場合はcnt信号）が非同期リセット解除タイミングでどのような値を取り得るかを検証する。
（ステップＳ３８）
Ｆ／Ｆ出力信号の生成論理に、非同期リセット時の値が存在するか否かを判断する。
【００９９】
デザイン４の場合では、cnt信号のＦ／Ｆが非同期リセット付きＦ／Ｆかどうかをチェックする。これは非同期リセット時の値が確定するか否かを確認する必要があるためである。
【０１００】
もし値が確定しなければ（ステップＳ３８：Ｎｏ）、リセット解除時のcnt信号の値は不定（‘Ｘ’）となることから、１／０どちらも取り得るため図１１ＢのLine44の条件式は真となる可能性があると判断する。従って、「当該ＦＳＭ回路はデッドロック誘発性がある」可能性があると判断し、図３ＡのＳ０４の処理へ移る。
【０１０１】
しかし、デザイン４の場合では、Line96の通り、cnt信号のＦ／Ｆは非同期リセット付きＦ／Ｆである（ステップＳ３８：Ｙｅｓ）ため、次の処理に移る。
（ステップＳ３９）
Ｆ／Ｆ出力信号の非同期リセット時の値と、条件式が真になるためのＦ／Ｆ出力信号の値が一致するか否かを判断する。
【０１０２】
デザイン４の場合では、cnt信号のリセット初期値を確認する。Line97にある通り、cnt信号のリセット初期値は”000”である。この値は、Line44の条件式が真になるための値である「cnt=”100”」とは一致しない（ステップＳ３９：Ｙｅｓ）。つまり、リセット解除タイミングにおいてcnt信号は”000”であることから、このタイミングで図１１ＢのLine44の条件式は常に偽となる。よって、このタイミングで状態がSTATE0→STATE1に遷移することはないことがわかるので、「当該ＦＳＭ回路はデッドロック誘発性がない」と判断する。
【０１０３】
もし、仮にデザイン４のLine44の条件式が「INDATA = '1' and cnt = "000"」と記述されていたならば、Ｓ３９の判定結果は偽となる（ステップＳ３９：Ｎｏ）。つまり、リセット解除タイミングにおいて、状態は必ずSTATE0→STATE1に遷移すると判断する。従って、「当該ＦＳＭ回路はデッドロック誘発性がある」可能性があると判断し、図３ＡのＳ０４の処理へ移る。
【０１０４】
なお、上記の実施形態では、非同期リセットの解除時の振る舞いを例として説明したが、リセット以外の非同期な信号に対する状態遷移が定義されたＦＳＭについても、同様に処理することができる。すなわち、上記の非同期リセット解除を、非同期信号の変化に置き換えて考えればよい。
（実施形態の効果）
本実施形態の回路検証方法によると、検証対象のＲＴＬ記述に含まれる、非同期な信号変化によって非定義な状態へ遷移するＦＳＭの記述を検出する。
【０１０５】
従って、非同期な信号変化時、例えば、非同期リセット解除タイミングのレーシングによるＦＳＭ回路のデッドロック不具合を、フロントエンド設計フェース、しかもＲＴＬシミュレーション以前で検出することができる。
【０１０６】
上記の不具合は、これまでは実機評価の段階又はゲート・シミュレーションの段階でしか見つけることができなかったので、後工程でのデバッグにかかる時間を大幅に短縮することができる（ＴＡＴ改善）という効果がある。
【０１０７】
また、フロント・ローディングの観点から、前工程での品質が改善される（品質向上）という効果もある。
【０１０８】
本実施形態の各フローチャートに示された処理を実行する主体は限定されない。各処理制御は、ハードウェアによって実行されてもよい。あるいは、ＣＰＵ（Central Processing Unit）（図示なし）を備える装置を回路検証装置として使用し、そのＣＰＵが所定の記憶手段（図示なし）から検証プログラムを読み込んで実行することによって、処理が行われてもよい。
【０１０９】
なお、本プログラムは、ＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）、フラッシュメモリ等の半導体記憶装置、あるいは光ディスク、磁気ディスク、光磁気ディスク等、非一時的な媒体に格納されてもよい。
【産業上の利用可能性】
【０１１０】
本発明の回路検証方法は、ＲＴＬ設計を行う半導体デバイスの開発全般において適用することができる。
【０１１１】
また、本発明の回路検証方法を用いる検証手段は、Formal検証用ツール等、半導体デバイス開発用のＥＤＡツールのプログラムに実装されてもよい。すなわち、図２のように、図１２のような一般的なFormal検証ツールに追加される形で実装されてもよい。あるいは、単独のＥＤＡツールとして実現されてもよい。
【符号の説明】
【０１１２】
１０１    有限ステートマシン（ＦＳＭ）
１０２    シンクロナイザ
【図１】
2015130104.tif 000003
【図２】
2015130104.tif 000004
【図３Ａ】
2015130104.tif 000005
【図３Ｂ】
2015130104.tif 000006
【図４】
2015130104.tif 000007
【図５】
2015130104.tif 000008
【図６】
2015130104.tif 000009
【図７Ａ】
2015130104.tif 000010
【図７Ｂ】
2015130104.tif 000011
【図７Ｃ】
2015130104.tif 000012
【図８】
2015130104.tif 000013
【図９Ａ】
2015130104.tif 000014
【図９Ｂ】
2015130104.tif 000015
【図１０Ａ】
2015130104.tif 000016
【図１０Ｂ】
2015130104.tif 000017
【図１０Ｃ】
2015130104.tif 000018
【図１１Ａ】
2015130104.tif 000019
【図１１Ｂ】
2015130104.tif 000020
【図１１Ｃ】
2015130104.tif 000021
【図１２】
2015130104.tif 000022
【図１３Ａ】
2015130104.tif 000023
【図１３Ｂ】
2015130104.tif 000024
【図１４Ａ】
2015130104.tif 000025
【図１４Ｂ】
2015130104.tif 000026
【図１５】
2015130104.tif 000027
【図１６】
2015130104.tif 000028
【図１７】
2015130104.tif 000029