(57)【要約】【課題】プロトコルや相互接続アーキテクチャなどのアーキテクチャの効率的な検証カバレッジを確実にする方法及び装置を本明細書及び特許請求の範囲に記載している。【解決手段】アーキテクチャの状態のカバレッジ空間を生成し、データベースに格納する。シミュレーション中、遭遇される、カバレッジ空間の状態がマーキングされる。これから、遭遇される状態、及び遭遇されない状態を判定することができる。遭遇されない状態に基づいて、先行シミュレーション中に遭遇されなかった状態の少なくとも一部を標的化するための標的化検査スイートが策定される。シミュレーション中に遭遇されないカバレッジ空間の状態に基づいた検査スイートの精緻化への、シミュレーションからの前述の帰還ループは、カバレッジ空間の十分な検証（すなわち、検証の十分な信頼度）が達成されるまで再帰的に反復することができる。【選択図】図２
2009157928.tif 000002
【特許請求の範囲】
【請求項１】
装置であって、
カバレッジ・データベースを保持する記憶媒体を備え、前記カバレッジ・データベースは、アーキテクチャの第１の数の考えられる状態に対応する第１の数のエントリを含み、前記複数の考えられる状態のうちの考えられる一状態に対応する前記第１の数のエントリのうちの一エントリが複数のパラメータ値を含み、前記パラメータ値はそれぞれ、前記考えられる一状態の前記アーキテクチャの関連付けられたパラメータの値を表す装置。
【請求項２】
請求項１記載の装置であって、前記第１の数のエントリのうちの前記一エントリは、トークン識別子を更に含み、前記トークン識別子は、前記複数のパラメータ値のアルゴリズムの組合せに基づく装置。
【請求項３】
請求項２記載の装置であって、前記第１の数のエントリのうちの前記一エントリは、前記考えられる一状態にレジスタ・トランスファ・レベル（ＲＴＬ）シミュレーションが遭遇することに応じて、マーキングされた値に更新される対象のマーキング・フィールドを更に含む装置。
【請求項４】
請求項１記載の装置であって、前記複数のパラメータ値は、前記複数のパラメータ値のうちの大局パラメータ値群、及び前記複数のパラメータ値のうちの複数のエージェント・パラメータ値群における前記第１の数のエントリのうちの前記一エントリにおいてグループ化され、前記大局パラメータ群は前記アーキテクチャの大局パラメータに対応し、前記複数のエージェント・パラメータ値群はそれぞれ、前記アーキテクチャのエージェント特有パラメータ値を含む装置。
【請求項５】
請求項１記載の装置であって、前記アーキテクチャはプロトコル・アーキテクチャを含み、前記プロトコル・アーキテクチャは、キャッシュ・コヒーレンス・プロトコル・アーキテクチャ、トランザクション層プロトコル・アーキテクチャ、リンク層プロトコル・アーキテクチャ、相互接続プロトコル・アーキテクチャ、無線通信プロトコル・アーキテクチャを含む群から選択される装置。
【請求項６】
請求項１記載の装置であって、前記関連付けられたパラメータは、各種のエージェント、エージェント応答、装置応答、相互接続応答、メッセージ応答、応答のタイプ、特定の動作に対する他の応答、応答のデスティネーション、メッセージ、メッセージのタイプ、メッセージのデスティネーション、要求、要求のタイプ、要求のデスティネーション、キャッシュのタイプ、キャッシュ状態、キャッシュの場所、レジスタ状態を含む群から独立的に選択される装置。
【請求項７】
請求項６記載の装置であって、前記第１の数の考えられる状態は、前記アーキテクチャのモデルを検査するためのモデル検査器の実行中に調査される全状態を含む装置。
【請求項８】
請求項６記載の装置であって、前記第１の数の考えられる状態は、前記アーキテクチャのモデルを検査するためのモデル検査器モデルの実行中に調査される全状態の対称的に縮減された組を含む装置。
【請求項９】
製品であって、
マシンによって実行されると、
プロトコル実現形態の汎用検査スイートのシミュレーション中に入らない、プロトコル実現形態の参照データベース内に保有される第１の数の状態を判定する機能と、
前記汎用検査スイートのシミュレーション中に入らない前記第１の数の状態のうちの複数を標的化するための、標的化されたシミュレーション検査スイートを、前記プロトコル実現形態についてシミュレートされると、策定する機能とを前記マシンに行わせるプログラム・コードを含む製品。
【請求項１０】
請求項９記載の製品であって、前記プロトコル実現形態の汎用検査スイートのシミュレーション中に入らない、プロトコル実現形態の参照データベース内に保持される第１の数の状態を判定する機能は、
前記プロトコル実現形態の前記汎用検査スイートをシミュレートする機能と、
前記汎用検査スイートのシミュレーション中に入る、前記参照データベース中に保持される第２の数の状態をマーキングする機能と、
前記汎用検査スイートのシミュレーション中、前記第２の数の状態をマーキングした後、マーキングされない前記第１の数の状態に応じて、前記汎用検査スイートのシミュレーション中に、前記参照データベース内に保持された前記第１の数の状態に入らない旨を判定する機能とを含む製品。
【請求項１１】
請求項１０記載の製品であって、前記汎用検査スイートのシミュレーション中に入らない前記第１の数の状態のうちの複数を標的化するための、標的化されたシミュレーション検査スイートを、前記プロトコル実現形態についてシミュレートされると、策定する機能は、
前記汎用検査スイートのシミュレーション中に入らない、前記第１の数の状態のうちの前記複数を識別する機能と、
前記汎用検査スイートのシミュレーション中に入らない、前記第１の数の状態の内の前記複数までの、初期状態からの複数のトレースを判定する機能と、
前記プロトコル実現形態についてシミュレートされる場合、前記標的化されたシミュレーション検査スイート内の前記複数のトレースを構築して、前記第１の数の状態のうちの前記複数を標的化する機能とを含む製品。
【請求項１２】
請求項１１記載の製品であって、前記汎用検査スイートのシミュレーション中に入らない前記第１の数の状態のうちの前記複数を識別する機能は、前記参照データベースの自動化クエリに応答する製品。
【請求項１３】
請求項１０記載の製品であって、前記プログラム・コードは、前記マシンによって実行されると、
前記標的化されたシミュレーション検査スイートをシミュレートする機能と、
前記標的化されたシミュレーション検査スイートのシミュレーション中に入る、前記参照データベースに保持される前記第１の数の状態のうちの前記複数にマーキングする機能とを前記マシンに更に行わせる製品。
【請求項１４】
製品であって、
マシンによって実行されると、
検証オブジェクトの考えられる状態のカバレッジ空間を前記検証オブジェクトの複数のパラメータに基づいて判定する機能と、
前記考えられる状態の前記複数のパラメータに対応する複数の対応する値に基づいて、前記考えられる状態のカバレッジ空間内の考えられる状態の対応するトークン識別子を算出する機能と、
前記考えられる状態の前記対応するトークン識別子及び前記複数の対応する値をデ―タベースのエントリに格納する機能とを前記マシンに更に行わせるプログラム・コードを含む製品。
【請求項１５】
請求項１４記載の製品であって、前記検証オブジェクトは、通信プロトコル、ネットワーキング・プロトコル、無線プロトコル、コヒーレンス・プロトコル、相互接続プロトコル、及び物理的相互接続アーキテクチャの群から選択される製品。
【請求項１６】
請求項１４記載の製品であって、複数の相互接続パラメータに基づいて検証オブジェクトの考えられる状態のカバレッジ空間を判定する機能は、
前記検証オブジェクトの複数の構成制約に基づいて前記検証オブジェクトの形式モデルを合わせる機能と、
前記複数のパラメータの差異にわたって、前記検証オブジェクトの考えられる状態全てを調査して、前記考えられる状態のカバレッジ空間を形成するようモデル検査器を実行する機能とを含む製品。
【請求項１７】
請求項１４記載の製品であって、前記考えられる状態の前記複数のパラメータに対応する複数の対応する値に基づいて、前記考えられる状態のカバレッジ空間内の考えられる状態の対応するトークン識別子を算出する機能は、前記対応するトークン識別子を得るためのアルゴリズムを使用して前記複数の対応する値を結合する機能を含む製品。
【請求項１８】
請求項１６記載の製品であって、
前記検証オブジェクトの汎用検査スイートをシミュレートする機能と、
前記検証オブジェクトの前記汎用検査スイートのシミュレート中に前記考えられる状態に遭遇することに応じて前記考えられる状態に関連付けられた前記データベースの前記エントリにマーキングする機能と、
前記検証オブジェクトについてシミュレートした場合、標的化された検査スイートを提供して、前記汎用検査スイートをシミュレートした後、前記データベースの前記エントリがマーキングされていないことに応じて前記考えられる状態を標的化する機能とを更に含む製品。
【請求項１９】
方法であって、
アーキテクチャの複数の考えられる状態を判定する工程と、
前記複数の考えられる状態毎の数値パラメータに基づいて前記複数の考えられる状態毎の識別子を算出する工程と、
前記複数の考えられる状態毎の前記識別子、及び、前記複数の考えられる状態毎の前記数値パラメータをデータベースに格納する工程とを含む方法。
【請求項２０】
請求項１９記載の方法であって、アーキテクチャの複数の考えられる状態を判定する工程は、複数の構成制約に基づいて形式モデルをフィルタリングして前記アーキテクチャの実現形態モデルを形成する工程と、前記実現形態モデルに対するモデル検査を行って、前記アーキテクチャの前記複数の考えられる状態を判定する工程とを含む方法。
【請求項２１】
請求項１９記載の方法であって、アーキテクチャの複数の考えられる状態を判定する工程は、複数の構成制約に基づいて形式モデルをフィルタリングして前記アーキテクチャの実現形態モデルを形成する工程と、前記実現形態モデルに対してモデル検査を行って前記アーキテクチャの前記考えられる状態全てを判定する工程と、前記考えられる状態全てのうちの複数の対称状態を縮減して前記複数の考えられる状態を判定する工程とを含む方法。
【請求項２２】
請求項１９記載の方法であって、前記複数の考えられる状態毎の数値パラメータに基づいて前記複数の考えられる状態毎の識別子を算出する工程は、前記複数の考えられる状態毎の前記識別子を算出するための所定の数値計算用アルゴリズムを利用して、前記複数の考えられる状態毎の前記数値パラメータを結合する工程を含む方法。
【請求項２３】
方法であって、
アーキテクチャの考えられる状態の数を判定する工程と、
汎用検査スイートを実行して前記アーキテクチャの動作をシミュレートする工程と、
前記汎用検査スイートの実行中に遭遇されない前記考えられる状態の数のうちの複数に基づくフィードバックを供給して、標的化された検査スイートを形成する工程とを含み、前記標的化された検査スイートは実行されると、前記汎用検査スイートの実行中に遭遇されない前記考えられる状態の数のうちの前記複数を標的化する方法。
【請求項２４】
請求項２３記載の方法であって、前記アーキテクチャはプロトコル・アーキテクチャを含み、前記プロトコル・アーキテクチャは、相互接続通信プロトコル・アーキテクチャ、キャッシュ・コヒーレンシ・プロトコル・アーキテクチャ、ネットワーク通信プロトコル・アーキテクチャ、及び無線通信プロトコル・アーキテクチャを含む群から選択される方法。
【請求項２５】
請求項２３記載の方法であって、アーキテクチャの考えられる状態の数を判定する工程は、
前記アーキテクチャの形式モデルを前記アーキテクチャの実現形態特有モデルに、複数の構成制約に基づいてフィルタリングする工程と、
モデル検査器を実行して、前記アーキテクチャの前記実現形態特有モデルの前記考えられる状態の数を判定する工程とを含む方法。
【請求項２６】
請求項２３記載の方法であって、前記考えられる状態の数それぞれの表現を前記データベースのエントリに記憶する工程を含み、前記データベースの各エントリは、前記エントリに関連付けられた前記考えられる状態の数のうちの考えられる状態を規定する複数のパラメータに関連付けられた複数の数値を保持するための数値フィールドと、前記複数の数値に基づいてトークン識別子を保持するためのトークン識別子フィールドと、マーキングされた値に更新されると、前記汎用検査スイートの実行中に前記考えられる状態に遭遇している旨を示すためのマーキング・フィールドとを含む方法。
【請求項２７】
請求項２６記載の方法であって、前記汎用検査スイートの実行中に遭遇されない前記考えられる状態の数のうちの複数に基づくフィードバックを供給して、標的化された検査スイートを形成する工程であって、前記標的化された検査スイートは実行されると、前記汎用検査スイート中に遭遇されない前記考えられる状態の数のうちの前記複数を標的化する工程は、
前記汎用検査スイートの実行中に前記状態の数のうちの前記考えられる状態に遭遇することに応じて、前記データベースの各エントリの前記マーキング・フィールドを更新する工程と、
遭遇されない前記考えられる状態の数のうちの前記複数を、マーキングされていない値を保持する前記考えられる状態の数のうちの前記複数それぞれに関連付けられた前記マーキング・フィールドに基づいて判定する工程と、
前記汎用検査スイートを修正して、前記標的化された検査スイートを形成する工程とを含む方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータ・システムの分野に関し、特に、プロトコルの検証方法に関する。
【背景技術】
【０００２】
半導体プロセス及びロジック設計の進展により、集積回路装置上に存在し得るロジックの量を増加させることが可能になっている。更に、コンピュータ・システムは、伝統的な計算機システム、メディア記憶システム、娯楽センター、オーディオ再生、ビデオ再生、サーバ等などの別々の数多くの機能を包含するよう進化している。更に、前述の、より高速でかつ拡張的な機能のためにコンピュータ・システム全体において情報を転送するための高性能プロトコルが開発されている。例として、インテル社のＱｕｉｃｋｐａｔｈ  Ａｒｃｈｉｔｅｃｔｕｒｅは、データを高速伝送することができる高速キャッシュ・コヒーレント・シリアル・ポイント・ツー・ポイント階層型プロトコルのプロトコル・アーキテクチャを含む。しかし、前述のより高度なプロトコルが進化するにつれ、プロトコル・アーキテクチャの各階層の複雑度も増加している。
【０００３】
伝統的には、動作が正確であることを確実にするためのプロトコル・アーキテクチャの検証には、コーナー・ケース（すなわち、極端な動作点又は状態）の手作業の識別を伴う。前述のコーナー・ケースは、プロトコル実現形態の動作を検証するためにシステム内で引き起こされる。コーナー・ケースの代わりに、又は、場合によってはコーナー・ケースに加えて、任意の動作変数／状態を変えて、プロトコル・アーキテクチャをランダムに検証する。
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかし、前述のパラメータ及び変数は、複雑度が増加するにつれ、数が非常に大きくなる。例えば、複数のエージェントを有する複雑なプロトコルの場合、潜在的な状態の数が指数関数的に増える。その結果、個人が、潜在的な状態のカバレッジ空間を考察することは、より困難になる。更に、現在の検証手法は多くの場合、多数の状態のうちのどれが検証されたかを追跡することができない。よって、検証されるアーキテクチャの量における正確な信頼度を得ることは一層困難になる。
【課題を解決するための手段】
【０００５】
以下の説明では、本発明の徹底的な理解に資するために、特定のプロトコル・アーキテクチャ、特定のプロトコル動作変数／パラメータ、特定のモデル、特定の検証工程等の例などの数多くの具体的な詳細を記載している。しかし、本発明を実施するためには、前述の具体的な詳細を使用しなくてもよいことが当業者には明らかであろう。一方、相互接続プロトコル／実現形態、形式相互接続モデルの開発／内容、特定のクエリや、動作上の他の具体的な詳細などの周知の構成部分又は方法は、本発明を不必要に不明瞭にすることを避けるために詳細に記載していない。
【０００６】
本明細書及び特許請求の範囲記載の方法及び装置は、複雑なプロトコルの実現形態を効果的かつ効率的に検証するための検証ストラテジを提供する。特に、相互接続プロトコルの検証は、キャッシュ・コヒーレンス相互接続プロトコル（インテル社のＱｕｉｃｋｐａｔｈの技術仕様にほぼ従っているキャッシュ・コヒーレンス・プロトコルを含む高速ポイント・ツー・ポイント相互接続など）を参照して説明して、検証方法を例証する。しかし、本明細書及び特許請求の範囲記載の方法及び装置は、何れのプロトコル上、相互接続アーキテクチャ階層上、若しくは他の複数のエージェント／パラメータ・システム上でも実現することができ、何れのプロトコル、相互接続アーキテクチャ階層、若しくは他の複数のエージェント／パラメータ・システムと連係しても実現することができるので、前述に限定されない。
【発明を実施するための最良の形態】
【０００７】
本発明は、例示の目的で示しており、添付図面の図によって限定されることを意図するものでない。
【実施例】
【０００８】
図１を参照すれば、システムの構成部分を結合するための複数の相互接続の実施例を示す。図示したように、伝統的なマルチプロセッサ・システムの一部分を描いている。しかし、本明細書及び特許請求の範囲記載の検証方法は、何れのシステム（単一プロセッサのコンピュータ・システム、サーバ、組み込み型システム、モバイル・システム、及び複数の電気エージェントを有する他のシステムなど）においても利用することができる。
【０００９】
一実施例では、ハブ１２５はチップセットに似ている。多くの場合、チップセットは、２つの集積回路装置（メモリ・コントローラ・ハブ（ＭＣＨ）や相互接続コントローラ・ハブ（ＩＣＨ）など）を含む。一実施例では、ハブ１２５は、プロセッサ１０６、１１１、１１６及び１２１をメモリ１３０に結合するＭＣＨである。しかし、ハブ１２５は、プロセッサと他のシステム装置との間の通信を容易にする何れかの集積回路を含み得る。
【００１０】
図示したようなメモリ１３０は、実行時間中にアクセスする対象のコード、データ及び他の情報を保持するためのシステム・メモリを含む。システム・メモリの例には、ダイナミック・ランダム・アクセス・メモリ（ＤＲＡＭ）がある。しかし、ダブル・データ・レート（ＤＤＲ）メモリ、シンクロナス・ダイナミックＲＡＭ（ＳＤＲＡＭ）、バッファ付きメモリや、他の既知の記憶装置などの何れのメモリも利用することができる。更に、メモリ１３０は、システム・メモリに限定されず、フラッシュ・メモリ装置などの他の既知のメモリ装置を含み得る。
【００１１】
プロセッサ・ソケット１０５、１１０、１１５及び１２０は、プリント回路基板（ＰＣＢ）やマザーボードなどの回路基板にプロセッサ１０６、１１１、１１６及び１２１を結合する。多くの場合、ソケット及び対応するパッケージング手法（ランド・グリッド・アレイ（ＬＧＡ）、ピン・グリッド・アレイ（ＰＧＡ）、ボール・グリッド・アレイ（ＢＧＡ）や他の既知のソケット手法など）が利用される。プロセッサ１０６、１１１、１１６及び１２１は多くの場合、物理プロセッサとして表されるが、何れの型の処理要素（マイクロプロセッサ、組み込み型プロセッサ、マルチコア・プロセッサ、マルチスレッド・プロセッサや信号プロセッサなど）も含み得る。
【００１２】
図示したような相互接続１２６は、プロセッサ１０６、１１１、１１６及び１２１をハブ１２５に結合する。多くの場合、相互接続１２６は、フロント・サイド・バス（ＦＳＢ）として表される。検証は、相互接続１２６及びそのプロトコルを参照して説明しているが、本明細書及び特許請求の範囲記載の検証方法は、通信プロトコルの何れかの数及び型を実現する、エージェントを結合するＩ／Ｏ相互接続、メモリ・バスや他のリンクなどの相互接続の何れでも利用することができる。物理的には、相互接続１２６は、パラレル・バス、シリアル・バス、マルチドロップ・バス、ポイント・ツー・ポイント・バス、ガニング・トランシーバ・ロジック（ＧＴＬ）バス、ＧＴＬ＋バス、ダブル・データ・レート（ＤＤＲ）バス、差動バス、又は、相互接続の他の既知の物理層／実現形態を利用することができる。特定の例証的な実施例として、相互接続１２６は、高速シリアル・ポイントツーポイント相互接続を含む。
【００１３】
一実施例では、相互接続１２６は、階層化プロトコル・スタック・アーキテクチャを含む。相互接続アーキテクチャの例示的な階層には、装置間の物理的な電気接続を設けるための物理層、トランザクション／要求／パケットのシーケンシングを支援するためのリンク層、及び種々の型のトランザクション／要求／パケットを実現するためのトランザクション層が挙げられる。前述の階層は、ペリフェラル・コンポーネント・インターコネクト（ＰＣＩ）エクスプレスなどの相互接続アーキテクチャにおいて一般的である。しかし、他の階層又はプロトコルが、相互接続アーキテクチャの一部として存在し得る。例えば、インテル社のＱｕｉｃｋｐａｔｈ技術仕様にほぼ従う相互接続アーキテクチャは、キャッシュ・コヒーレンス・プロトコルなどの種々のトランザクション及び通信プロトコルを含む。
【００１４】
上述の通り、相互接続のためのプロトコルの検証には、入出力（Ｉ／Ｏ）バス、ペリフェラル・コンポーネント・インターコネクト（ＰＣＩ）又はＰＣＩエクスプレス・バスや、メモリ・バス（メモリ・バス１２７など）などの、プラットフォーム内の何れの相互接続も含まれ得る。ハブ１２５をメモリ１３０に接続するための物理メモリの一般的な例には、ＤＤＲベースのバス、ランダム・アクセス・メモリ（ＲＡＭ）ベースのバス、若しくは何れかの他の既知のメモリ・バス、又はメモリ・バスに適合された他のバスが挙げられる。各型のバスは、検証する対象のそれ自身の通信プロトコルと関連付けることができる。
【００１５】
更に、プロトコルの検証方法は、伝統的なデスクトップ型コンピュータ・システムの相互接続に限定されない。例えば、ネットワーク・プロトコル、無線アクセス・プロトコル、及び他の複雑な通信プロトコルを同様に検証することができる。したがって、物理的相互接続の検証であっても、相互接続プロトコルの検証であっても、他のプロトコルの検証であっても、検証の標的は、アーキテクチャ、検証オブジェクト、及び検証標的と表すことができる。
【００１６】
図２を参照すれば、検証する対象のアーキテクチャの考えられる状態のカバレッジ空間のカバレッジ・データベースの実施例を示す。上述の通り、検証する対象のアーキテクチャの語は、検証する対象のプロトコル・アーキテクチャ（例えば、検証する対象のキャッシュ・コヒーレンス・プロトコル）、検証する対象の他のプロトコル、検証する対象の物理的相互接続、又はそれらの組合せの検証を表し得る。
【００１７】
一実施例では、データベース２０１は記憶媒体２００に保持される。記憶媒体は、電子情報を保持することができる記憶装置（ディスク、ディスク・ドライブ、メモリ、テープ・ドライブ、外部記憶装置、一時メモリ、揮発性メモリ、不揮発性メモリ、他の記憶装置や、マシン・アクセス可能な／マシン読み取り可能な媒体など）の何れをも含む。マシン・アクセス可能な媒体は、データベース２０１に保持される情報などの情報を記憶媒体から、アクセスする対象のコンピュータ・システムに搬送又は伝送する搬送波又は他の電子伝送媒体を含み得る。
【００１８】
一実施例では、アーキテクチャのカバレッジ空間データベースは、動作中に遭遇し得る、プロトコル・アーキテクチャなどのアーキテクチャの複数の状態を含む。例として、カバレッジ・データベースは、アーキテクチャの構成拘束モデルなどの、アーキテクチャの実現形態の潜在的な状態を全て含む。しかし、別の例では、カバレッジ・データベースは、アーキテクチャ実現形態の考えられる状態の縮減された組を含む。
【００１９】
例えば、相互接続のプロトコル層の形式モデルが、その相互接続の実現形態特有のプロトコル・モデルに合わせられる。ここでは、変数／パラメータを変えて、実現形態特有のプロトコル内の別々の状態を実現する場合、変数の組それぞれは潜在的には、対称状態をもたらす対称の変数の組を有し得る。その結果、この例では、１つの対称状態のみがデータベース２０１内に維持され、対称的に縮減された相互接続状態の組が形成される。これは、一般に、カバレッジ空間としても表し得る。
【００２０】
検証のカバレッジ空間を非常に単純化した例として、キャッシュ・コヒーレント相互接続のキャッシュ・コヒーレント・プロトコルの形式モデルは、構成制約（プロトコル・エージェントの数、プロトコル・エージェントのタイプ等など）に基づいて合わせられる。キャッシュ・コヒーレンス・プロトコルの検証のためのカバレッジ空間は、プロトコル・エージェントそれぞれ及び／又はコヒーレンシ・プロトコルの種々の大局パラメータの種々のエージェント・パラメータに基づいて、考えられる状態、又は考えられる状態の対称的に縮減された組の全てを含む。
【００２１】
しかし、複雑なプロトコル又は相互接続の場合、パラメータ数は潜在的に、かなりの数に増加する。例えば、特定のプロトコル実現形態の場合、最大１００以上のパラメータが存在し得る。よって、各パラメータの別々の値の組合せそれぞれには、潜在的には、非常に大きな数の状態が（プロトコルの特定の実現形態についても）可能になる。
【００２２】
一実施例では、状態は、検証オブジェクトのパラメータ、装置、エージェント及び／又は他の構成部分の状態のスナップショットを表す。状態は、アーキテクチャ又は検証オブジェクトのアーキテクチャ状態としても表すことができる。別の例として、状態は、状態のスナップショットにおけるパラメータの値の組合せで規定される。よって、１００個のパラメータが、アーキテクチャについて識別された場合、上記１００個のパラメータの別々の値の組合せが全て、潜在的には、別々の状態をもたらす。
【００２３】
複雑なプロトコルの場合、状態は、多数のパラメータを表すことが多いので、キャッシュ・コヒーレンス・プロトコルの場合、状態の非常に単純化された例証的な例には、共有コヒーレンス状態にキャッシュ線を保持する１つのプロセッサ、無効状態にキャッシュ線を保持する２つのプロセッサが挙げられ、スヌープは、上記プロセッサの一方で受信される。ここでは、複数のプロトコル・エージェント、複数の状態に保持された複数のキャッシュ線、及び特定のデスティネーションで受信された要求／メッセージが存在している。したがって、この単純な例だけでも、かなり多くのパラメータが存在している。別の例証的な例では、データ・ペイロードを収容する書込トランザクションは潜在的には、他のパラメータ（書込のデスティネーション、書き込む対象のデータ・ペイロードに関連付けられたキャッシュ線の状態、祖語接続トラフィック、他のエージェントによる書込応答等）を変えることができるので、複数の状態をもたらす。
【００２４】
したがって、一実施例では、パラメータは、プロトコル、物理ロジック、装置、エージェント、又は、別々の状態に変えるか、又は入れることができる大局的な状態／変数内の何れかの要素を表す。特定の例として、キャッシュ・コヒーレンス・プロトコルを検証する場合、キャッシュ・エージェントのパラメータは、スヌープに対するキャッシュ応答を含む。ここでは、キャッシュ応答パラメータの一値は、スヌープされたキャッシュ線の、要求側の装置への転送を含み、キャッシュ応答パラメータの第２の値は、キャッシュ線をホーム・ノードに書き込む工程を含む。他の一般的なコヒーレンシ・プロトコル・パラメータには、各種のエージェント、エージェント応答、装置応答、相互接続応答、メッセージ応答、応答のタイプ、特定の動作に対する他の応答、応答のデスティネーション、メッセージ、メッセージのタイプ、メッセージのデスティネーション、要求、要求のタイプ、要求のデスティネーション、キャッシュのタイプ、キャッシュ状態、キャッシュの場所、レジスタ状態等が挙げられる。
【００２５】
しかし、物理的相互接続、通信プロトコルや他のプロトコルなどの何れのアーキテクチャは検証オブジェクトであり得るので、パラメータは、広い範囲の変数を包含し得る。潜在的なプロトコル関連パラメータを例証すれば、網羅的でないが、プロトコル・エージェントの数、プロトコル・エージェントのタイプ、エージェントのキャッシュ実現形態のタイプ、各種のプロトコル・エージェントの数、プロトコル・エージェントの型、プロトコル・エージェントの状態、プロトコル・エージェント内又はバス上の回路又はステ―ト・マシンの状態、エージェント識別子、プロトコル要求の数、要求タイプ、要求ソース、要求デスティネーション、要求の状態、参照された動作、動作のソース、参照されたアドレス、アクセスされたアドレス、アドレス位置の状態、データ・ペイロード、プロトコル・エージェントの状態、キャッシュの状態、キャッシュ線の状態、物理プロトコル状態パラメータ（電圧、周波数、電力状態や、他の物理プロトコル属性など）が挙げられる。
【００２６】
相互接続の物理層を検証する場合、相互接続の物理パラメータの例には、電圧、周波数、周期、スペクトル拡散、ジッタ、雑音等が挙げられる一方、他のパラメータには、相互接続関連ステート・マシンの状態、エージェントのタイプ、エージェントの状態、エージェント内のＩ／Ｏ回路の状態等が挙げられる。しかし、アーキテクチャ内の可変要素を何れもパラメータとみなし得る。
【００２７】
カバレッジ空間が指数関数的に増加し、個人が理解することが困難になるにつれ、一実施例では、データベース２０１は、相互接続アーキテクチャ／実現形態の考えられる状態のカバレッジ空間を保持する。図示したように、データベース２０１の各エントリ（エントリ２５０乃至２５７など）は、相互接続実現形態の考えられる状態を表す。したがって、エントリ２５０への参照は、フィールド２１０内に規定されたパラメータ値を有する状態２５０と同義である。ここでは、エントリ２５０のパラメータ値フィールド２１０は、状態２５０に対応する関連パラメータの数値を保持する。
【００２８】
一実施例では、パラメータ値フィールド２１０は、複数のフィールド２１１、２１２、２１３及び２１４に分割される。例として、データベース２０１は、３つのプロトコル・エージェントを有するコヒーレンシ・プロトコルの実現形態のカバレッジ空間を保持するものとする。ここでは、フィールド２１１乃至２１３は、３つのプロトコル・エージェントそれぞれに対応する。各フィールド内では、論理的にはサブフィールドとしてみることができる各数値は、予め定義されるか、又は、対応するパラメータと予め関連付けられる。
【００２９】
例えば、第１のエージェントのフィールド２１１では、フィールド２１１の第１の数値はエージェントのタイプを規定し、第２の数値は、第１のエージェントがホーム・ノードであるか否かを規定し、第３の数値は、キャッシュ線の状態を規定する等である。スヌープ／読み出しに対する応答などの、特定の要求／動作に対する応答は、潜在的には、数多くの差異を有する。例えば、別々の４つの応答を備えた応答は潜在的には、考えられる４つの組合せ（すなわち、１、２、３及び４）を有する２進の２ビットで表される。上記組合せはそれぞれ、考えられる応答を表す。
【００３０】
更に、フィールド２１４は、エージェント全ての大局パラメータを含む大局パラメータ・フィールドであり得る。例えば、スヌープに対する大局キャッシュ応答は、ホーム・ノードへの転送であり得る。そういうものとして、フィールド２１４内のパラメータ値は、前述のキャッシュ応答を表す。上記例は例証に過ぎず、如何なる数（数十、数百、又は数千など）のエージェント及びパラメータをも如何なる形式でもフィールド２１０において表すことができる。更に、種々の要素を表す上記既知の方法の何れも、フィールド２１０において利用することができる。
【００３１】
別の実施例では、フィールド２１０は複数のシーケンス値を保持し、フィールド２１０内の数値の所定の構造により、各パラメータ値が、対応するパラメータと関連付けられる。例として、フィールド２１０内の第１の数は合計エージェントの数を表し、第２の数はキャッシング・エージェントの数を表し、第３の数は、要求に対する、第１のエージェントによる応答を表し、第４の数は、要求に対する、第２のエージェントによる応答を表す等である。ここでは、パラメータをエージェントで分類する代わりに、パラメータは順次記載されている。しかし、パラメータを表す如何なる設計実現形態又は形式もデータベース２０１において利用することができる。
【００３２】
相互接続の複雑度が増加し、変数／パラメータの数が増加するにつれ、データベース２０１内に保持する対象の状態の数も大きく増加する。したがって、一実施例では、各エントリは、各エントリを一意に識別するためのトークン識別子フィールド２０５を含む。例えば、フィールド２１０内に保持される数値パラメータ値は状態２５０（すなわち、エントリ２５０）を規定し、エントリ２５０のトークンＩＤ２０５は、エントリ２５０のフィールド２１０内に保持される数値に基づく。
【００３３】
第１の例として、数値計算用アルゴリズムを利用して数値を結合して、対応するトークンＩＤを得る。したがって、百個の数値がパラメータ・フィールド２１０内に保持されている場合、百個又はその一部分の値を各エントリ２５０乃至２５７において結合して、エントリ２５０乃至２５７毎の一意のトークンＩＤ２０５を得る。パラメータは、別々の数値にわたって変えられるので、トークンＩＤは、フィールド２１０内のパラメータ値における変動に基づいて変わる。例えば、スヌープ・パラメータに対する応答が第１の応答（０として表すものとする）から第２の応答（１として表すものとする）に変えられた場合、トークン識別子も、数値パラメータ値の数学的な結合に基づいて変わる。如何なるアルゴリズムも利用して、数値パラメータ値をトークンＩＤに結合することができる。
【００３４】
一実施例では、各エントリ２５０乃至２５７は、マーキング・フィールド２１５も含む。マーキング・フィールド２１５は、マーキングされていない値などの第１の値を保持している場合、シミュレーション中、対応する状態に遭遇していないことを表す。例えば、マーキング・フィールド２１５がマーキングされていない場合、エントリ２５０（すなわち、状態２５０）は、シミュレーション中に遭遇していない。対照的に、エントリ２５０のマーキング・フィールド２１５が、マーキングされた値に更新された場合、状態２５０はシミュレーション中に遭遇している。したがって、シミュレーション中にマーキングすることにより、シミュレーション中に入った／遭遇した状態がどれであるか、及び遭遇していない状態がどれであるかを、その後、判定することが可能である。
【００３５】
その結果、検証オブジェクト（プロトコル、物理的相互接続、他の階層、又はアーキテクチャなど）のカバレッジ空間が生成され、潜在的には、検証に利用される。一実施例では、データベース２０１が、生成され、その後の検証のために記憶媒体上に備えられるか、又は上記記憶媒体を介して備えられる。ここでは、検証オブジェクトの実現形態の何れのレベルも、カバレッジ空間（すなわち、データベース２０１内に保持される考えられる状態）の生成のために規定することが可能である。
【００３６】
例えば、相互接続アーキテクチャの形式モードは、実現形態特有モデルにフィルタリングすることができる。実現形態特有モデルの制約に応じて、データベース２０１内の状態の数が変えられる。例えば、第１のモデルが、プロトコル・エージェントの数しか規定しない場合、多くの他のパラメータがなお変えられていることがあり得るので、カバレッジ空間が非常に大きいことがあり得る。対照的に、モデルが、エージェントの数、エージェントのタイプ、エージェントの相互接続、特定のプロトコル制限を規定する場合、カバレッジ空間を縮減することができる。更に、検証オブジェクトの考えられる状態を調査するようモデル検査器が実行されると、状態の完全な組又は縮減された組がデータベース２０１のエントリに格納される。データベース２０１は次いで、顧客などの別のユーザに供給して、プロトコル、相互接続、又は他の検証オブジェクトの検証を可能にすることができる。データベース２０１と同様なデータベースを利用した相互接続アーキテクチャを検証する検証方法を以下に説明する。
【００３７】
図３に移れば、アーキテクチャ（プロトコル・アーキテクチャ、物理的相互接続アーキテクチャ、相互接続プロトコル・ア―キテクチャや他のアーキテクチャ・システムなど）の検証中のアーキテクチャ状態カバレッジを確実にする方法のフロー図の実施例を描く。図３及び図４のフローは、ほぼ直列に、かつ特定の順序で示しているが、フローの何れも、並列に、又は別の順序で行うことができる。例えば、フロー４３０中のマーキングは多くの場合、シミュレーション４２５中に行われるが、シミュレーション後に行われてもよい。更に、汎用検査スイートのシミュレーションを、並列に、又はフロー４０５乃至４１５と完全に無関係に行うことができる。
【００３８】
更に、上記フローは何れも、マシンによってアクセス又は読み取り可能な媒体からのコードの実行の結果として行うことができる。マシン・アクセス可能な媒体又はマシン読み取り可能な媒体（製品など）は以下に更に詳細に説明する。したがって、コンパイラ、パーサ、又は他の実行可能なコードは、実行されると、命令、動作、関数呼出し、及び他の実行可能なコード又は構造を挿入して、以下のフローに示す動作を行うことができる。更に、一実施例では、図３及び図４を参照して説明したフローそれぞれを自動化することができる。一実施例では、自動化は、フロー内のタスクを行うためのスクリプト、パーサ、又は他のコードの実行を含む。更に、マスタ・コード又は他のコード自体は、次のフロー（やはり自動化してもよい）を呼び出すか、又は前述の次のフローを実行させることができる。
【００３９】
フロー３００では、検証オブジェクト（相互接続アーキテクチャ、プロトコル・アーキテクチャや、状態又は変数の検証の他の既知の標的など）の考えられる状態を求める。上述の通り、一実施例では、考えられる状態は、動作中に遭遇し得るアーキテクチャの状態を表す。ここで、考えられる状態は、パラメータ、変数、回路及びステート・マシンの状態、並びに、何れかの他の上述又は既知のパラメータのスナップショットを表す。
【００４０】
例えば、相互接続アーキテクチャの識別されたパラメータの特定値の結合により、単一の相互接続アーキテクチャ状態が生じ得る。例証すれば、コヒーレンス・プロトコルでは、単純化された例示的な状態は、３つのプロトコル・エージェント（一つのエージェントはキャッシュ線を保有状態に保持し、２つのエージェントはキャッシュ線を無効状態に保持する）、スヌープがホーム・ノードに書き込むための大局応答を含み、スヌープが受信される。ここでは、コヒーレンス・プロトコルは、規定された状態にある。しかし、他の変数／パラメータ（記載せず）が含められ、変えられた場合、前述の規定されたパラメータは事実上、クエリを形成する。クエリは論理的には、考えられる状態の部分集合空間（すなわち、他のパラメータを変えた、上記からの規定されたパラメータを有する状態）をみることができる。
【００４１】
一実施例では、相互接続アーキテクチャの形式モデルは、実現形態特有モデルにフィルタリングされるか、又は合わせられる。ここでは、形式モデルは、アーキテクチャ／プロトコルの規定（コヒーレンス・プロトコルが実現されるための制約の完全な形式モデル）を実施することができる。一実施例では、形式モデルは、インテル社のＱｕｉｃｋｐａｔｈの規定にほぼ従うコヒーレンス・プロトコルの形式モデルを含む。しかし、形式モデルは、プロトコル、アーキテクチャ、相互接続、相互接続階層、又は他の検証オブジェクトの何れのモデリングも含み得る。一実施例では、データベース２０１は、形式モデルの状態のカバレッジ空間を保持する。
【００４２】
しかし、完全な規定内で、相互接続アーキテクチャの特定の実現形態を利用することができる。その結果、形式モデルは、特定の実現形態の特定の構成制約に基づいてフィルタリングし、合わせ、かつ／又は修正することができる。例えば、コヒーレンス・プロトコルでは、エージェントの数、及び、エージェントのタイプ又は他の情報を規定することができる。実現形態特有モデルを得ると、モデル検査器又は他のツールは、相互接続アーキテクチャの考えられる状態のカバレッジ空間を求めるよう実行される。上述の通り、カバレッジ空間は、実現形態モデルの考えられる状態全て、又は、対称的に縮減された状態の組などの縮減された状態の組を含み得る。
【００４３】
次に、フロー３０５乃至フロー３１０では、汎用検査スイートが、シミュレーションのためにロードされ、実行される。一実施例では、シミュレーション環境は、レジスタ・トランスファ・レベル（ＲＴＬ）のシミュレーション環境を含む。例として、動作中のアーキテクチャの動作をシミュレートするためにＲＴＬ環境が生成される。汎用検査スイートは、コヒーレンス・プロトコルの別々のトレース及び状態を強調するために行い得る通常の動作を引き起こす／シミュレートする。例えば、特定の既知の困難なトランザクション又は構成を汎用検査スイートに含めて、動作中にプロトコルに障害が生じない旨を検査することができる。汎用検査スイートは、プロトコル状態のランダムな検証を可能にするための任意のケース、トラフィック及び活動も含み得る。汎用検査スイートの同様なシミュレーションを、物理的相互接続階層や他のプロトコルなどの何れかの検証オブジェクトに利用することができる。
【００４４】
フロー３１５では、汎用検査スイートの実行／シミュレーション中に遭遇されない考えられる状態の数のうちの複数に基づいたフィードバックを供給して、標的化された検査スイートを形成する。ここでは、フロー３１６で、シミュレーション中に遭遇しなかったか、又は入らなかった考えられるアーキテクチャ状態が求められる。一実施例では、図２のデータベース２０１と同様なデータベースが、この判定のために利用される。上述の通り、データベースは、考えられる状態（検証オブジェクト、又はその一部の縮減された部分の考えられる状態全てであり得る）のカバレッジ空間を保持することができる。
【００４５】
例として、シミュレーション中に遭遇した状態がデータベース内でマーキングされる。データベース２０１のトークンＩＤを利用して、データベースに索引付けし、正しいエントリにマーキングすることができる。したがって、シミュレーションが完了すると、入った状態は全て、データベース２０１においてマーキングされる。その結果、マーキングされていない、データベース２０１において保持された考えられる状態は何れも、シミュレーション中に遭遇していないものと判定される。
【００４６】
フロー３１７では、遭遇していない考えられる状態を標的化するために、標的化された検査スイートが判定される。一実施例では、遭遇していない状態を求めるためにデータベースがクエリされる。例えば、状態の大空間（すなわち、同じパラメータの特定の結合）に遭遇しない場合、穴又は間隙として表される。例として、第１のプロセッサが線を共有状態に保持し、第２のプロセッサが線を共有状態に保持し、スヌープが第３のプロセッサから受信される状態に全く遭遇しないものとする。前述の３つのパラメータのみが一定である１００個のパラメータを備えたデータベースにより、論理的には、遭遇されない状態（すなわち、前述のパラメータを含み、その他の９７個を変動させる状態全て）が多数もたらされる。すなわち、非常に大きな間隙又は穴が生じる。同様なパラメータを備えた多数の状態が、適切な動作を確実にするためにシミュレーション中に遭遇されなかったからである。
【００４７】
したがって、一実施例では、状態情報を形式モード又は他のモデルにフィードバックして、初期状態から非遭遇状態に到達するためのトレースを判定する。すなわち、非遭遇状態に到達するためにアーキテクチャにおいて何が生じる必要があるかが判定される。この情報を次いで利用して、標的化された検査スイートを構築する。これは、潜在的には、非遭遇状態又はその一部分に到達するためにシミュレーションにおいてトレースを引き起こす。
【００４８】
ここでは、汎用検査スイートを上記トレース情報又は他の情報で修正して非遭遇状態を標的化することができる。しかし、標的検査スイートは、遭遇されない考えられる状態全てを標的化する必要がある訳でない。実際に、考えられる多くの状態を備えた非常に複雑な相互接続では、考えられる状態全てを標的化することは非常に困難であり得る。よって、状態全てに遭遇するよりも、一定の信頼度（すなわち、検証された状態の一定の割合）に到達することのみが目標であり得る。いくつかの穴／間隙における少なくとも一部の状態が検証されることを確実にするための一定割合の間隙／穴の信頼度目標も存在し得る。その結果、特定のユーザ解析、又はプログラムによる解析による、検証のために穴、間隙、又はコーナー・ケースを包含するよう標的化するために、遭遇していない考えられる状態の部分集合を求めることができる。
【００４９】
上述の通り、標的検査スイートは、実行されると、汎用検査スイートの実行／シミュレーション中に遭遇されない考えられるアーキテクチャ状態を引き起こすか、又はシミュレートすることが意図されている。更に、遭遇されない考えられる状態の部分集合を、物理的なユーザにより、又は、コードの実行によって合理的に選択して、間隙、穴、コーナー・ケース、識別された困難な状態、又は他の考えられる状態を標的化することができる。
【００５０】
フロー３１０に戻れば、標的化検査スイートは、汎用検査スイートと同様に実行／シミュレートされる。ここでは、新たに遭遇した状態も、データベースにおいてマーキングすることができる。更に、フィードバック・ループ３１５は、未だ遭遇していない他の考えられる状態を更に標的化するか、又は先行して標的化されたが、シミュレーション中に遭遇していない考えられる状態を再標的化するよう再帰的に反復することができる。
【００５１】
図４に移れば、アーキテクチャの効率的なシミュレーション検証カバレッジを確実にする方法／ストラテジのフロー図の非常に単純化された特定の例証的な実施例を描く。フロー４０５乃至４１７では、形式モデルが、アーキテクチャの特定の実施例の構成制約に基づいてフィルタリングされ、モデル検査器が、フィルタリングされた実現形態の特定のモデルの考えられる状態のカバレッジ空間を調査するよう実行され、カバレッジ空間がデータベース４１７に記憶される。
【００５２】
上述の通り、カバレッジ空間は、アーキテクチャ／検証オブジェクトの考えられるアーキテクチャ状態全て、又は、対称的に縮減された状態の組などの縮減された状態の組を含み得る。更に、データベース４１７は、図２のデータベース２０１と似ており、データベースのエントリはカバレッジ空間のアーキテクチャ状態に対応する。ここで、各エントリは、エントリに対応するアーキテクチャ状態を規定する、アーキテクチャのパラメータの少なくとも複数のパラメータ値、前述の複数のパラメータ値に基づいたトークン識別子（ＩＤ）、及びマーキング・フィールドを含む。
【００５３】
ここでは、検証及びシミュレーションは、並列に行われるか、データベースの生成直後に行われるか、又は後に行われる。例えば、プロトコル・アーキテクチャなどのアーキテクチャの規定又はモデルを供給する企業は、更に、又は、あるいは、フロー４１７からのデータベースを顧客に供給して、相互接続の効率的なシミュレーション及び検証を可能にすることができる。汎用検査スイート及び他のコード／スクリプトも供給することができる。
【００５４】
しかし、データベースが作成され、かつ／又は供給された後、フロー４２５で、フロー４２０からの汎用検査スイートがシミュレートされる。例証された実施例では、レジスタ・トランスファ・レベル（ＲＴＬ）シミュレーションが行われる。しかし、何れの言語、コード、シミュレータ、又は他の既知のシミュレーション／検証ツールを利用して、アーキテクチャの動作をシミュレートすることもできる。シミュレーション中又はシミュレーション後、遭遇されたアーキテクチャの状態が、フロー４１７のデータベース内のフロー４３０においてマーキングされる。上述の通り、状態／エントリ毎のトークンＩＤを利用してデータベース４１７に索引付けすることができる。汎用データベース鍵などの何れかの他の鍵を代わりに利用してデータベースに索引付けすることもできる。
【００５５】
ここでは、フロー４２５でシミュレーション中に遭遇しなかった／入らなかった、マーキングされていない、データベースに保持されたカバレッジ空間の考えられる状態がフロー４３５で判定される。この判定に基づいて、フロー４４０で、シミュレーション中に遭遇していないカバレッジ空間の考えられる状態を標的化するために、標的化された検査スイートが策定／判定される。前述の通り、間隙及び穴、並びに他の状態を、自動化ソフトウェアを利用して標的化し、モデルにフィードバックして、前述の状態を標的化するためのトレース／情報を判定することができる。遭遇されていない考えられる状態全てを標的化する訳でないことがあり得る。標的化された状態を、コーナー状態、既知の問題状態、及び状態カバレッジにおける間隙／穴、並びに、ランダムに標的化された特定数の状態に遭遇するよう合理的に選択して更なるカバレッジを設けることができるからである。標的化検査スイートを次いで、シミュレーション・フロー４２５において利用し、新たに遭遇されるデータベース・エントリ／状態がマーキングされる。考えられる状態の十分な検証カバレッジが達成されるまでこの処理を再帰的に行うことができる。
【００５６】
したがって、上述の通り、複雑なプロトコル、複雑な相互接続や、他の複雑な検証オブジェクトなどの複雑なアーキテクチャの効率的な、かつ自動化された検証方法を本明細書及び特許請求の範囲で説明している。従来は、プロトコル及び相互接続は複雑でなく、ユーザはカバレッジ空間を理解し、検証中の信頼度を確実にするために十分な検査スイートを供給することが可能であった。しかし、データベースを使用してアーキテクチャ状態のカバレッジ空間を保持することにより、複雑なアーキテクチャは電子形式で理解することができる。更に、シミュレーション中に遭遇した状態にマーキングすることにより、遭遇した状態の数及び遭遇していない状態の数も理解することができる。これに基づいて、標的化検査スイートを策定して、カバレッジ空間の十分な検証が達成されることを確実にすることができる。その結果、アーキテクチャの検証信頼度は、理解することができるのみならず、非シミュレーション状態の再帰的標的化によっても達成することができる。
【００５７】
本明細書及び特許請求の範囲記載の値は、数、状態、論理状態、又は２進の論理状態の何れかの既知の表現を含む。多くの場合、論理レベル、ロジック値、又は論理値の使用は、１及び０としても表され、これは単に２進の論理状態を表す。例えば、１は高論理レベルを表す一方、０は低論理レベルを表す。一実施例では、トランジスタ又はフラッシュ・セルなどの記憶セルは、単一の論理値又は複数の論理値を保持することができることがあり得る。しかし、コンピュータ・システムにおける値の他の表現を使用している。例えば、１０（１０進数）は、２進値１０１０及び１６進値Ａとして表すこともできる。したがって、値は、コンピュータ・システムに保持することができる情報の表現を何れも含む。
【００５８】
更に、状態は、値、又は値の一部分で表すことができる。例として、論理１などの第１の値はデフォルト値又は初期値を表し得る一方、論理０などの第２の値は非デフォルト値を表し得る。更に、一実施例では、リセット及びセットの語はそれぞれ、デフォルト値又は状態、及び更新された値又は状態を表す。例えば、デフォルト値は潜在的には、高論理値（すなわち、リセット）を含む一方、更新された値は潜在的には、低論理値（すなわち、セット）を含む。値の組合せの何れを利用して、何れの数の状態を表すこともできる。
【００５９】
上述の方法、ハードウェア、ソフトウェア、ファームウェア又はコードは、処理エレメントによって実行可能なマシン・アクセス可能な媒体上又はマシン読み取り可能な媒体上に記憶された命令又はコードを介して実現することができる。マシン・アクセス可能な／読み取り可能な媒体は、マシン（コンピュータや電子システムなど）によって読み取り可能な形式の情報を供給（すなわち、記憶及び／又は送信）する機構を何れも含む。例えば、マシン・アクセス可能な媒体には、ランダム・アクセス・メモリ（ＲＡＭ）（スタティックＲＡＭ（ＳＲＡＭ）やダイナミックＲＡＭ（ＤＲＡＭ）など）、ＲＯＭ、磁気記憶媒体若しくは光記憶媒体、フラッシュ・メモリ装置、電気記憶装置、光記憶装置、音響記憶装置、又は他の形式の伝搬信号（例えば、搬送波、赤外信号、ディジタル信号）、記憶装置等が挙げられる。例えば、マシンは、伝搬信号上で伝送される対象の情報を保持することができる媒体から、搬送波などの伝搬信号を受信することにより、記憶装置にアクセスすることができる。
【００６０】
本明細書全体の、「ｏｎｅ  ｅｍｂｏｄｉｍｅｎｔ」又は「ａｎ  ｅｍｂｏｄｉｍｅｎｔ」への言及は、本願の実施例に関して説明した特定の構成、構造又は特性が本発明の少なくとも一実施例に含まれていることを意味している。よって、本明細書全体の種々の箇所に記載された「ｉｎ  ｏｎｅ  ｅｍｂｏｄｉｍｅｎｔ」又は「ｉｎ  ａｎ  ｅｍｂｏｄｉｍｅｎｔ」は、必ずしも、同じ実施例を全て表している訳でない。更に、特定の構成、構造、又は特性を、１つ又は複数の実施例において何れかの適切なやり方で組み合わせることができる。
【００６１】
上記明細書では、特定の例示的な実施例を参照して詳細な説明を記載している。しかし、特許請求の範囲記載の本発明のより広い趣旨及び範囲から逸脱しない限り、種々の修正及び変更を行うことができることは明らかとなるであろう。よって、本願の明細書及び図面は、限定的な意味合いでなく、例証の意味合いでみるものとする。更に、実施例及び例示的な文言を上述の通り、使用していることは、同じ実施例又は同じ例を必ずしも表しておらず、別々の実施例及び別個の実施例、並びに、潜在的には同じ実施例を表すことができる。
【図面の簡単な説明】
【００６２】
【図１】システムの構成部分を結合するための別々の相互接続を含むシステムの実施例を示す図である。
【図２】アーキテクチャの構成のカバレッジ空間データベースを保持するための記憶媒体の実施例を示す図である。
【図３】アーキテクチャの検証カバレッジを確実にする方法のフロー図の実施例を示す図である。
【図４】相互接続アーキテクチャの検証カバレッジを確実にする別の方法のフロー図の実施例を示す図である。
【符号の説明】
【００６３】
２００  記憶媒体
２０１  データベース
【図１】
2009157928.tif 000003
【図２】
2009157928.tif 000004
【図３】
2009157928.tif 000005
【図４】
2009157928.tif 000006