(57)【要約】      （修正有）【課題】回路検証に関する不都合、問題点あるいはその両方を軽減または解消する回路のための有向ファルシフィケーション方法、論理及びシステムを提供する。【解決手段】回路の有向ファルシフィケーションのための方法は、前記回路の状態空間の１以上の分割を選択するステップ１００を有する。前記分割は前記状態空間の一部のみを有し、前記回路の１以上の特性を示す１以上のプリイメージ計算に従って選択される。前記特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す。本方法はさらに、前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップ１０２を有する。【選択図】図２
2005182766.tif 000002
【特許請求の範囲】
【請求項１】
回路の有向ファルシフィケーションのための方法であって、
前記回路の状態空間の１以上の分割を選択するステップと、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップと、
から構成され、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とする方法。
【請求項２】
請求項１記載の方法であって、
前記ファルシフィケーションベース順方向到達可能性技術による１以上の分割の分析は、前記１以上の分割における幅優先探索（ＢＦＳ）を実行することからなることを特徴とする方法。
【請求項３】
請求項１記載の方法であって、さらに、
前記回路の状態空間の複数の分割を選択するステップと、
前記複数の分割の何れかが前記回路において１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って、互いに独立な前記複数の分割のそれぞれをパラレルに分析するため、１以上のＰＯＢＤＤを利用するステップと、
を有することを特徴とする方法。
【請求項４】
請求項１記載の方法であって、
前記回路の状態空間の１以上の選択された分割は、前記１以上の分割の分析が前記１以上の分割における１以上の深い状態に到達することを可能にするサイズを有することを特徴とする方法。
【請求項５】
請求項１記載の方法であって、
２つのプロセッサから構成される中央演算ユニット（ＣＰＵ）は、前記１以上の分割が前記回路における１以上のエラーを有するか判断するため、前記ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割の分析を実行することを特徴とする方法。
【請求項６】
回路の有向ファルシフィケーションのための論理であって、該論理はコンピュータ実行可能な媒体に符号化され、実行時に、
前記回路の状態空間の１以上の分割を選択するステップと、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップと、
を処理可能であり、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とする論理。
【請求項７】
請求項６記載の論理であって、さらに、
前記ファルシフィケーションベース順方向到達可能性技術による１以上の分割の分析するため、前記１以上の分割において幅優先探索（ＢＦＳ）を実行するステップを、
処理可能であることを特徴とする論理。
【請求項８】
請求項６記載の論理であって、さらに、
前記回路の状態空間の複数の分割を選択するステップと、
前記複数の分割の何れかが前記回路において１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って、互いに独立な前記複数の分割のそれぞれをパラレルに分析するため、１以上のＰＯＢＤＤを利用するステップと、
を処理可能であることを特徴とする論理。
【請求項９】
請求項６記載の論理であって、
前記回路の状態空間の１以上の選択された分割は、前記１以上の分割の分析が前記１以上の分割における１以上の深い状態に到達することを可能にするサイズを有することを特徴とする論理。
【請求項１０】
回路の有向ファルシフィケーションのためのシステムであって、
前記回路の状態空間の１以上の分割を選択する手段と、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用する手段と、
から構成され、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とするシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本開示は、一般に回路検証に関し、より詳細には回路の有向ファルシフィケーションに関する。
【背景技術】
【０００２】
ハードウェアの設計におけるエラー検出は、二分決定図（ＢＤＤ）に基づく探索をしばしば必要とする困難な問題である。しかしながら、現在のｂｄｄアプローチは、典型的には、不安定あるいは非効率なものである。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明は、回路検証に関する不都合、問題点あるいはその両方を軽減または解消するものである。
【課題を解決するための手段】
【０００４】
一実施例では、回路の有向ファルシフィケーションのための方法は、前記回路の状態空間の１以上の分割を選択するステップを有する。前記分割は前記状態空間の一部のみを有し、前記回路の１以上の特性を示す１以上のプリイメージ計算に従って選択される。前記特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す。本方法はさらに、前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップを有する。
【０００５】
本発明のある実施例は、１以上の技術上の効果を提供するかもしれない。一例として、ある実施例は、パラレルな枠組みにおいて状態空間分割を利用する。ある実施例では、複数のファルシフィケーションアルゴリズムが、互いに異なるサーチパスを探索するため、互いの試行から独立してパラレルに実行される。ある実施例は、分割から生じる潜在的なコンパクト性を十分活用し、回路におけるエラーを検出するため、ＢＤＤを利用するパフォーマンス特性における変動を取り除く傾向がある。ある実施例では、パラレルなファルシフィケーションは、典型的に逐次的ファルシフィケーションにおいてボトルネックとなる分割スケジューリングを回避する。ある実施例は、従来及び分割ＢＤＤに対するかなりのパフォーマンスのゲインを生成する。
【発明の効果】
【０００６】
本発明によると、回路検証に関する不都合、問題点あるいはその両方を軽減または解消する回路の有向ファルシフィケーションのための方法、論理及びシステムが提供される。
【０００７】
本発明のある実施例は、上記技術的効果のすべてまたは一部を提供するか、あるいはその何れをも提供しない。ある実施例は、ここでの図面、説明及び請求項から当業者には自明であるかもしれない他の技術的効果の１以上を提供するものであるかもしれない。
【発明を実施するための最良の形態】
【０００８】
図１は、回路１２の有向ファルシフィケーション（ｄｉｒｅｃｔｅｄ  ｆａｌｓｉｆｉｃａｔｉｏｎ）のための一例となるシステム１０を示す。システム１０は、後述するように、有向ファルシフィケーションのための回路１２と、回路１２において有向ファルシフィケーションを実行するためのエラー検出モジュール１４及びエラー検出データ１６を有する。１以上のリンクにより、システム１０のコンポーネントは互いに接続される。一例としてかつ限定することなく、１つのリンクは、適切な場合、１以上の回路基板上の１以上の配線、１以上の内部または外部バス、１以上のローカルエリアネットワーク（ＬＡＮ）、１以上のメトロポリタンエリアネットワーク（ＭＡＮ）、１以上のワイドエリアネットワーク（ＷＡＮ）、１以上のインターネット部分、あるいは上記２以上のリンクの組み合わせを有するようにしてもよい。
【０００９】
回路１２は、例えば、当該ハードウェアに対応する１以上の仕様に従ってハードウェアが適切に動作するか判断するためテストを行うためのハードウェア、論理または他のハードウェア表現を有する。一例としてかつ限定することなく、回路１２は、特定の機能を提供するよう互いに構成及び接続されたゲート、カウンタ、インバータ、バッファ及び他の回路コンポーネントなどの回路コンポーネントを有するものであってもよい。他の例として、回路１２は、論理やこのようなコンポーネントの他の表現を含むものであってもよい。回路１２は、数百万の回路コンポーネントを有するものであってもよい。ある機能を提供するため、回路１２は、１以上のプロパティを含む必要があるかもしれない。回路１２は、数百万のそのようなプロパティを含む必要があるかもしれない。ある実施例では、１以上の論理表現により、回路１２の１つのプロパティが記述されているかもしれない。回路１２の「プロパティ（ｐｒｏｐｅｒｔｙ）」とは、回路１２の論理的に表現可能な状態、特性、振舞いまたは動作、あるいは回路１２の他のプロパティを含むものであるかもしれない。
【００１０】
エラー検出モジュール１４は、後述のような、１以上のリンクを介し回路１２にアクセスし、回路１２を検証するためのハードウェア、ソフトウェア、埋め込み論理コンポーネントあるいは上記２以上のコンポーネントの組み合わせを含む。ある実施例では、回路１２におけるエラー検出は、回路１２が１以上のプロパティを有するか判断するための論理１２のテストを含む。一例としてかつ限定することなく、論理１２が１以上のプロパティを含むか判断するための回路１２のテストは、後述のような、回路１２における状態の特定を含むものであってもよい。エラー検出モジュール１４は、分割モジュール１８と１以上のファルシフィケーションモジュール２０を含む。分割モジュール１８は、後述のような、回路１２の状態空間を分割するためのハードウェア、ソフトウェア、埋め込み論理コンポーネントあるいは２以上の上記コンポーネントの組み合わせを含む。回路１２の状態空間は、回路１２のすべてまたは実質的にすべての状態を含む。各ファルシフィケーションモジュール２０は、後述のような、ＰＯＢＤＤを用いたファルシフィケーションアルゴリズムを回路１２の状態空間の一部に適用するためのハードウェア、ソフトウェア、埋め込み論理コンポーネントあるいは２以上の上記コンポーネントの組み合わせを含む。エラー検出データ１６は、回路１２のタイプを特定するデータと、ある実施例では、エラー検出モジュール１４が回路１２におけるエラーを検出するのに利用する他のデータを含む。ある実施例では、１以上のコンピュータシステムは、エラー検出モジュール１４とエラー検出データ１６へのユーザアクセスを提供する。一例としてかつ限定することなく、１以上のコンピュータシステムは、エラー検出モジュール１４とエラー検出データ１６を有し、ユーザは、エラー検出モジュール１４及びエラー検出データ１６への入力を与え、それらからの出力を受け取るため、１以上のコンピュータシステムにアクセスするようにしてもよい。
【００１１】
ファルシフィケーションとは、エラーを含む回路１２のエラー状態を検出することである。より正確には、プロパティｐが与えられたとき、ファルシフィケーションとは、ｐが破られる偽の状態ｓｐを検出することであり、検証の双対となるものである。回路１２におけるエラー状態とは、適切な場合、回路１２の不適当な機能に関する回路１２の状態を含むことを意味する。以前の検証アルゴリズムは、エラー状態が存在しないことを示すため、回路１２の到達可能な状態空間を効率的にカバーしようとする。しかしながら、回路１２がエラーを含む場合、当該回路の到達可能な状態空間を網羅的に探索しようとするより、エラー状態の検出はしばしばより効率的である。回路１２のエラーとは、適切な場合、回路１２における１以上のエラー状態を含むことを意味する。
【００１２】
広く用いられる２つのファルシフィケーションアルゴリズムは、（１）充足可能性ソルバ（ＳＡＴ  ｓｏｌｖｅｒ）を利用した有界モデルチェッキング（ＢＭＣ）と、（２）ＢＤＤを利用したモデルチェッキング及び記号到達可能性とである。ＢＭＣは、項（ｃｌａｕｓｅ）として状態を表し、ＳＡＴソルバを用いて、１以上の初期状態の集合から１以上のエラーの集合までのパスを検出する。１以上の初期状態の集合から１以上のエラーの集合までのパスを検出するため、ＢＭＣは、回路１２に対応する状態グラフの遷移関係（ＴＲ）を繰り返し展開し、このＴＲを項に変換する。この結果、ＢＭＣのみが相対的に浅いエラー（それらへの相対的に短いパスを有するエラーを含む）を検出するのに良好に機能する。深いエラーを検出するためには、ＢＭＣは、多数の項を生成する必要があり、これにより、以降のＳＡＴチェッキングを実現不可能なものにしてしまうことが多い。
【００１３】
エラーは、回路１２の相対的に深い所にあるかもしれない。一例としてかつ限定することなく、イーサネット（登録商標）スイッチを実現するハードウェアは、相対的に多数のタイムフレームに対して初期化を実行するかもしれない。イーサネット（登録商標）スイッチのハードウェアによる実現を具現化する回路１２の１以上のプロパティは、必然的に初期設定段階より深い所に存在するであろう。ＢＭＣは、初期設定段階より深いエラーの検出では効果的でないかもしれない。ＢＤＤを用いた回路１２の到達可能性分析は、ＢＭＣに置き換えられてもよい。様々なカウンタに類似した回路１２は、当該回路１２がコンパクトなＢＤＤ表現を有するが、実質的に管理不可能な数のＳＡＴ項を導くという意味で、「ＢＤＤフレンドリ」なものである。ＶＩＳ−Ｖｅｒｉｌｏｇベンチマークからの「Ｂ１２」回路１２は、そのような回路１２の一例である。従って、様々なシナリオにおいて、ＢＭＣは不適当であり、ＢＤＤを用いたエラー検出が必要とされる。以下で説明されるように、ある実施例はＢＤＤを利用することにより、ファルシフィケーションを向上させる。
【００１４】
記号到達可能性分析には、通常ＢＤＤである記号データ構造を用いた幅優先探索（ＢＦＳ）が含まれる。検証のための記号到達可能性は、到達可能なすべての状態を探索し、エラー状態が存在しないことを証明しようと試みる。エラー状態が到達可能である場合、当該エラーに導くパスが検出されるかもしれない。
【００１５】
状態空間の爆発的増大は、到達可能性分析の重大な問題である。回路１２のサイズが大きくなるに従い、回路１２の状態空間は回路１２のサイズに伴って指数的に増大するかもしれない。ＢＤＤは状態集合の記号表現であるため、回路１２に対応するＢＤＤのサイズはかなり大きなものとなるかもしれず、この点において、ＢＤＤにより処理することは厄介であり、かつメモリ多消費なものとなるかもしれない。さらに、ＢＤＤのサイズが適度に大きなものとなったとしても、エラーが回路１２の深い所に存在する場合、当該エラーに到達するには、到達可能性の多数のステップを要することになるであろう。このような状況は、ＢＤＤを用いた回路１２の到達可能性分析を遅延させ、分析を効果的なものにしなくなる傾向がある。モノリシック順序付けＢＤＤ（ＯＢＤＤ）は、一般に非効率的な表現である。分割ＯＢＤＤ（ＰＯＢＤＤ）を生成するため機能的分割を利用することは、このような表現のサイズをかなり減少させるかもしれない。
【００１６】
さらに、ＯＢＤＤは不安定なものとなる傾向がある。ＯＢＤＤのパフォーマンスは、ＯＢＤＤの生成及び処理に利用される変数の選択された値に一般に影響を受ける。一例としてかつ限定することなく、変数の順序付けは、しばしばＯＢＤＤのサイズの決定に重要な役割を担う。わずかな変数の設定の微妙な変化でさえ、ＯＢＤＤに関するメモリ要求のかなりの変動をもたらし、これにより、ＯＢＤＤの処理に関する時間要求に影響を与えるかもしれない。ＰＯＢＤＤは、それのパフォーマンスが各種分割要因にもまた影響を受けるため、ＯＢＤＤよりさらに不安定なものとなる傾向がある。
【００１７】
ＢＭＣは、ファルシフィケーションを通じた深いエラーの検出において効果的なものではない。ＯＢＤＤを用いた以前の到達可能性アルゴリズムは大域的な幅優先であるため、このようなアルゴリズムは深いエラーの検出においては効果的ではない。ある実施例は、典型的には、ＰＯＢＤＤに関する不安定さを取り除く傾向がある。ＰＯＢＤＤはコンパクトな表現を与え、分割到達可能性アルゴリズムは局所的（大域的でない）に幅優先であるため、ＰＯＢＤＤを利用したファルシフィケーションは、回路１２の深い所にあるエラーに対してより効果的なものとなる傾向がある。しかしながら、ＰＯＢＤＤはそれを生成するための変数の選択された値の影響を受けるため、ＰＯＢＤＤの実践的用途は限定される傾向がある。ある実施例では、ファルシフィケーションのため調整されたＰＯＢＤＤを利用した探索は、回路１２の状態空間の複数の探索を含む。複数の探索は、互いに独立かつパラレルに実行され、相異なる探索パスを含む。ある実施例では、各ファルシフィケーションモジュール２０は、これら複数の探索の１つを実行するようにしてもよい。
【００１８】
ＰＯＢＤＤを利用した複数の分割を処理するための適切なスケジュールの決定は、困難なものとなる傾向がある。不適切なスケジュールは、複数の分割の逐次的処理を非効率なものとするであろう。ＰＯＢＤＤを利用した複数の分割を処理するための適切なスケジュールの決定を回避するため、ある実施例は、互いにパラレルな状態空間の複数の検索を用いたＰＯＢＤＤを利用して、ファルシフィケーションを実行する。ある実施例は、状態空間の逐次的検索と、互いにパラレルな状態空間の検索の両方を同時に利用して、ＰＯＢＤＤを用いたファルシフィケーションを実行する。ある実施例では、到達可能性アルゴリズムは、有限状態マシーンの幅優先探索を含む。到達可能性アルゴリズムへの入力は初期状態の集合と、現在状態と当該現在状態から到達可能な次の状態とを関連付けるＴＲである。到達可能状態を決定するため、到達可能性アルゴリズムは一定の点に達するまで、繰り返し画像を計算する。
【００１９】
ある実施例は、ＰＯＢＤＤを用いて到達可能性に基づき検証を向上させる。一例としてかつ限定することなく、ＰＯＢＤＤを用いた到達可能性アルゴリズムは、以下の一例となる論理を含むものであってもよい。
【００２０】
【表１】
2005182766.tif 000003
ある実施例では、上記到達可能性アルゴリズムは、ＬｅａｓｔＦｉｘｅｄＰｏｉｎｔの各ステップの各分割ｉにおいて、できるだけ多くの画像計算を実行する。到達可能性アルゴリズムがもはや画像の計算をすることができなくなると、到達可能性アルゴリズムは各分割を互いに同期させる。各分割を互いに同期させるため、到達可能性アルゴリズムは、分割ｉから導出される各分割ｉの遷移を考える。
【００２１】
ＰＯＢＤＤを用いた上記到達可能性アルゴリズムは、厳密なＢＦＳ探索ではない。到達可能性アルゴリズムは、各分割に局所的なＢＦＳを実行し、その後、ある分割から他の分割にクロスオーバーする遷移から生じる状態を追加するため、各分割を互いに同期させる。従って、ある実施例では、到達可能性アルゴリズムは、状態空間の個々の領域、すなわち分割が、互いに独立に幅優先に探索される領域ＢＦＳを適用する。このような状態空間の探索は、ファルシフィケーションを大きく向上させるかもしれない。ＢＤＤが状態空間を幅優先探索するのに利用されるとき、ＢＤＤのパフォーマンスはＢＤＤを生成及び処理するための各種変数に割り当てられる値の影響を受ける。このような感応性は、ＢＤＤのサイズの相違から生じる傾向がある。到達可能性の間に、ＢＤＤは互いに類似した状態の集合をカバーする。
【００２２】
ＰＯＢＤＤを用いた典型的な到達可能性分析は、従来のＢＦＳを実行するものではない。分割要因に関して互いに異なる（軽微なものでさえ）ＰＯＢＤＤを用いた状態空間の探索は、互いに異なる状態空間の分割をもたらす傾向がある。このような探索はしばしば、互いに異なる順序で状態空間内の状態を探索する。グラフのサイズはまた、ＰＯＢＤＤがコンパクトな表現を与える傾向があるため、グラフの生成に用いられる分割変数に割り当てられる値に従って変化するようにしてもよい。このような状態空間の探索のためのパスの変動可能性及びコンパクトさに関する可能性は、このような分析を実行するのに利用される設定に対するＰＯＢＤＤを用いた到達可能性分析の感度を増幅させるものである。
【００２３】
ファルシフィケーションに対してＰＯＢＤＤを用いた到達可能性アルゴリズムが分割を探索するシーケンスは、当該到達可能性アルゴリズムのパフォーマンスに影響を与える。エラー状態を有する分割を探索する前に、エラー状態を含まない分割を探索することは、エラー状態の発見を遅らせる傾向があり、第１分割のエラー状態は第２分割のエラー状態より到達が容易であるかもしれない。この結果、エラー状態の発見可能性は、しばしば分割を探索するスケジュールに依存することになる。ファルシフィケーションによりエラーの検出が予期され、検証によりエラーが存在しないことを示すため、状態空間が探索されるため、スケジューリングはファルシフィケーションに対する到達可能性アルゴリズムの問題点を与える傾向があるが、検証に対する到達可能性アルゴリズムの同様の問題点を与えるものでない。
【００２４】
ある実施例は、２つの状態空間の分布尺度を利用する。第１の尺度は、深さｄである初期状態の集合から到達可能なエラー状態に導く最短パスの長さである。深さｄまでのＢＦＳにより、このエラーは検出されるであろう。浅いバグは、ｄの小さな値を有する最近接の到達可能なエラーを有し、深いバグはｄの大きな値を有する最近接の到達可能なエラーを有する。第２の尺度は、１以上の分割において到達可能なエラー状態の発生頻度である。到達可能なエラー状態を含む分割は、ウィットネス分割（ｗｉｔｎｅｓｓ  ｐａｒｔｉｔｉｏｎ）である。第１尺度と第２尺度との間の相互作用は、４つの可能なシナリオをもたらす。
・シナリオ１：浅いバグに対する多数のウィットネス分割。テストやシミュレーションを含む多くの方法がエラーを検出する可能性がある。
・シナリオ２：浅いバグに対する少数のウィットネス分割。例えば、ＯＢＤＤやＳＡＴ  ＢＭＣなどのＢＦＳを利用した状態空間を探索する方法が、エラーを検出する可能性がある。
・シナリオ３：深いバグに対する多数のウィットネス分割。多くの方法が回路１２の深くに進む困難さを経験し、浅い深さでのみ回路１２を探索することができる。ＢＦＳを状態空間に適用するＰＯＢＤＤを利用した到達可能性分析は、より少ない時間でより深い状態に到達する傾向がある。ある分割のエラー状態は、他の分割のエラー状態より到達可能性が高いものであるかもしれない。
・シナリオ４：深いバグに対する少数のウィットネス分割。シナリオ４は、形式検証に対する困難なシナリオである。上述のように、ＰＯＢＤＤの生成及び処理のための変数の値の選択及び分割オーダの変化は、結果を大きく変化させるかもしれない。１以上の第１探索は、１以上の第２探索よりはるかに速くエラーを検出するかもしれず、パフォーマンスの潜在的なインスタンビリティ（ｉｎｓｔａｎｂｉｌｉｔｙ）に付加される。
【００２５】
上述のように、回路の深くのエラーを検出するのにＰＯＢＤＤを利用したファルシフィケーションに対する到達可能性アルゴリズムのパフォーマンスは、到達可能性アルゴリズムによる分割の処理順序及び到達可能性アルゴリズムによる状態空間の探索方法に依存する。ある実施例は、並列処理を用いてこのようなパフォーマンスの問題を解決する。ある実施例では、ファルシフィケーションモジュール２０においてパラレルに実行される複数のファルシフィケーションアルゴリズムは、互いに異なるサーチパスに沿った状態空間の探索を可能にし、これにより、エラー状態の迅速な発見を容易にし、設定に対するＰＯＢＤＤの感度を減少させる。ファルシフィケーションを用いたエラー状態の発見は、状態が探索される順序に依存する。状態空間のある探索は、厳密なＢＦＳより速くエラー状態を発見するかもしれない。エラー状態の分布は事前的には未知なものであるため、１以上の効率的サーチパスの決定は困難である。
【００２６】
ある実施例では、ＰＯＢＤＤはコンパクトな表現を提供し、かつＰＯＢＤＤの生成及び処理に利用される変数に割り当てられた値に対して感度が高いため、複数のファルシフィケーションモジュール２０の各々は、ＰＯＢＤＤを利用することにより、回路１２の状態空間の分割をパラレルに探索する。すべてのファルシフィケーションモジュール２０は、ファルシフィケーションモジュール２０がエラー状態を特定すると、各自の探索を継続することをやめる。上述のように、ファルシフィケーションモジュール２０は、互いにパラレルに動作し、互いに独立に実行するプロセッサを含む。ファルシフィケーションモジュール２０が互いにパラレルに動作し、互いに独立に実行するプロセッサを含むため、各ファルシフィケーションモジュール２０は、ローカルメモリを利用して、回路１２の状態空間の分割を探索するようにしてもよい。
【００２７】
ある実施例では、分割モジュール１８は、各分割における固定点計算を簡単化するため、回路１２の状態空間の相対的に少数の分割を生成する。分割モジュール１８による相対的に少数の分割の生成の結果として、分割モジュール１８は、相対的に多数の分割を生成する。より少数の分割は、上述のＰＯＢＤＤを用いた一例となる到達可能性アルゴリズムが分割のより深くに進入することを可能にし、到達可能性アルゴリズムが上記シナリオ３及び４におそらく対応する回路１２のより深くにあるエラー状態を特定することを可能にする。
【００２８】
ある実施例では、エラー検出モジュール１４は、回路１２の状態空間の分割をパラレルに処理する。ファルシフィケーションモジュール２０は、その他の分割から独立した分割の１つを処理し、可能な限り遠くの分割に到達する。エラー検出モジュール１４は、２以上の分割を互いに同期させるようにしてもよい。ある実施例では、エラー検出モジュール１４は、同期処理のための１以上の共有メモリを利用して、異なるプロセッサにおける異なるメモリの処理に関するオーバヘッドを低下させる。回路１２の状態空間のパラレルな分割の処理は、回路１２におけるエラーの検出に関する作業を分散させ、処理対象のスケジューリング分割を回避する。
【００２９】
一例としてかつ限定することなく、Ｎ個の分割を仮定する。また、共有メモリモデルを利用したファルシフィケーションモジュール２０などの独立なプロセッサにおける分割の実行を仮定する。また、簡単化のため、パラレルにこれら分割を実行するのに十分なプロセッサが利用可能であり、プロセッサの利用が実際のオーバヘッドを被らないことを仮定する。分割ｉを完全に観察するための時間をｔｉとする。これにより、Ｎ個の分割を含む状態空間を完全に探索するのに要する合計時間は、逐次的アプローチではＳｔｉであり、パラレルに実行されるときにはｍａｘ（ｔｉ）である。ファルシフィケーションに対して、エラーが検出されると、当該アルゴリズムは停止する。ｅｉを分割ｉにおけるエラー状態の特定に要する時間とする。分割ｉがエラー状態を含まないときには、等号ｅｉ＝ｔｉが成り立つ。最初の（ｊ−１）個の分割がエラーを含まず、ｊ番目の分割がエラー状態を有するように、Ｎ個の分割がスケジューリングされると仮定する。このとき、逐次的アプローチによりかかる時間は、
【００３０】
【数１】
2005182766.tif 000004
である。すべての分割がパラレルに実行されるとき、最先のエラー状態が検出されるまで、各分割は実行する。トータルの作業にかかる時間は、Ｎ＊ｍｉｎｊｅｊに限定され、ユーザにより認められる時間はさらにｍｉｎｊｅｊまで減少される。ここで、当該時間ｍｉｎｊｅｊは合計の逐次的時間
【００３１】
【数２】
2005182766.tif 000005
より小さく、ゲインはパラレルなプロセッサの個数に関して超線形（ｓｕｐｅｒｌｉｎｅａｒ）であるかもしれない。逐次的な実行と比較して、パラレルな設定は、ＰＯＢＤＤが高速なファルシフィケーションに適するものとすることができるということを示す劇的なゲインを提供することが可能である。また、逐次的なケースでは、エラーを含まない分割は必ずしも探索される必要がないかもしれない。エラーが検出されるときでも、当該エラーは、到達するのが最も容易な分割にあるものではないかもしれない。パラレルなケースは、そのような順序付けが不要であり、エラー状態に最も迅速に到達するという点で効果的である。
【００３２】
ある実施例では、ファルシフィケーションモジュール２０は、５１２ＭＢのメインメモリを備えた２．２ＧＨｚデュアルプロセッサＸＥＯＮ中央演算ユニット（ＣＰＵ）を有する。ある実施例は、コロラド大学決定図（ＣＵＤＤ）ＢＤＤパッケージを用いたＶＩＳ２．０上でファルシフィケーションモジュール２０（または１以上のエラー検出モジュール１４のコンポーネント）を実現する。ある実施例は、変数の再順序付けのためレイジーシフトを利用する。ある実施例では、ＶＩＳ−Ｖｅｒｉｌｏｇベンチマークでの回路１２のすべての失敗した不変量が、ファルシフィケーションのため考慮される。このような実施例は、重要なＢＤＤパラメータが少数の走査に対し変化するとき、ＯＢＤＤ及びＰＯＢＤＤを用いたファルシフィケーションに要する時間の変動を示す傾向がある。ＰＯＢＤＤはその多くがＯＢＤＤを用いた方法には利用可能でない、より大きな変数の集合に反応する。しかしながら、より多くの実行は、複数の提示から構成されるより多くのデータを生成するであろう。両方の方法に対して、同数かつ少数の走査が分析されてもよい。
【００３３】
ＯＢＤＤを用いた到達可能性アルゴリズムの容易に変化可能な変数は、分割ＴＲのクラスタサイズである。一例としてかつ限定することなく、ユーザは、例えば、１００、２００、５００、２５００及び５０００などの１００から５０００までの範囲でクラスタサイズを変化させるようにしてもよい。ベースライン設定はそれの結果が変動に対して比較され、極値のほぼ平均である２５００のクラスタサイズを有するようにしてもよい。他の容易に変化可能な変数は、一時的変数の導入に対する閾値である。ユーザは、この閾値を不変なものにしておくかもしれない。パラメータの変動に関わらず、ＯＢＤＤを用いた各探索は厳密にＢＦＳを保持するものであってもよい。エラー検出モジュール１４がＰＯＢＤＤを用いて状態を探索する順序は、変数の設定により変動する。ある実施例は、２つの変数集合を含む。第１の集合は、例えば、分割変数や分割数などのデータ構造表現に対応する変数を含む。第２集合の変数は、例えば、ＴＲのクラスタサイズ、分割を開始するときには分割を処理するためのスケジュール、及び動的な分割閾値などの到達可能性に関するものである。ＰＯＢＤＤをＯＢＤＤと同数の走査（例えば、５）に制限するため、ユーザは、限られた個数の変数のみを変化させるようにしてもよい。ある実施例では、ユーザは、分割変数の選択及びＴＲのクラスタサイズのみを変化させる。ある実施例では、各走査に対して、分割モジュール１８は、１６個の初期分割を生成するため、４つの分割変数を利用する。
【００３４】
ある実施例では、最初の３つの走査に対して、到達可能性変数が一定とされる。例えば、ＴＲクラスタサイズが２５００の以前のベースライン値に設定される。分割変数の以下の選択が試行される。すなわち、ＯＢＤＤ変数順序リストの変数、ＴＲ分析からの変数、及び状態集合グラフを用いた同様の分析からの変数である。ある実施例では、ユーザは、他の何れの分割変数も変化させない。最後の２つの走査に対して、すべての分割変数が一定とされ、到達可能性パラメータが可変とされる。上記第１の分割選択と、クラスタサイズの極値を省略した２００及び５００のクラスタサイズが利用される。
【００３５】
ある実施例では、ＯＢＤＤの結果は変数設定の変化により控えめに変動する。ＰＯＢＤＤの結果はしばしば、大きさに関する多数のオーダを含む変化を含む。この結果、分割はその設定の影響を受ける。さらに、どのような変数設定の単一の選択も、ＶＩＳベンチマークのすべてのファルシフィケーションプロパティの計算を行うことができない。各設定は、１以上の回路に対して本質的なものであるかもしれない。ある回路では、ＯＢＤＤに基づく走査の何れもがエラーを検出しないかもしれない。しかしながら、共に考慮されるとき、ＰＯＢＤＤに基づく走査は、すべてのプロパティをファルシファイ（ｆａｌｓｉｆｙ）ことが可能である。ＰＯＢＤＤはまた、より広範な振る舞いを示す傾向がある。ある実施例は、様々な設定をパラレルに試行し、非効率なケースを拒絶する自動的方法を提供する。ある実施例は、複数の探索をパラレルに行い、何れかが終了すると、残りを終了させることにより、このような方法を実現する。ある実施例は、ＯＢＤＤ及びＰＯＢＤＤを用いてこのような方法をファルシフィケーションに適用する。
【００３６】
ある実施例では、複数の分割のパラレルなサーチは、最も速く到達するエラー状態を検出する。さらに、ある回路１２では、最も効率的な設定集合を提供する設定はない。ある実施例では、しかしながら、パラレルな走査はスケジューリングを必要とせず、このため、エラー状態により速く到達することができる。ある実施例は、ＰＯＢＤＤとパラレルなフレームワークを用いた分割を利用する誘導なしの自動的アプローチを介して、初期状態から離れたエラーを検出する問題を解決する。ある実施例は、二方面の解を含むものである。第１に、複数の独立なファルシフィケーションアルゴリズムは、主としてＢＦＳによる既存のアプローチと異なり、相異なるサーチパスをパラレルに探索する。複数の独立なファルシフィケーションアルゴリズムをパラレルに探索させると、相異なるサーチパスは、ＢＤＤパラメータに対するファルシフィケーションの感度を低下させ、全体的な安定性を向上させる。第２に、状態空間のパラレルなサーチは分割スケジューリングを回避させ、これによりしばしば、ファルシフィケーションに対する逐次的なアプローチのボトルネックとなる。ある実施例では、パラレル化は、たとえ小さなスケールであっても、大きさに関する２つのオーダのゲインを提供するかもしれない。
【００３７】
ある実施例は、分割技術を用いた回路におけるバグや他のエラーの自動的検出方法を含む分割志向アプローチを利用した有向ファルシフィケーションを提供する。数学的には、ファルシフィケーション（プロパティＰは誤りか？）は、単に、検証（プロパティＰは真であるか？）の否定であるが、実際的には、ファルシフィケーションは設計検証における典型的なキーとなる問題である。多くのプロパティベースの検証ツールは、しばしば実際には、プロパティの十分な集合が存在せず、必要な集合のみが存在するため、あるタイプのファルシフィケーションを試みる。従って、ファルシフィケーションに集中することが実用的である。シミュレーションは、しばしば、ファルシフィケーションにおけるその利用のため利用される。しかしながら、シミュレーションは、大きな状態集合を観察するためには典型的には弱く、以前の形式検証（ＦＶ）技術は、深いかあるいは困難な機能を探索するためには不適切である。これに関して、ＰＯＢＤＤは、それが回路の深さ優先探察（ＤＦＳ）分析に基づくものであるため、ファルシフィケーションを容易にするかもしれない。
【００３８】
ＰＯＢＤＤは、それがＤＦＳ分析に基づくものであるため、深い状態に相対的に速く到達するのに利用することができる。しかしながら、このような技術は、エラーが一様分布していない場合、あるいはエラーが低い密度の分割からの短いパスを有する場合、失敗するかもしれない。ある実施例は、１以上のエラー状態（存在する場合には）に到達するのに探索されるべき状態空間のパターンを決定し、必要に応じて深さ優先分析の方向を決定する。ある実施例はまた、１以上のエラー状態に到達するのに有益な状態マップをもたらし（当該エラー状態が他の分割において発生したとしても）、必要に応じてエラーウィットネスを捕捉する。
【００３９】
ある実施例では、ＤＦＳ、それに続きＢＦＳ、さらにその後に誘導探索により方法が動作する。これにより、当該方法は、各段階において生成された情報から効果を得ることができるかもしれない。当該方法は、モノリシックな計算を伴うことなく、ＰＯＢＤＤ構成を計算することによりＤＦＳ段階において動作するようにしてもよい。第２段階では、小さなモノリシック計算は、当該計算が困難さを示すまで、実行されるようにしてもよい。第３段階では、ＢＤＤの爆発的増大が発生するまで、プリイメージが可能なエラー状態から計算されてもよい。爆発的増大の定義は、以降における集合の共通部分の演算に影響を与えず、ＢＤＤ計算オーバヘッドを生成しないように保持されてもよい。この情報は、計算され、先行するＢＦＳ走査から当該方法にわたされるようにしてもよく、これにより、当該方法における効率性を促進させるかもしれない。このステップは、エラーウィットネスとそのプリイメージの確率分布（またはマップ）の効率的な決定を促進し、これによりエラー地形（ｔｅｒｒａｉｎ）が与えられるかもしれない。その後、この地形は、１以上の分割に効率的にマッピングされ、当該情報はＤＦＳ探索が行われるべき１以上の分割を決定するため利用されてもよい。しかしながら、通信中において、残りの分割がタッチされるであろう。この段階において、当該方法は、計算された状態によりエラー地形の共通部分を計算するようにしてもよい。第１の共通部分において、エラーが検出されているため、当該方法は終了するようにしてもよい。ある実施例は、ファルシフィケーションに基づく検証技術に関する時間要求を大きく軽減するかもしれない。ある実施例では、このようなゲインは、１０×から１００×（以前の技術に対して）のオーダであってもよい。
【００４０】
図２は、回路１２の有向ファルシフィケーションのための一例となる方法を示す。本方法はステップ１００から開始され、エラー検出モジュール１４が回路１２にアクセスし、分割モジュール１８を利用して、ＰＯＢＤＤを用いたファルシフィケーションに対して回路１２の状態空間を分割する。ステップ１０２において、各ファルシフィケーションモジュール２０が、回路１２におけるエラーを特定するため、ＰＯＢＤＤを用いたファルシフィケーションアルゴリズムを状態空間の分割に適用する。上述のように、ある実施例では、ファルシフィケーションモジュール２０の何れかがエラーを特定すると、すべてのファルシフィケーションモジュール２０が、状態空間の探索の継続をやめる。ステップ１０４において、エラー検出モジュール１４は、通信のため、存在する場合には、回路１２の１以上の特定されたエラーを示す出力を１以上のユーザに提供し、ここで本方法は終了する。
【００４１】
本開示は特定の実施例及び一般的に関連する方法に関して説明されたが、上記実施例及び方法の変更及び置換は当業者には明らかであろう。このため、上記実施例に関する説明は、本開示を画定または限定するものではない。本開示の趣旨及び範囲から逸脱することなく、他の変更、置き換え及び変形もまた可能である。
【００４２】
（付記１）  回路の有向ファルシフィケーションのための方法であって、
前記回路の状態空間の１以上の分割を選択するステップと、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップと、
から構成され、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とする方法。
【００４３】
（付記２）  付記１記載の方法であって、
前記ファルシフィケーションベース順方向到達可能性技術による１以上の分割の分析は、前記１以上の分割における幅優先探索（ＢＦＳ）を実行することからなることを特徴とする方法。
【００４４】
（付記３）  付記１記載の方法であって、さらに、
前記回路の状態空間の複数の分割を選択するステップと、
前記複数の分割の何れかが前記回路において１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って、互いに独立な前記複数の分割のそれぞれをパラレルに分析するため、１以上のＰＯＢＤＤを利用するステップと、
を有することを特徴とする方法。
【００４５】
（付記４）  付記３記載の方法であって、
前記複数の分割の第１分割の第１分析は、前記複数の分割の１以上の第２分割の１以上の第２分析における１以上の第２サーチパスに関して一意的な第１サーチパスから構成されることを特徴とする方法。
【００４６】
（付記５）  付記３記載の方法であって、
前記複数の分割の１つ分割の各分析は、該分割を探索するためローカルメモリを利用することからなることを特徴とする方法。
【００４７】
（付記６）  付記３記載の方法であって、さらに、
前記複数の分割の１つの分割の分析が前記回路においてエラーを検出する場合、前記複数の分割のすべての分析を終了させるステップを、
有することを特徴とする方法。
【００４８】
（付記７）  付記３記載の方法であって、さらに、
前記複数の分割の第１分割の第１分析が固定されたポイントに到達する場合、前記複数の分割の前記第１分割を、前記複数の分割の１以上の第２分割と同期させるステップを有し、
前記１以上の第２分割の１以上の第２分析はまた固定されたポイントを有する、
ことを特徴とする方法。
【００４９】
（付記８）  付記７記載の方法であって、さらに、
前記複数の分割の第１分割を前記複数の分割の１以上の第２分割と同期させるため、共有メモリを利用するステップを、
有することを特徴とする方法。
【００５０】
（付記９）  付記１記載の方法であって、
前記回路の状態空間の１以上の選択された分割は、前記１以上の分割の分析が前記１以上の分割における１以上の深い状態に到達することを可能にするサイズを有することを特徴とする方法。
【００５１】
（付記１０）  付記１記載の方法であって、
２つのプロセッサから構成される中央演算ユニット（ＣＰＵ）は、前記１以上の分割が前記回路における１以上のエラーを有するか判断するため、前記ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割の分析を実行することを特徴とする方法。
【００５２】
（付記１１）  回路の有向ファルシフィケーションのための論理であって、該論理はコンピュータ実行可能な媒体に符号化され、実行時に、
前記回路の状態空間の１以上の分割を選択するステップと、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用するステップと、
を処理可能であり、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とする論理。
【００５３】
（付記１２）  付記１１記載の論理であって、さらに、
前記ファルシフィケーションベース順方向到達可能性技術による１以上の分割の分析するため、前記１以上の分割において幅優先探索（ＢＦＳ）を実行するステップを、
処理可能であることを特徴とする論理。
【００５４】
（付記１３）  付記１１記載の論理であって、さらに、
前記回路の状態空間の複数の分割を選択するステップと、
前記複数の分割の何れかが前記回路において１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って、互いに独立な前記複数の分割のそれぞれをパラレルに分析するため、１以上のＰＯＢＤＤを利用するステップと、
を処理可能であることを特徴とする論理。
【００５５】
（付記１４）  付記１３記載の論理であって、
前記複数の分割の第１分割の第１分析は、前記複数の分割の１以上の第２分割の１以上の第２分析における１以上の第２サーチパスに関して一意的な第１サーチパスから構成されることを特徴とする論理。
【００５６】
（付記１５）  付記１３記載の論理であって、
前記複数の分割の１つ分割の各分析は、該分割を探索するためローカルメモリを利用することからなることを特徴とする論理。
【００５７】
（付記１６）  付記１３記載の論理であって、さらに、
前記複数の分割の１つの分割の分析が前記回路においてエラーを検出する場合、前記複数の分割のすべての分析を終了させるステップを、
処理可能であることを特徴とする論理。
【００５８】
（付記１７）  付記１３記載の論理であって、さらに、
前記複数の分割の第１分割の第１分析が固定されたポイントに到達する場合、前記複数の分割の前記第１分割を、前記複数の分割の１以上の第２分割と同期させるステップを処理可能であり、
前記１以上の第２分割の１以上の第２分析はまた固定されたポイントを有する、
ことを特徴とする論理。
【００５９】
（付記１８）  付記１７記載の論理であって、さらに、
前記複数の分割の第１分割を前記複数の分割の１以上の第２分割と同期させるため、共有メモリを利用するステップを、
処理可能であることを特徴とする論理。
【００６０】
（付記１９）  付記１１記載の論理であって、
前記回路の状態空間の１以上の選択された分割は、前記１以上の分割の分析が前記１以上の分割における１以上の深い状態に到達することを可能にするサイズを有することを特徴とする論理。
【００６１】
（付記２０）  付記１１記載の論理であって、さらに、
前記１以上の分割が前記回路における１以上のエラーを有するか判断するため、前記ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割の分析を実行する２つのプロセッサから構成される中央演算ユニット（ＣＰＵ）を、
有することを特徴とする論理。
【００６２】
（付記２１）  回路の有向ファルシフィケーションのためのシステムであって、
前記回路の状態空間の１以上の分割を選択する手段と、
前記１以上の分割が前記回路の１以上のエラーを有するか判断するため、ファルシフィケーションベース順方向到達可能性技術に従って前記１以上の分割を分析するため、１以上のＰＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  Ｏｒｄｅｒｅｄ  Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）を利用する手段と、
から構成され、
前記１以上の分割の各々は、前記状態空間の一部のみから構成され、前記回路の１以上の特性を示す１以上のプリイメージ計算の１以上の結果に従い選択され、
前記１以上の特性は、前記分割が前記回路における１以上のエラーを有する可能性を示す、
ことを特徴とするシステム。
【図面の簡単な説明】
【００６３】
【図１】回路の有向ファルシフィケーションのための一例となるシステムを示す。
【図２】回路の有向ファルシフィケーションのための一例となる方法を示す。
【符号の説明】
【００６４】
１０  システム
１２  回路
１４  エラー検出モジュール
１６  エラー検出データ
１８  分割モジュール
２０  ファルシフィケーションモジュール
【図１】
2005182766.tif 000006
【図２】
2005182766.tif 000007
【外国語明細書】
2005182766.tif 000008
2005182766.tif 000009
2005182766.tif 000010
2005182766.tif 000011
2005182766.tif 000012
2005182766.tif 000013
2005182766.tif 000014
2005182766.tif 000015
2005182766.tif 000016
2005182766.tif 000017
2005182766.tif 000018
2005182766.tif 000019
2005182766.tif 000020
2005182766.tif 000021
2005182766.tif 000022
2005182766.tif 000023
2005182766.tif 000024
2005182766.tif 000025
2005182766.tif 000026
2005182766.tif 000027
2005182766.tif 000028
2005182766.tif 000029
2005182766.tif 000030
2005182766.tif 000031