【誤訳訂正書】
【提出日】平成24年8月3日(2012.8.3)
【誤訳訂正１】
【訂正対象書類名】特許請求の範囲
【訂正対象項目名】全文
【訂正方法】変更
【訂正の内容】
【特許請求の範囲】
【請求項１】
デジタル回路のインプリメンテーション記述を読み込むステップと、
前記デジタル回路のアーキテクチャ記述を読み込むステップと、
同じ初期値を用いた同じプログラムの実行を通じて、前記アーキテクチャ記述によって記述されたデータ転送の前記アーキテクチャシーケンスが、前記インプリメンテーション記述によって実行された前記データ転送のインプリメンテーションシーケンスにマッピング可能であることをデモンストレートすることにより、マッピングが、全単射であることと、前記デジタル回路のデータ転送のアーキテクチャシーケンスの時間的な順序が、前記デジタル回路のデータ転送のインプリメンテーションシーケンスの時間的な順序に対応することとを確認する、デモンストレートするステップと、
前記デモンストレートするステップにおける前記インプリメンテーション記述との前記アーキテクチャ記述の等価性の検証の結果を出力するステップとを含む、デジタル回路のインプリメンテーション記述とのデジタル回路のアーキテクチャ記述の等価性をフォーマルに検証する方法。
【請求項２】
データ転送の前記アーキテクチャシーケンスからデータ転送の前記インプリメンテーションシーケンスへの前記マッピングが、同じデータがデータメモリの同じアドレスから転送されること、或いは、同じデータがデータメモリの同じアドレスへ転送されることを確認する請求項１の方法。
【請求項３】
前記デジタル回路のデータ転送の前記インプリメンテーションシーケンスが、アクセスプロトコル記述によって記述される請求項１又は２の方法。
【請求項４】
前記デモンストレートするステップが、
マッピングされた割り込み信号を有するデータ転送の前記アーキテクチャシーケンス信号のマッピングが、前記割り込み信号によって影響を受けるデータ転送の前記インプリメンテーションシーケンスに対応するために、前記同じプログラムの実行を通じて、前記インプリメンテーション記述の割り込み信号の動作が、前記アーキテクチャ記述の割り込み信号の動作にマッピング可能であることをデモンストレートする請求項１の方法。
【請求項５】
前記デモンストレートするステップが、
対応情報を読み込むステップと、
読み込まれた前記対応情報を使用して、複数のデモンストレートステップを生成するステップとを含み、前記デモンストレートステップのうちの１つが、前記同じプログラムのサイクルの実行後の、アーキテクチャ記述とインプリメンテーション記述との対応を検証する請求項１に係る方法。
【請求項６】
前記アーキテクチャ記述および前記インプリメンテーション記述の等価でないペアについて誤った検証を出力しないように、前記対応情報を使用する請求項５に係る方法。
【請求項７】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージのストール条件を含む請求項５又は６に係る方法。
【請求項８】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージの取り消し条件を含む請求項５又は６に係る方法。
【請求項９】
前記対応情報が、前記インプリメンテーション記述の、１つ以上のパイプラインステージの分類を含む請求項５又は６に係る方法。
【請求項１０】
前記対応情報が、前記インプリメンテーション記述からプログラムカウンタを読み込むための関数を含む請求項５又は６に係る方法。
【請求項１１】
前記対応情報が、前記インプリメンテーション記述のインプリメンテーションレジスタ内の値を、前記アーキテクチャ記述の対応するアーキテクチャレジスタにマッピングするための、１つ以上の仮想レジスタを含む請求項５又は６に係る方法。
【請求項１２】
１つ以上の前記仮想レジスタが、命令シーケンスの順番で、前記インプリメンテーション記述の１つ以上のパイプラインステージをテストするための関数であり、１つ以上の前記仮想レジスタが、関連するデータを持つ１つ以上の前記パイプラインステージのうちの１つから、少なくとも１つのパイプライン値を返し、１つ以上の前記パイプラインステージの何れもが関連するデータを持たない場合、１つ以上の前記仮想レジスタが、対応する前記アーキテクチャレジスタを実行する前記インプリメンテーションレジスタの値を返す請求項１１に係る方法。
【請求項１３】
１つ以上の前記仮想レジスタが、１つ以上のサブ関数から生成された関数である請求項１２に係る方法。
【請求項１４】
前記仮想レジスタが仮想レジスタファイル内に組織される請求項１１〜１３の１の請求項に係る方法。
【請求項１５】
前記デモンストレートするステップがさらに、前記同じプログラムのそれぞれのサイクルが、インプリメンテーションクロックサイクルの有限数によって実行されることを確認する請求項１に係る方法。
【請求項１６】
前記同じプログラムの前記サイクルが、命令又は割り込みを含む請求項１５に係る方法。
【請求項１７】
複数の前記デモンストレートステップを生成する前記ステップが、
プロパティを生成するステップと、
生成された前記プロパティのすべてを証明するために、或いは、生成された前記プロパティのうち誤りであるものの少なくとも１つを識別するために、生成された前記プロパティを検証するステップとを含む請求項５に係る方法。
【請求項１８】
プロパティを生成する前記ステップが、
１つ以上のプレースホルダーを含むプロパティスキーマにアクセスするステップと、
１つ以上の前記プレースホルダーを、前記対応情報からの値に置き換えるステップとを含み、それによって、少なくとも１つの生成されたプロパティを生成する請求項１７に係る方法。
【請求項１９】
生成された前記プロパティのうち誤りであるものの少なくとも１つの前記識別を停止する請求項１７又は１８の１の請求項に係る方法。
【請求項２０】
生成された前記プロパティのサブセットが作成され、前記サブセットのメンバプロパティのそれぞれが、インプリメンテーションサイクルのうちの１つの実行を記述する請求項１７に係る方法。
【請求項２１】
前記インプリメンテーションサイクルが、前記インプリメンテーション記述によって実行される命令、もしくは前記インプリメンテーション記述によって実行される割り込みのいずれかである請求項２０に係る方法。
【請求項２２】
インプリメンテーションサイクルのそれぞれについて、前記インプリメンテーションサイクルを記述する少なくとも１つのプロパティが存在する請求項２０又は２１に係る方法。
【請求項２３】
生成された前記プロパティの前記サブセットが、前記インプリメンテーションサイクルの前記実行の結果として、１つ以上の仮想レジスタの変化を指摘する請求項２０又は２１に係る方法。
【請求項２４】
生成された前記プロパティの前記サブセットが、
どのように前記インプリメンテーションが命令を要求し、いつどのように前記インプリメンテーションがプログラムカウンタを変更するのか；
いつどのようにパイプライン中の命令が取り消されるのか；
いつ、前記インプリメンテーション記述のどの前記データ転送が、前記インプリメンテーションによって実行されるのか；
を検証するためのプロパティから構成され、
前記命令の前記実行に引き続き、前記インプリメンテーションが、さらなるインプリメンテーションサイクルを実行する状態にある請求項２０〜２３の１の請求項に係る方法。
【請求項２５】
前記結果が、
生成されたプロパティのすべての証明の表示、
前記アーキテクチャ記述と前記インプリメンテーション記述との前記等価性の確認、
生成された前記プロパティのうちの１つが誤りであることの表示、或いは、
生成された前記プロパティのうち誤りであるもののリストのいずれかである請求項１〜２４のいずれか１の請求項に係る方法。
【請求項２６】
前記同じプログラムが命令メモリ内にある請求項１〜２５のうちのいずれかの請求項に係る方法。
【請求項２７】
前記アーキテクチャ記述が、プロセッサのアーキテクチャ記述であり、前記インプリメンテーション記述が、プロセッサのインプリメンテーション記述である請求項１〜２６のうちのいずれかの請求項に係る方法。
【請求項２８】
前記インプリメンテーション記述を読み込む前記ステップが、前記インプリメンテーション記述の最初の部分を読み込むことを含み、
前記アーキテクチャ記述を読み込む前記ステップが、前記アーキテクチャ記述の最初の部分を読み込むことを含み、
前記インプリメンテーション記述の前記最初の部分と前記アーキテクチャ記述の前記最初の部分との前記等価性を検証するための前記対応情報を使用して、且つ、前記等価性がデモンストレートされる場合に、前記インプリメンテーション記述の残りの部分と前記アーキテクチャ記述の残りの部分とを読み込む請求項５に係る方法。
【請求項２９】
デジタル回路のインプリメンテーション記述のインプリメンテーションレジスタの値から、前記デジタル回路のアーキテクチャ記述のアーキテクチャレジスタの対応する値へのマッピングを含む仮想レジスタファイル。
【請求項３０】
デジタル回路のインプリメンテーション記述を読み込むステップと、
前記デジタル回路のアーキテクチャ記述を読み込むステップと、
対応情報を読み込むステップと、
プロパティのセットを生成するステップと、
プロパティの前記セットを検証することにより、生成された前記プロパティのすべてが適合することを示す、或いは、生成された前記プロパティのうち誤りであるものの少なくとも１つを識別する、検証するステップと、
前記検証するステップにおける前記インプリメンテーション記述との前記アーキテクチャ記述の等価性の前記検証の結果を出力するステップとを含む、デジタル回路のインプリメンテーション記述とのデジタル回路のアーキテクチャ記述の等価性を検証する方法。
【請求項３１】
前記検証が、同じ初期値を用いた同じプログラムの実行を通じて、前記アーキテクチャ記述によって記述されたデータ転送の前記アーキテクチャシーケンスが、前記インプリメンテーション記述によって実行された前記データ転送のインプリメンテーションシーケンスにマッピングされることをデモンストレートすることにより、マッピングが、全単射であることと、前記デジタル回路のデータ転送のアーキテクチャシーケンスの時間的な順序が、前記デジタル回路のデータ転送のインプリメンテーションシーケンスの時間的な順序に対応することとを確認する請求項３０の方法。
【請求項３２】
プロパティの前記セットを検証する前記ステップが、シミュレーションの結果に関する前記インプリメンテーションプロパティのシミュレーションを含む請求項３０の方法。
【請求項３３】
データ転送のアーキテクチャシーケンスからデータ転送のインプリメンテーションシーケンスへのマッピングが、同じデータがデータメモリの同じアドレスから転送されること、或いは、同じデータがデータメモリの同じアドレスへ転送されることを確認する請求項３０の方法。
【請求項３４】
前記デジタル回路のデータ転送の前記インプリメンテーションシーケンスが、アクセスプロトコル記述によって記述される請求項３１〜３３の方法。
【請求項３５】
前記デモンストレートするステップが、
前記同じプログラムの実行を通じて、前記インプリメンテーション記述の割り込み信号の動作が、前記アーキテクチャ記述の割り込み信号の動作にマッピング可能であることをデモンストレートする請求項３１の方法。
【請求項３６】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージのストール条件を含む請求項３０に係る方法。
【請求項３７】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージの取り消し条件を含む請求項３０に係る方法。
【請求項３８】
前記対応情報が、前記インプリメンテーション記述の、１つ以上のパイプラインステージの分類を含む請求項３０に係る方法。
【請求項３９】
前記対応情報が、前記インプリメンテーション記述からプログラムカウンタを読み込むための関数を含む請求項３０に係る方法。
【請求項４０】
前記対応情報が、前記インプリメンテーション記述のインプリメンテーションレジスタ内の値を、前記アーキテクチャ記述の対応するアーキテクチャレジスタにマッピングするための、１つ以上の仮想レジスタを含む請求項３０に係る方法。
【請求項４１】
１つ以上の前記仮想レジスタが、命令シーケンスの順番で、前記インプリメンテーション記述の１つ以上のパイプラインステージをテストするための関数であり、１つ以上の前記仮想レジスタが、関連するデータを持つ１つ以上の前記パイプラインステージのうちの１つから、少なくとも１つのパイプライン値を返し、１つ以上の前記パイプラインステージの何れもが関連するデータを持たない場合、１つ以上の前記仮想レジスタが、対応する前記アーキテクチャレジスタを実行する前記インプリメンテーションレジスタの値を返す請求項４０に係る方法。
【請求項４２】
１つ以上の前記仮想レジスタが、１つ以上のサブ関数から生成された関数である請求項４０又は４１に係る方法。
【請求項４３】
前記仮想レジスタが仮想レジスタファイル内に組織される請求項４０〜４１の１の請求項に係る方法。
【請求項４４】
前記デモンストレートするステップがさらに、前記同じプログラムのそれぞれのサイクルが、インプリメンテーションクロックサイクルの有限数によって実行されることを確認する請求項３１に係る方法。
【請求項４５】
前記同じプログラムの前記サイクルが、命令又は割り込みを含む請求項４４に係る方法。
【請求項４６】
プロパティを生成する前記ステップが、
１つ以上のプレースホルダーを含むプロパティスキーマにアクセスするステップと、
１つ以上の前記プレースホルダーを、前記対応情報からの値に置き換えるステップとを含み、それによって、少なくとも１つの生成されたプロパティを生成する請求項３０に係る方法。
【請求項４７】
生成された前記プロパティのうち誤りであるものの少なくとも１つの前記識別を停止する請求項３０〜４６のいずれか１の請求項に係る方法。
【請求項４８】
生成された前記プロパティのサブセットが作成され、前記サブセットのメンバプロパティのそれぞれが、インプリメンテーションサイクルのうちの１つの実行を記述する請求項３０に係る方法。
【請求項４９】
前記インプリメンテーションサイクルが、前記インプリメンテーション記述によって実行される命令、もしくは前記インプリメンテーション記述によって実行される割り込みのいずれかである請求項４８に係る方法。
【請求項５０】
インプリメンテーションサイクルのそれぞれについて、前記インプリメンテーションサイクルを記述する少なくとも１つのプロパティが存在する請求項４８又は４９に係る方法。
【請求項５１】
生成された前記プロパティの前記サブセットが、前記インプリメンテーションサイクルの前記実行の結果として、１つ以上の仮想レジスタの変化を指摘する請求項４８又は４９に係る方法。
【請求項５２】
生成された前記プロパティの前記サブセットが、
どのように前記インプリメンテーションが命令を要求し、いつどのように前記インプリメンテーションがプログラムカウンタを変更するのか；
いつどのようにパイプライン中の命令が取り消されるのか；
いつ、前記インプリメンテーション記述のどの前記データ転送が、前記インプリメンテーションによって実行されるのか；
を検証するためのプロパティから構成され、
前記命令の前記実行に引き続き、前記インプリメンテーションがさらなるインプリメンテーションサイクルを実行可能な状態にある請求項４８〜５１の１の請求項に係る方法。
【請求項５３】
前記結果が、
生成されたプロパティのすべての証明の表示、
前記アーキテクチャ記述と前記インプリメンテーション記述との前記等価性の確認、
生成された前記プロパティのうちの１つが誤りであることの表示、或いは、
生成された前記プロパティのうち誤りであるもののリストのいずれかである請求項３０に係る方法。
【請求項５４】
前記同じプログラムが命令メモリ内にある請求項３１、３５および４４の１の請求項に係る方法。
【請求項５５】
前記アーキテクチャ記述が、プロセッサのアーキテクチャ記述である請求項３０〜５４のいずれか１の請求項に係る方法。
【請求項５６】
前記インプリメンテーション記述を読み込む前記ステップが、前記インプリメンテーション記述の最初の部分を読み込むことを含み、
前記アーキテクチャ記述を読み込む前記ステップが、前記アーキテクチャ記述の最初の部分を読み込むことを含み、
前記インプリメンテーション記述の前記最初の部分と前記アーキテクチャ記述の前記最初の部分との前記等価性を検証するための前記対応情報を使用して、且つ、前記等価性がデモンストレートされる場合に、前記インプリメンテーション記述の残りの部分と前記アーキテクチャ記述の残りの部分とを読み込む請求項３０に係る方法。
【請求項５７】
デジタル回路のアーキテクチャ記述を読み込むステップと、
前記デジタル回路のアクセスプロトコル記述を読み込むステップと、
対応情報を読み込むステップと、
カバレッジ・ポイントのセットを生成するステップと、
カバレッジ・ポイントの前記セットをシミュレーションモニタに変換するステップと、
前記シミュレーションモニタをシミュレーションに含めるステップとを含む、プロセッサインプリメンテーションのシミュレーションベースの検証のための機能的なカバレッジ・ポイントのフルセットを生成する方法。