(57)【要約】      （修正有）【課題】より少ないユーザ入力で高レベルの品質のプロセッサ用フォーマル検証を記述する。【解決手段】インプリメンテーション記述を読み込むステップと、アーキテクチャ記述を読み込むステップと、マッピングが、全単射であることと、データ転送のアーキテクチャシーケンスの時間的な順序が、データ転送のインプリメンテーションシーケンスの時間的な順序に対応することとを保証するように、同じ初期値を用いた同じプログラムの実行を通じて、前記アーキテクチャ記述によって記述されたデータ転送の前記アーキテクチャシーケンスが、前記インプリメンテーション記述によって実行された前記データ転送のインプリメンテーションシーケンスにマッピング可能であることを実証するステップと、前記インプリメンテーション記述との前記アーキテクチャ記述の等価性の検証の結果を出力するステップとを含む。【選択図】図１
2008181490.tif 000002
【特許請求の範囲】
【請求項１】
インプリメンテーション記述を読み込むステップと、
アーキテクチャ記述を読み込むステップと、
マッピングが、全単射であることと、データ転送のアーキテクチャシーケンスの時間的な順序が、データ転送のインプリメンテーションシーケンスの時間的な順序に対応することとを保証するために、同じ初期値を用いた同じプログラムの実行を通じて、前記アーキテクチャ記述によって記述されたデータ転送の前記アーキテクチャシーケンスが、前記インプリメンテーション記述によって実行された前記データ転送のインプリメンテーションシーケンスにマッピング可能であることを実証するステップと、
前記インプリメンテーション記述との前記アーキテクチャ記述の等価性の検証の結果を出力するステップとを含む、インプリメンテーション記述とのアーキテクチャ記述の等価性をフォーマルに検証する方法。
【請求項２】
データ転送の前記アーキテクチャシーケンスからデータ転送の前記インプリメンテーションシーケンスへの前記マッピングが、同じデータがデータメモリの同じアドレスから転送されること、或いは、同じデータがデータメモリの同じアドレスへ転送されることを保証する請求項１の方法。
【請求項３】
データ転送の前記インプリメンテーションシーケンスが、アクセスプロトコル記述によって記述される請求項１又は２の方法。
【請求項４】
前記実証するステップが、
マッピングされた割り込み信号を有するデータ転送の前記アーキテクチャシーケンス信号のマッピングが、前記割り込み信号によって影響を受けるデータ転送の前記インプリメンテーションシーケンスに対応するために、前記同じプログラムの実行を通じて、前記インプリメンテーション記述の割り込み信号の動作が、前記アーキテクチャ記述の割り込み信号の動作にマッピング可能であることを実証する請求項１の方法。
【請求項５】
前記実証するステップが、
対応情報を読み込むステップと、
読み込まれた前記対応情報を使用して、複数の実証ステップを生成するステップとを含み、前記実証ステップのうちの１つが、前記同じプログラムのサイクルの実行後の、アーキテクチャ記述とインプリメンテーション記述との対応を検証する請求項１に係る方法。
【請求項６】
前記アーキテクチャ記述および前記インプリメンテーション記述の等価でないペアについて誤った検証を出力しないように、前記対応情報を使用する請求項５に係る方法。
【請求項７】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージのストール条件を含む請求項５又は６に係る方法。
【請求項８】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージの取り消し条件を含む請求項５又は６に係る方法。
【請求項９】
前記対応情報が、前記インプリメンテーション記述の、１つ以上のパイプラインステージの分類を含む請求項５又は６に係る方法。
【請求項１０】
前記対応情報が、前記インプリメンテーション記述からプログラムカウンタを読み込むための関数を含む請求項５又は６に係る方法。
【請求項１１】
前記対応情報が、前記インプリメンテーション記述のインプリメンテーションレジスタ内の値を、前記アーキテクチャ記述の対応するアーキテクチャレジスタにマッピングするための、１つ以上の仮想レジスタを含む請求項５又は６に係る方法。
【請求項１２】
１つ以上の前記仮想レジスタが、命令シーケンスの順番で、前記インプリメンテーション記述の１つ以上のパイプラインステージをテストするための関数であり、１つ以上の前記仮想レジスタが、関連するデータを持つ１つ以上の前記パイプラインステージのうちの１つから、少なくとも１つのパイプライン値を返し、１つ以上の前記パイプラインステージの何れもが関連するデータを持たない場合、１つ以上の前記仮想レジスタが、対応する前記アーキテクチャレジスタを実行する前記インプリメンテーションレジスタの値を返す請求項１１に係る方法。
【請求項１３】
１つ以上の前記仮想レジスタが、１つ以上のサブ関数から生成された関数である請求項１２に係る方法。
【請求項１４】
前記仮想レジスタが仮想レジスタファイル内に組織される請求項１１〜１３の１の請求項に係る方法。
【請求項１５】
前記実証するステップがさらに、前記同じプログラムのそれぞれのサイクルが、インプリメンテーションクロックサイクルの有限数によって実行されることを確認する請求項１に係る方法。
【請求項１６】
前記同じプログラムの前記サイクルが、命令又は割り込みを含む請求項１５に係る方法。
【請求項１７】
複数の前記実証ステップを生成する前記ステップが、
プロパティを生成するステップと、
生成された前記プロパティのすべてを証明するために、或いは、生成された前記プロパティのうち誤りであるものの少なくとも１つを識別するために、生成された前記プロパティを検証するステップとを含む請求項５に係る方法。
【請求項１８】
プロパティを生成する前記ステップが、
１つ以上のプレースホルダーを含むプロパティスキーマにアクセスするステップと、
１つ以上の前記プレースホルダーを、前記対応情報からの値に置き換えるステップとを含み、それによって、少なくとも１つの生成されたプロパティを生成する請求項１７に係る方法。
【請求項１９】
生成された前記プロパティのうち誤りであるものの少なくとも１つの前記識別を停止する請求項１７又は１８の１の請求項に係る方法。
【請求項２０】
生成された前記プロパティのサブセットが作成され、前記サブセットのメンバプロパティのそれぞれが、インプリメンテーションサイクルのうちの１つの実行を記述する請求項１７に係る方法。
【請求項２１】
前記インプリメンテーションサイクルが、前記インプリメンテーション記述によって実行される命令、もしくは前記インプリメンテーション記述によって実行される割り込みのいずれかである請求項２０に係る方法。
【請求項２２】
インプリメンテーションサイクルのそれぞれについて、前記インプリメンテーションサイクルを記述する少なくとも１つのプロパティが存在する請求項１７に係る方法。
【請求項２３】
生成された前記プロパティの前記サブセットが、前記インプリメンテーションサイクルの前記実行の結果として、１つ以上の仮想レジスタの変化を指摘する請求項２０又は２１に係る方法。
【請求項２４】
生成された前記プロパティの前記サブセットが、
どのように前記インプリメンテーションが命令を要求し、いつどのように前記インプリメンテーションがプログラムカウンタを変更するのか；
いつどのように前記パイプライン中の命令が取り消されるのか；
いつ、前記インプリメンテーション記述のどの前記データ転送が、前記インプリメンテーションによって実行されるのか；
を検証するためのプロパティから構成され、
前記命令の前記実行に引き続き、前記インプリメンテーションが、さらなるインプリメンテーションサイクルを実行する状態にある請求項２０〜２３の１の請求項に係る方法。
【請求項２５】
前記結果が、
生成された前記プロパティのすべての前記証明の表示、
前記アーキテクチャ記述と前記インプリメンテーション記述との前記等価性の確認、
生成された前記プロパティのうちの１つが誤りであることの表示、或いは、
生成された前記プロパティのうち誤りであるもののリストのいずれかである上記請求項のいずれか１の請求項に係る方法。
【請求項２６】
前記同じプログラムが命令メモリ内にある上記請求項のうちのいずれかの請求項に係る方法。
【請求項２７】
前記アーキテクチャ記述が、プロセッサのアーキテクチャ記述であり、前記インプリメンテーション記述が、プロセッサのインプリメンテーション記述である上記請求項のうちのいずれかの請求項に係る方法。
【請求項２８】
前記インプリメンテーション記述を読み込む前記ステップが、前記インプリメンテーション記述の最初の部分を読み込むことを含み、
前記アーキテクチャ記述を読み込む前記ステップが、前記アーキテクチャ記述の最初の部分を読み込むことを含み、
前記インプリメンテーション記述の前記最初の部分と前記アーキテクチャ記述の前記最初の部分との前記等価性を検証するための前記対応情報を使用して、且つ、前記等価性が実証される場合に、前記インプリメンテーション記述の残りの部分と前記アーキテクチャ記述の残りの部分とを読み込む請求項５に係る方法。
【請求項２９】
インプリメンテーション記述のインプリメンテーションレジスタの値から、アーキテクチャ記述のアーキテクチャレジスタの対応する値へのマッピングを含む仮想レジスタファイル。
【請求項３０】
インプリメンテーション記述を読み込むステップと、
アーキテクチャ記述を読み込むステップと、
対応情報を読み込むステップと、
プロパティのセットを生成するステップと、
生成された前記プロパティのすべてが適合することを示すために、或いは、生成された前記プロパティのうち誤りであるものの少なくとも１つを識別するために、プロパティの前記セットを検証するステップと、
前記インプリメンテーション記述との前記アーキテクチャ記述の等価性の前記検証の結果を出力するステップとを含む、インプリメンテーション記述とのアーキテクチャ記述の等価性を検証する方法。
【請求項３１】
前記検証が、マッピングが、全単射であることと、データ転送のアーキテクチャシーケンスの時間的な順序が、データ転送のインプリメンテーションシーケンスの時間的な順序に対応することとを保証するために、同じ初期値を用いた同じプログラムの実行を通じて、前記アーキテクチャ記述によって記述されたデータ転送の前記アーキテクチャシーケンスが、前記インプリメンテーション記述によって実行された前記データ転送のインプリメンテーションシーケンスにマッピングされることを実証する請求項３０の方法。
【請求項３２】
プロパティの前記セットを検証する前記ステップが、前記シミュレーションの結果に関する前記インプリメンテーションプロパティのシミュレーションを含む請求項３０の方法。
【請求項３３】
データ転送の前記アーキテクチャシーケンスからデータ転送の前記インプリメンテーションシーケンスへの前記マッピングが、同じデータがデータメモリの同じアドレスから転送されること、或いは、同じデータがデータメモリの同じアドレスへ転送されることを保証する請求項３０の方法。
【請求項３４】
データ転送の前記インプリメンテーションシーケンスが、アクセスプロトコル記述によって記述される請求項３０〜３３の方法。
【請求項３５】
前記実証するステップが、
前記同じプログラムの実行を通じて、前記インプリメンテーション記述の割り込み信号の動作が、前記アーキテクチャ記述の割り込み信号の動作にマッピング可能であることを実証する請求項３０の方法。
【請求項３６】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージのストール条件を含む請求項３０に係る方法。
【請求項３７】
前記対応情報が、前記インプリメンテーション記述の、１つ又は複数のパイプラインステージの取り消し条件を含む請求項３０に係る方法。
【請求項３８】
前記対応情報が、前記インプリメンテーション記述の、１つ以上のパイプラインステージの分類を含む請求項３０に係る方法。
【請求項３９】
前記対応情報が、前記インプリメンテーション記述からプログラムカウンタを読み込むための関数を含む請求項３０に係る方法。
【請求項４０】
前記対応情報が、前記インプリメンテーション記述のインプリメンテーションレジスタ内の値を、前記アーキテクチャ記述の対応するアーキテクチャレジスタにマッピングするための、１つ以上の仮想レジスタを含む請求項３０に係る方法。
【請求項４１】
１つ以上の前記仮想レジスタが、命令シーケンスの順番で、前記インプリメンテーション記述の１つ以上のパイプラインステージをテストするための関数であり、１つ以上の前記仮想レジスタが、関連するデータを持つ１つ以上の前記パイプラインステージのうちの１つから、少なくとも１つのパイプライン値を返し、１つ以上の前記パイプラインステージの何れもが関連するデータを持たない場合、１つ以上の前記仮想レジスタが、対応する前記アーキテクチャレジスタを実行する前記インプリメンテーションレジスタの値を返す請求項４０に係る方法。
【請求項４２】
１つ以上の前記仮想レジスタが、１つ以上のサブ関数から生成された関数である請求項４０又は４１に係る方法。
【請求項４３】
前記仮想レジスタが仮想レジスタファイル内に組織される請求項４０〜４１の１の請求項に係る方法。
【請求項４４】
前記実証するステップがさらに、前記同じプログラムのそれぞれのサイクルが、インプリメンテーションクロックサイクルの有限数によって実行されることを確認する請求項３０に係る方法。
【請求項４５】
前記同じプログラムの前記サイクルが、命令又は割り込みを含む請求項４４に係る方法。
【請求項４６】
プロパティを生成する前記ステップが、
１つ以上のプレースホルダーを含むプロパティスキーマにアクセスするステップと、
１つ以上の前記プレースホルダーを、フェイルセーフ対応情報からの値に置き換えるステップとを含み、それによって、少なくとも１つの生成されたプロパティを生成する請求項３０に係る方法。
【請求項４７】
生成された前記プロパティのうち誤りであるものの少なくとも１つの前記識別を停止する請求項３０〜４６のいずれか１の請求項に係る方法。
【請求項４８】
生成された前記プロパティのサブセットが作成され、前記サブセットのメンバプロパティのそれぞれが、インプリメンテーションサイクルのうちの１つの実行を記述する請求項３０に係る方法。
【請求項４９】
前記インプリメンテーションサイクルが、前記インプリメンテーション記述によって実行される命令、もしくは前記インプリメンテーション記述によって実行される割り込みのいずれかである請求項４８に係る方法。
【請求項５０】
インプリメンテーションサイクルのそれぞれについて、前記インプリメンテーションサイクルを記述する少なくとも１つのプロパティが存在する請求項３０に係る方法。
【請求項５１】
生成された前記プロパティの前記サブセットが、前記インプリメンテーションサイクルの前記実行の結果として、１つ以上の仮想レジスタの変化を指摘する請求項４８又は４９に係る方法。
【請求項５２】
生成された前記プロパティの前記サブセットが、
どのように前記インプリメンテーションが命令を要求し、いつどのように前記インプリメンテーションがプログラムカウンタを変更するのか；
いつどのように前記パイプライン中の命令が取り消されるのか；
いつ、前記インプリメンテーション記述のどの前記データ転送が、前記インプリメンテーションによって実行されるのか；
を検証するためのプロパティから構成され、
前記命令の前記実行に引き続き、前記インプリメンテーションが実行可能な状態にある請求項４８〜５１の１の請求項に係る方法。
【請求項５３】
前記結果が、
生成された前記プロパティのすべての前記証明の表示、
前記アーキテクチャ記述と前記インプリメンテーション記述との前記等価性の確認、
生成された前記プロパティのうちの１つが誤りであることの表示、或いは、
生成された前記プロパティのうち誤りであるもののリストのいずれかである請求項３０に係る方法。
【請求項５４】
前記同じプログラムが命令メモリ内にある請求項３０〜５３の１の請求項に係る方法。
【請求項５５】
前記アーキテクチャ記述が、プロセッサのアーキテクチャ記述である請求項３０〜５４のいずれか１の請求項に係る方法。
【請求項５６】
前記インプリメンテーション記述を読み込む前記ステップが、前記インプリメンテーション記述の最初の部分を読み込むことを含み、
前記アーキテクチャ記述を読み込む前記ステップが、前記アーキテクチャ記述の最初の部分を読み込むことを含み、
前記インプリメンテーション記述の前記最初の部分と前記アーキテクチャ記述の前記最初の部分との前記等価性を検証するための前記対応情報を使用して、且つ、前記等価性が実証される場合に、前記インプリメンテーション記述の残りの部分と前記アーキテクチャ記述の残りの部分とを読み込む請求項３０に係る方法。
【請求項５７】
アーキテクチャ記述を読み込むステップと、
アクセスプロトコル記述を読み込むステップと、
対応情報を読み込むステップと、
カバレッジ・ポイントのセットを生成するステップと、
カバレッジ・ポイントの前記セットをシミュレーションモニタに変換するステップと、
前記シミュレーションモニタをシミュレーションに含めるステップとを含む、プロセッサインプリメンテーションのシミュレーションベースの検証のための機能的なカバレッジ・ポイントのフルセットを生成する方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はディジタルハードウェアの検証の分野に関する。
【背景技術】
【０００２】
ハードウェア機能検証
ディジタルハードウェアの検証は、集積回路の生産の１ステップである。ディジタルハードウェアの検証がディジタルハードウェア内のバグをすべて取り除くのに失敗する場合、ディジタルハードウェア用の生産プロセスは、その高い固定費で再開される必要があり得る。また、そのディジタルハードウェアを組み込んでいる製品の市場への導入が、遅延を被るであろう。
【０００３】
ディジタルハードウェアのデザインプロセスの１ステップは機能検証であり、それにより、ディジタルハードウェア回路の最初の記述が確認され、回路が常に意図する通りに動作するか否かを確認する。回路記述は、いくつかのハードウェア記述言語（例えば、VHDL、Verilog或いはSystemVerilog）のＲＴＬ記述として与えられる。一般に、現在の検証方法は、回路デザイン中の機能的なバグのすべてを識別するとは限らない。機能的なバグが発見されないままである理由は、次のように分類され得る。
●  刺激されなかったバグ：回路デザインに適用される刺激が、刺激されなかったバグを動作させて、回路チェッカーの入力部に至らせるのに失敗するので、これら機能的なバグは見つからない。
●  見落とされたバグ：これら機能的なバグは、チェッカーの入力に対して刺激され繁殖される。しかし、チェッカーが、見落とされたバグを識別するように設計されていない。
●  誤って容認されたバグ：これら機能的なバグは、回路デザインの仕様に対する、実装者および検証エンジニアによる一致した誤解から生じる。
【０００４】
シミュレーションによる検証
機能検証のための主な方法はシミュレーションである。シミュレーションベースの検証方法は、発見されないバグに関する３つの種類すべての傾向を有する。シミュレータ速度とテスト下にある回路のリアルタイム実行との間に１０６倍以上の係数の違いがあるため、シミュレーションは、機能的なバグのすべてを刺激するのに失敗する。従って、シミュレーションが、プロジェクトの利用可能な時間内で、回路デザインを徹底的に検証するために必要な刺激のすべてを展開することができるとは限らない。シミュレーション・カバレッジ・メトリクスは、この状況を救済しない。シミュレーション・カバレッジ・メトリクスは、回路設計全域のうち、制限された検証キャパシティの割り当てにおいてのみ助けとなり得る。
【０００５】
したがって、見落とされたバグの問題は、一般に、検証プランニングによって取り扱われる。検証タスクは、回路の仕様およびアーキテクチャの検査によって、共通のデザインパターンを適切なアサーションに関連づけることによって、或いは、回路設計者に、回路内の信号間の特に重要な関係に注意することを依頼することによって特定される。得られる検証タスクの完全性は、通常、ヒューマンエラーにより危険にさらされる。したがって、実行者は、未対処の検証ニーズに対する新しい眼識を捕らえるために、検証プロセスの全体にわたって、この検証プランニングを「動的に」しておく。
【０００６】
フォーマル機能検証
フォーマル検証は、シミュレーションベースの検証の代わりとされている。フォーマル機能検証では、ＲＴＬ記述の適切な動作を保証するために、いわゆるプロパティが回路デザインに対して証明される。フォーマル検証は、数学的な証明の方法を使用する。したがって、フォーマル検証は、あたかも回路があらゆる入力刺激で刺激されたかのように動作する[BCDM86]。したがって、上記した分類の用語において、フォーマル検証は、検証が終わった後のデザインにおいて、刺激されなかったバグの存在を回避する。
【０００７】
近年、フォーマル検証は、１セットのプロパティが、回路の入出力動作[BB05]全体を正確に検査することを保証するアプローチによって補完されてきた。そのため、そのプロパティのセットは「コンプリート」と称される。上記した分類の用語において、それは、検証後のデザインにおいて、見落とされたバグの存在を回避する。
【０００８】
フォーマル等価性検証
フォーマル機能検証に加えて、フォーマル等価性検証[BW99]がある。フォーマル等価性検証のゴールは、ＲＴＬ記述が設計され検証された後のデザインの、プロセスステップを検証することである。これらデザインプロセスステップの検証は、デザインプロセスステップ前後の回路記述の比較を必要とする。例えば、合成ステップを検証するために、ＲＴＬ記述は、合成されたネットリストと形式的に比較される。その簡単なユーザインタフェースにより、今日の等価性の確認は、同じデザインの２つの記述を比較するために最も広く用いられているアプローチである。
【０００９】
フォーマル等価性検証において使用されるアルゴリズムは、同じデザインの２つの記述の各々からオートマトンを抽出し、２つのオートマトン中の対応する入力ビット、出力ビットおよび状態ビットのペアを特定し、そして、２つの記述中の対応する状態ビットおよび出力ビットの、次の状態関数および出力関数を比較することによって、同じデザインのこれら２つの記述を比較する。これは組み合わせ等価性検証と呼ばれる。両方の回路表現が同じ状態エンコードを有する場合、組み合わせ等価性検証が唯一適用可能である。
【００１０】
プロセッサ検証
一般的なタスク
通常、プロセッサは、プロセッサによって実行されるアセンブラコードを記述するプログラマが、プロセッサのハードウェア説明書を詳細に理解する必要のないように開発されている。それよりも、プロセッサが次の命令の実行を開始する前に、あたかも１つの命令が完全に実行されたかのように、プログラマがプロセッサをみなせることで十分である。プロセッサのこのモデルは、アーキテクチャ、或いはプロセッサのアーキテクチャ記述と呼ばれ、以下でより詳細に記述されるであろう。
【００１１】
効率性の理由で、プロセッサは、例えばパイプラインといった、プロセッサが複数の命令を同時に実行する方法で実装される。これは、シーケンシャル化メカニズムが、パイプラインの効果をユーザに見えなくするように、或いは、プロセッサの効率的な動作を保証するように設計されることを必要とする。そのようなシーケンシャル化メカニズムは、例えば、フォワーディング、ストーリング、或いは推測的実行であり、以下に記述されるであろう。これらシーケンシャル化メカニズムは、プロセッサのＲＴＬ記述で記述される。以下では、ＲＴＬ記述はインプリメンテーション記述と呼ばれるであろう。
【００１２】
プロセッサについての検証問題は、インプリメンテーションが、アーキテクチャが示唆する方法でプログラムを実際に実行することを示すことである。機能検証タスクが、シーケンシャル化メカニズムを含むＲＴＬ記述を検証するので、この検証問題は機能検証タスクである。しかしながら、この機能検証タスクは、同じ回路の２つの記述、即ちアーキテクチャ記述とインプリメンテーション記述との間の等価性検証タスクとして見ることもできる。更に、この等価性検証タスクは、現在知られている等価性検証タスクのアプローチをはるかに越える。この理由は、プロセッサのアーキテクチャ記述をインプリメンテーション記述に変換するデザインステップが、人間の創造性と、パイプライン化、フォワーディング、命令の推測的実行、或いはストーリングのような手の込んだメカニズムの導入とを必要とすることである。特に、プロセッサのアーキテクチャ記述とインプリメンテーション記述とは、回路のタイミングにおいて異なる。プロセッサのインプリメンテーション記述における１つの命令の完了と、同じプロセッサにおける次の命令との間の時間差は、幅広く変化し得る。命令実行の完了順序がプログラム中の命令シーケンスと異なるように、スーパースカラ・プロセッサにおいては、一方の命令実行が、スーパースカラ・プロセッサ内の他方の命令実行を追い越すことができる。アーキテクチャ記述とインプリメンテーション記述との間の詳細な時相関係は、通常、プログラマにとって重要ではない。プログラマは、プログラムを記述する際、命令の巨視的な平均スループットに興味がある。
【００１３】
プロセッサのインプリメンテーション記述とアーキテクチャ記述との間の等価性検証は、割り込みによって悪化する。プロセッサが、入力信号上で適切な値を受信すると、割り込みがプロセッサに到着する。プロセッサの内部状態に依存して、プロセッサは、割り込みを受理するか否かを決定する。割り込みを受理すると、プロセッサは割り込みを実行するであろう。通常、この割り込み実行は、プロセッサによって既に開始された命令実行を置き換える。割り込み実行の一部は、プログラムの別の部分、即ち割り込みサービスルーチンの実行に切り換えることである。
【００１４】
インプリメンテーションを行う間、設計者によって、割り込みが到着する場合にプロセッサが実行する命令のどの命令が、その割り込み実行によって置き換えられなければならないかに関する決定が下される。この決定は、等価性検証の際に考慮されなければならない。
【００１５】
プロセッサ検証
最先端技術による産業上のプロセッサ検証は、[BB06]に記述されている。シミュレーションベースの検証についての一般的なアイデアは、インプリメンテーション記述およびアーキテクチャ記述の両方に同じプログラムを実行させ、次に、インプリメンテーション記述およびアーキテクチャ記述の両方において、プロセッサとデータメモリとの間の通信トラフィックを比較することである。このアプローチは、各々のインタフェースにおいて観測され得るものに基づいたインプリメンテーションおよびアーキテクチャの検査により、プロセッサ検証を実行する。バグは、インプリメンテーションおよびアーキテクチャのメモリへのトラフィックが互いに逸脱する場合に発見される。
【００１６】
プロセッサを検証するために使用されるプログラムは、アーキテクチャ記述およびインプリメンテーション記述で提供される。プログラムは、特別に開発されるか、ランダムに生成されるか、或いは、例えばオペレーティングシステムのブートといったアプリケーションプログラムから導かれる。このいわゆる「ブラックボックス」アプローチに起因する問題が、割り込みに関係する。比較は、インプリメンテーション記述およびアーキテクチャ記述の対応する時点において、割り込みが遅れずに到着することを必要とする。インプリメンテーション記述およびアーキテクチャ記述における割り込みの正確な対応は、多くの場合、検証エンジニアによって手動で提供される。このことは退屈であり、エラーとなる傾向を有する。
【００１７】
多くの場合、シミュレーションベースの検証は、プロセッサのインタフェース信号を通じてプロセッサを検査するだけでなく、プロパティが保持する内部信号間の関係について確認する。これら内部信号のプロパティは、時相論理表現であり、それらは、インプリメンテーションのあらゆるクロックサイクルについて満たされると予想され、一般にアサーションと呼ばれる。アサーションを使用する検証アプローチは、アサーションベースの検証[FKL03]と称される。多くの場合、アサーションは、インプリメンテーション記述を開発する設計エンジニアによって提供される。プロパティが満たされない場合、シミュレーションは、プロセッサのインタフェース信号においてバグが観測可能になるかなり前に、エラー、もしくは設計者にバグの識別を可能にする警告メッセージを発行する。
【００１８】
プロセッサのインプリメンテーション中に、信頼度が一旦或るレベルに到達すると、２つの異なる命令シーケンスを使用して或る結果を計算し、これら或る結果を比較する自己テストプログラムもまた適用される。
【００１９】
しかしながら、以前に議論されたように、発見されないバグが刺激されなかったか、或いは見落とされたかのどちらかの理由で、シミュレーションベースのアプローチは、発見されないバグの危険性を被る。
【００２０】
フォーマル検証のほとんどの応用例は、原則としてプロパティ中の矛盾をすべて識別するプロパティのフォーマル検証に集中する。しかしながら、上記したバグ分類の点に関して、フォーマル検証は、プロパティがバグを見落とし得るという問題について考慮していない。
【００２１】
フォーマル検証のプロセッサへの応用例は、既に学術的に研究された。BurchとDill[BD94]は、コントロールパス検証についてのアイデア、即ち、単純なパイプラインにおいて、プロセッサがどのようにどのデータを結合するかを決定する部分の検証を発展させた。しかしながら、BurchとDillは、データパス、即ち、コントロールパスからの信号に依存してデータを実際に転送又は結合する部分を全く考慮しなかった。本発明は、コントロールパスおよびデータパスを含むプロセッサ全体の検証を可能にする。スーパースカラ若しくはアウトオブオーダプロセッサへのいくつかの拡張が開発されている[VB00,PJB99,BCBZ02]。しかしながら、これら文献に記述されたアプローチは、特定のデザインの特定の部分にのみ注目する。即ち、それらは、アーキテクチャ記述に対するインプリメンテーション記述の完全な検証を提供しない。さらに、発明として提供される自動化の程度は一般的に低く、効率的なデバッグ環境と統合されていない。
【００２２】
プロセッサ検証に対する最も高度なアプローチは、完全性アプローチ[BB05]に基づく。この目的のために、アーキテクチャ記述を捕らえるプロパティが記述されなければならない。これらプロパティが、デザインに対して証明されるべきである。プロパティがバグを見落とさないことが、完全性チェッカーを使用して示されなければならない。これは、完全なフォーマル検証において、刺激されなかったバグもしくは見落とされたバグが、設計中に残らないことを保証する。
【発明の開示】
【００２３】
既に設計されたインプリメンテーションのフォーマル検証
本発明は、より少ないユーザ入力で高レベルの品質を導く、プロセッサ用のフォーマル検証を記述する。プロパティの開発に代えて、設計者は、アーキテクチャ記述と、データバスおよび命令バス上の通信のためのプロトコル情報と、デザインプロセス中で利用可能な情報を捕らえる、いわゆる対応情報とを提供することだけをしなければならない。要求されたユーザ入力の明確な構造は、例えばアーキテクチャ記述の形式化を単一の作業ステップで可能にし、このことは、誤ってバグを受理する危険性を大幅に低減する。
【００２４】
対応情報は、フェイルセーフに従う方式で開発される。不適切な対応情報が提供される場合であっても、検証は、アーキテクチャとインプリメンテーションとが等価であると誤って主張しないであろう。不適切な対応情報は、検証に、違いを誤って報告させ得ることが注目されるべきである。
【００２５】
インプリメンテーションの設計と平行したフォーマル検証
最先端技術に記述されるように、プロセッサが完全に設計された後、得られる検証プロセスが適用され得る。こうした事後の検証に加えて、本発明は、デザインプロセスに平行した検証プロセスも可能にする。それは、フォーマルな証明を使用するステップ・バイ・ステップ方式のプロセッサ開発が、あらゆるステップを検証することを可能にする。
【００２６】
このアプローチは、アーキテクチャ記述[SCLA+04][SHNB+04]からプロセッサ用のプログラムを開発するために必要とされるソフトウェアを生成する、プロセッサ開発ツールを補完する。それらは、例えば、
●  シミュレータ
●  デバッガ
●  アセンブラ
●  逆アセンブラ
●  リンカ
●  コンパイラ
である。
【００２７】
シミュレーション
本発明の方法は、プロパティの生成を必要とする。これら生成されたプロパティもまた、シミュレーションベースのアプローチにおいて確認され得る。シミュレーションベースのアプローチは、アサーションベースの検証において標準的な手続である。このことは、アーキテクチャ記述およびインプリメンテーション記述をシミュレートし、次に、アーキテクチャ記述およびインプリメンテーション記述の両方のメモリトラフィックを比較するアプローチに対して、いくつかの利点を有する。
●  インプリメンテーションの割り込みからアーキテクチャの割り込みへの明確で単純なマッピング
●  プロセッサが実行する命令シーケンスの識別
●  バグが命令又は割り込みの実行を妨げる場合、シミュレータがインプリメンテーション記述を実行し、命令の実行又はインプリメンテーションを記述するプロパティを評価すると、バグが見つかるであろう。これは、最先端技術に係るアプローチよりも早く、したがって、容易なデバッギングを可能にする。最先端技術のアプローチでは、バグの影響は、バグが観測可能になる前に、プロセッサ状態で長い間格納され得る。このことは、バグの追跡の困難さを保証する結果となる。
●  発見されないバグの分類の点において、検証がバグを見落とさない傾向を有することが証明され得る。
【００２８】
これら特性をもって、本アプローチは、シミュレーション用の一般的なアサーションベースの検証アプローチを越える。
【００２９】
専門用語および表記法
時相論理ＩＴＬ
本発明は、以下に示される時相論理ＩＴＬで記述されるであろう。しかしながら、本発明はこの時相論理に制限されない。本発明の手続もまた、例えばＬＴＬ、ＰＳＬ或いはＳＶＡといった、他のすべての線形時相論理を使用して適用され得る。
【００３０】
時相論理は、インプリメンテーション記述の、複数のプロパティによる複数の動作的な様相間の関係を記述するために使用される。次の表現、即ち、ＩＴＬ言語の若干の修正では、プロパティチェッカ[BS01]の入力言語が使用されるであろう。この言語では、複数の時点を参照することにより、時間的な様相が記述される。そのような時点は、同期式デジタル回路中のサイクルに対応する。
【００３１】
ＩＴＬの核心は、次の３つのフォームのうちの１つの論理行で構成される。
at <time point>: <Boolean condition>;
during [<time point1>, <time point2>]: <Boolean condition>;
within [<time point1>, <time point2>]: <Boolean condition>;
第１のフォームは明示された時点において、第２のフォームは区間内のすべての時点について、そして、第３のフォームは区間内の少なくとも１つの時点について、ブール条件の妥当性を要求する。区間が空の場合、第２のフォームは自明のこととして満たされ、第３のフォームは自明のこととして満たされない。
【００３２】
標準のオペレータについて、特定の時点Tにおけるブール条件は、時間Tにおける部分的な表現を評価し、そのオペレータに従ってそれら部分的な表現を組み合わせることにより評価される。この評価は、いくつかの部分的な表現がいくつかの信号によって与えられるまで、部分的な表現を分解する。このような場合において、時間Tにおけるその信号のその値が使用される。フォームnext(Term,n)又はprev(Term,n)の部分的な表現を評価するために、時点T+n又はT-nのそれぞれにおいて、表現Termが実行されるであろう。フォームTerm@T’の部分的な表現を評価するために、時点T’においてタームTermが評価される。
【００３３】
ブール演算式について、以下のオペレータは<=で記述され、以上のオペレータは>=で記述され、不等のオペレータは/=で記述され、含意のオペレータは->で表示される。区間は[a,b]で記述され境界を含む。ブール演算の結果について、値１および真が同義語として用いられ、同様に、値０および偽が同義語として用いられるであろう。
【００３４】
時点は、任意であるが時間tにおける固定された点に関連して、或いは、tに関連してそれ自身が定義される時間変数に関連して明示される。時間変数は、次の表現のリストによって宣言される。
【００３５】
T1 = B1 + n1 .. m1,
T2 = B2 + n2 .. m2,
....;
これら表現において、Biは、t、或いは、上記したリスト中で宣言された、j<iの別の時間変数Tjのいずれかである。時間変数に許される値の割り当ては、上記の与えられた条件を満たさなければならない。即ち、Bi+ni<=Ti<=Bi+miが真でなければならない。miは無限大であることができ、その場合、それぞれの宣言は、
Ti >= Bi + ni
或いは、
Ti> Bi + ni
に置き換えられる。
【００３６】
時間変数は、検査下にある回路がどのようにその環境と同期するかを記述するために使用される。これについて、時間変数Tiをセットするために、次のフォームの表現が使用される。
【００３７】
during [Bi + ni, Ti - 1]: signal /= value;
at         Ti:      signal = value;
論理行は、次のように条件を形成する。最も単純な場合では、条件は論理行を表す。２つの条件の連続は、それらの論理積に対応する。
【００３８】
パラメータ化された条件から形成される表現
for each j in m .. n:
Condition(j)
end for each;
は
Condition(m);
Condition(m+1);
...
Condition(n);
のように扱われなければならない。n<mの場合、上記表現は自明のこととして、条件真に適合しなければならない。
【００３９】
ブール演算式について、表現
for each j in m .. n:
Expression(j)
end for each;
は
Expression(m) and
Expression(m+1) and
... and
Expression(n);
のように扱われなければならない。条件次第で部分的な表現はマクロに要約されることができ、必要であれば、マクロはパラメータを持つことができる。
【００４０】
プロパティは次のフォームを有する。
【００４１】
property <name>;
for timevars: <time variable declaration>;
assume:
<condition 1>;
prove:
<condition 2>;
end property;
<condition 1>は仮定部分と呼ばれ、<condition 2>はプロパティの証明部分と呼ばれる。仮定部分のそれぞれは仮定と呼ばれるであろう。tのすべての値と、<time variable declaration>において明示される時間変数のすべての値とについて仮定部分が満たされ、且つ、証明部分も満たされる場合、プロパティは満たされる。反対の例は、インプリメンテーション記述の動作と、時点tと、<time variable declaration>において明示された、仮定部分を満たすが証明部分を満たさない時間変数についての値のセットとを示す。
【００４２】
仮定部分又は証明部分を形成する論理行は、フォーム<label>のカットポイントによって割り込みされ得る。この場合、仮定内の<label>のすべてについて、個別の証明が実行されるであろう。結果として生じるプロパティは、仮定部分および証明部分中のすべての連続する行をカットすることにより引き出される。その結果生じるプロパティは、部分的なプロパティと呼ばれ、<property_name>.<label>によって参照されるであろう。
【００４３】
プロパティがエントリー「dependencies:」を含む場合、このエントリー内に明示されたブーリアンマクロは、リセット後のすべての時点についての仮定として扱われるべきである。
【００４４】
left_hookおよびright_hookは、プロパティへの付加的なエントリーである。これらエントリーは、t+<offset>或いは<TimeVariable>+<offset>のフォームの表現を用いて、時点を参照する。エントリーは、次のセクションに記述された方法で、実行トレースに一致するチェーンをプロパティがどのように形成するかを記述する。
【００４５】
専門用語
termプロパティは、回路動作の様相間の動作関係について記述する時相論理表現に使用されるであろう。フォーマル検証ツールによる検査は証明と呼ばれる。フォーマル検証ツールが、プロパティの適合を決定する場合、回路に対する入力刺激のすべてについて、回路が動作関係を示す。動作関係に矛盾する回路動作を導く、少なくとも１つの入力刺激がある場合、フォーマル検証ツールは、プロパティの失敗を決定する。プロパティもまた、シミュレーションにより検査され得る。その場合、シミュレーションが、すべての入力刺激を検査するほど十分に強くないので、プロパティの適合を実証することができない。しかしながら、シミュレーションは、プロパティの失敗を示すのに十分である。デザイン記述に対するプロパティをシミュレータによって検査するために、デザイン記述は、シミュレータを用いてシミュレートされ、シミュレータは、シミュレータを用いて生成された値のシーケンスについてのプロパティを評価する。評価が、プロパティの失敗を示す場合、エラーメッセージがシミュレータによって発行される。
【００４６】
回路の実行トレースは、回路がそのハードウェア記述に従って作成し得る回路の入力、出力、および内部信号の値のシーケンスである。反対の例は、プロパティに矛盾する実行トレースである。
【００４７】
時間変数の所定の実例について、仮定部分および証明部分の双方が実行トレースによって満たされる場合、時間変数（「t」を含む）のいくつかの所定の実例について、プロパティが実行トレースに一致すると言われる。実行トレースがいくつかの回路によって生成される場合、且つ、その回路についてプロパティの適合が証明される場合、全体のプロパティが一致するか否かを決定するために、仮定部分の一致を確認するので十分である。
【００４８】
プロパティチェーンは、プロパティのシーケンスP0,P1,P2,…である。すべての時間変数の実例がプロパティP0,P1,P2,…に存在する場合、プロパティチェーンは、プロパティが実行トレースに一致するような、且つ、すべてのi>=0について、プロパティPi+1のleft hookがプロパティPiのright hookに等しいような実行トレースに一致すると言われる。
【００４９】
たとえVが実際に表現の結果に寄与する場合であっても、表現Eを形成するシンタックス内にVが生じる場合、表現Eは、いくつかの変数Vに「依存する」と言われる。例えば、表現「V and not V or W」は、VおよびWに依存する。
【００５０】
発明の概念的な背景
アーキテクチャ記述
プロセッサのアーキテクチャ記述は、例えばプログラマーズ・マニュアルによって提供される視点を示す。アーキテクチャ記述は、プロセッサが次の命令を開始する前に、プロセッサがすべての命令を完全に実行するという、プロセッサの視点を取る。したがって、アーキテクチャ記述は、クロックサイクル毎に１つの命令を実行する同期式オートマトンと考えられ得る。命令に加えて、アーキテクチャは割り込みも実行する。割り込みは、アーキテクチャ割り込み信号によって、アーキテクチャ記述に合図される。プロセッサが割り込みを受理する場合、プロセッサは、命令の代わりに割り込みを実行する。１つの割り込み又は１つの命令の実行は、「アーキテクチャサイクル」と称されるであろう。
【００５１】
アーキテクチャのインタフェースは、データメモリ又は命令メモリと通信する信号により、割り込み信号およびリセット信号により与えられる。アーキテクチャ記述の状態は一般的に次のものを含む。
●  実行される命令のアドレスを提供するプログラムカウンタ。
●  命令が動作する１つ又は複数のレジスタファイル。これらレジスタファイルはレジスタの配列であり、単一のレジスタに縮退してもよい。レジスタファイルは、例えば、プロセッサが処理するデータを格納する。別の例は、最後の命令実行に関する情報を提供するブール変数を用いたプログラム・ステータス・ワードである（例えば、オーバフローを生成する最後の命令実行を強調するブール変数、或いは、最後の命令の結果がゼロであることを示すブール変数）。レジスタファイルは、例えば、割り込み優先順位および割り込みマスク（いくつかの割り込みをオフにする）等の、割り込みの受理を決定するために必要とされる情報、或いは、割り込みを実行するために必要とされる情報を格納することもできる。
【００５２】
アーキテクチャ記述の命令は、単純な命令と、ジャンプ命令とに分類することができる。単純な命令については、プログラムカウンタは、カウンタと同様に更新される。多くの場合、ジャンプ命令は、アーキテクチャ記述の状態に関する条件を明示する。ジャンプ命令実行中に、条件は、アーキテクチャ記述の状態で評価されるであろう。条件が満たされる場合、アーキテクチャプログラムカウンタは、命令に明示されるいくつかの新規の値にセットされるであろう。ジャンプ命令の条件が満たされる場合、ジャンプが「起こる」と呼ばれる。条件が満たされない場合、ジャンプが「起こらない」と呼ばれる。後者の場合、単純な命令による更新のように、アーキテクチャプログラムカウンタが更新される。
【００５３】
同様に、割り込み実行は、アーキテクチャ記述に、アーキテクチャプログラムカウンタを割り込みサービスルーチンの開始アドレスにセットさせる。
【００５４】
インプリメンテーション
プロセッサは、一般的に、アーキテクチャ記述で記述されたオートマトンによって実行されない。代わりに、命令実行がパイプラインされる。従って、ＲＴＬインプリメンテーションは、複数の命令を同時に扱うことができ、それぞれの命令は、それら異なる実行フェーズ中にある。プロセッサの共通クラスは、１つのパイプラインから構成され、これは、本発明が例示されるであろうクラスである。図８に、単一のパイプラインから構成されるそのようなプロセッサを示す。本発明がそのようなパイプラインに制限されないことに注意されなければならない。
【００５５】
パイプラインはステージ1…nから構成されると言われる。ステージ１  ３０１は、ステージ１がプログラムカウンタを含むように選択される。命令実行は複数のフェーズから構成され、それぞれのフェーズは、パイプラインステージの１つのステージにおいて実行される。例えば、ステージ１は、命令メモリ３１２へ読み込み要求を発行する。ステージ２  ３０２は、命令メモリが返す命令３１３を受信する。更に、ステージ２は、命令が組み合わせるオペランド３１０を読み込む。
【００５６】
ステージ３  ３０３は、命令仕様に従ってオペランドを組み合わせる。このことは、結果がインプリメンテーションレジスタファイル３０５に書き戻されるまで、ステージ４  ３０４に格納される結果を与える。
【００５７】
命令は、パイプラインステージに沿って移動し、命令実行の関連するフェーズを実行することによるインプリメンテーションによって実行される。このステージを実行する信号が、命令実行によってコントロールされる場合、命令はステージにあると言われる。したがって、命令は、最初はステージ１にあり、次に、命令はステージ２に移動し、その後ステージ３など、命令が最後のパイプラインステージに達するまで移動し、そこで命令実行は終了する。命令がステージsから次のステージまで移動することが可能な場合、ストール信号３０７によってs+1が決定される。ストール信号が０である場合、命令はステージsから次のパイプラインステージまで移動することができ、そうでなければ、命令はパイプラインステージsに残らなければならない。
【００５８】
プロセッサパイプラインは、命令実行を、割り込み入力３１４によって合図される割り込み実行に置き換えることにより、割り込みを実行する。いくつかのステージは、割り込みの受理に対応可能なように設計されている。割り込みが受理される場合、そのステージの命令実行、および、より下位のステージ番号を有するすべての命令実行は、取り消し信号３０８をアクティブ化することにより取り消される。取り消しは、取り消しを行った後に、あたかも命令が存在しなかったかのようにプロセッサが動作することを意味する。割り込みは、その後、取り消された最も高位の命令に代えて、フェーズ中において実行される。
【００５９】
１つの命令の、或いは１つの割り込み実行は、インプリメンテーションサイクルと呼ばれるであろう。プログラムサイクルは、インプリメンテーション或いはアーキテクチャサイクルのための集合タームとならなければならない。
【００６０】
プロセッサインプリメンテーションは、インプリメンテーションレジスタファイル３０５と呼ばれるレジスタファイルを含むであろう。命令実行又は割り込み実行が、当該更新が起こるべきであるステージ３０４にある場合、これらインプリメンテーションレジスタファイルは、インプリメンテーションサイクルの結果を用いて更新されるであろう。このステージは、インプリメンテーションレジスタファイルの書き戻しステージと呼ばれる。命令についてのオペランドは、一般に、インプリメンテーションレジスタファイルから読み込まれる。例外は、以下に記述されるパイプラインハザードに関連する。
【００６１】
多くの場合、命令の結果は、書き戻しステージの前のステージ３０３において計算される。その後、その結果は、その結果が計算されるステージと書き戻しステージとの間のステージを通じてシフトされる必要がある。これは、ステージを実行するいくつかの信号によって行われる。
【００６２】
パイプラインステージを通じたこの結果のシフティングのせいで、結果は、その結果が生成されたしばらく後に、インプリメンテーションレジスタファイル３０５に書き戻される。このことは、結果を生成した命令の以後の命令が、インプリメンテーションレジスタファイルに書き込まれる結果の以前の結果を必要とするという状況を導く場合がある。この状況はパイプラインハザードと呼ばれる。パイプラインハザードを解決するために、特別のフォワーディングハードウェア３０９が要求され、パイプライン中に依然として存在するそのような結果が、次の命令に対して利用可能となるようにする。結果が依然として生成されない場合、第２の命令実行が遅延されなければならない。これは、パイプラインをストールすることにより達成される。
【００６３】
プロセッサのほとんどのジャンプ命令は条件付き、即ち、条件が、PCが正常な方法でインクリメントされるのか、もしくは新しいアドレスにセットされるのかを決定する。その結果、条件が実行されるまで、プロセッサは、ジャンプ後の次の命令について不確定な状態となる。条件の実行が、さらに後のステージにある場合もある。時間の浪費を避けるために、プロセッサは次の命令について推測してもよく、この条件付き実行が、この推測が不正確であることを示す場合は、それら次の命令を削除する。この削除は、ステージからの命令を取り消すことにより達成される。取り消しはまた、割り込みが命令シーケンスを適切に修正することを保証する。
【００６４】
等価性
本発明は、アーキテクチャ記述とインプリメンテーション記述との間の等価性を検証する。等価性の正確な概念はここに示されるであろう。
【００６５】
アーキテクチャ記述とインプリメンテーション記述との間の等価性を定義するために、アーキテクチャ記述は、クロックサイクル毎に、厳密に１つの命令又は割り込みを実行する同期式回路のように扱われるであろう（アーキテクチャサイクルと呼ばれる）。アーキテクチャサイクルは、リセット後、アーキテクチャ状態AS@1で開始する番号付けがなされるであろう。i番目の（i=1,2,3,…）アーキテクチャサイクルの後、プロセッサはアーキテクチャ状態AS@i+1にある。
【００６６】
アーキテクチャ記述およびインプリメンテーション記述は、等しいリセット状態から開始し、同じプログラムを実行する。即ち、双方が、命令メモリの同じアドレスから同じ命令を得る。そのうえ、データメモリは、最初に同じアドレスに同じデータを格納し、アーキテクチャ記述およびインプリメンテーション記述がこれらアドレスに書き込むまで、アーキテクチャ記述およびインプリメンテーション記述が同じデータメモリアドレスから同じデータを受信するようにする。アーキテクチャ記述およびインプリメンテーション記述の双方が、命令メモリに格納されたあらゆる実行可能なプログラム用のデータメモリへ、要求の同じシーケンスを作成する場合において、割り込みが到着しない限り、インプリメンテーション記述はアーキテクチャ記述に等価であると言われる。このことは、アーキテクチャ記述によって記述されるデータ転送のシーケンスから、インプリメンテーション記述によって記述されるデータ転送のシーケンスへのマッピングが存在しなければならないことを意味する。このマッピングは、アーキテクチャ記述のi番目のデータ転送を、インプリメンテーション記述のi番目のデータ転送へマッピングしなければならない。マッピングは、アーキテクチャ記述によって記述されるあらゆるデータ転送と、インプリメンテーション記述のマッピングされたデータ転送とが、同じ方向で同じアドレスにデータ転送を実行することを保証しなければならない。また、書き込み要求の場合、それらは同じデータを転送する。
【００６７】
そのようなマッピングが存在する場合、アーキテクチャ記述によって記述されるデータ転送のシーケンスと、インプリメンテーションによって記述されるデータ転送のシーケンスとは、タイミングの点およびプロトコルに関して異なるが、要求（読み込み又は書き込み）の方向、要求のアドレス、および書き込みリクエストによって書き込まれるデータに関して等しい。
【００６８】
等価性のこの概念は、割り込みに適合するために洗練されていなければならない。インプリメンテーション記述の割り込み入力信号irptについての動作（即ち、信号値の時間経過）を、アーキテクチャ記述の割り込み入力信号IRPTについての動作へマッピングする割り込みマッピングが存在しなければならない。
【００６９】
このマッピングは、割り込み入力信号irptの動作を受信するインプリメンテーションと、割り込み信号IRPTによって割り込まれるアーキテクチャとの双方が、データメモリへの要求の同じシーケンスを生成するようにしなければならない。そのようなマッピングがある場合、インプリメンテーション記述はアーキテクチャ記述に等価であると言われる。一旦マッピングが存在すると示されると、本発明はマッピングを記述することができる。
【００７０】
アプローチ
等価性を検証するために、アプローチは、全体のパイプラインによって単一の命令がどのように実行されるのか、或いは、全体のパイプラインによって割り込みがどのように実行されるのかを完全に記述するプロパティを生成する。以下、これら生成されたプロパティ（リセットに関するプロパティを含む）は「メインプロパティ」と称されるであろう。実行が、異なる場合（例えば、条件が満たされる或いは満たされない条件付きジャンプ）を使用して最も良く記述される場合、１つの与えられた命令又は割り込みについて、いくつかのメインプロパティが存在する場合がある。
【００７１】
メインプロパティに加えて、補助プロパティおよび生存プロパティが生成される。この発明の一側面は、このアプローチによって生成される補助プロパティとメインプロパティとが共に、明確な方法で適合することである。任意の適正な入力トレースが与えられると、生成されたメインプロパティおよび生成された補助プロパティにのみ基づいて、インプリメンテーション動作を予測することが可能である。これは一般的な品質判定基準である。その利点および必要なツールは、完全性チェッカーに関する同時継続中の特許出願[BB05]に詳細に記載されている。構文によりプロパティがこの基準を満たすので、この発明の目的のために、完全性チェックツールの特定のアプリケーションは必要ではない。
【００７２】
生成されたメインプロパティのそれぞれの内容は、生成されたメインプロパティが次のことを実行することを含む。
●  プロセッサが命令実行を開始可能な状態にあると仮定する。
●  命令メモリへのアクセスの生成を証明する。
●  フェッチされた命令およびプロセッサの状態が、プロパティが役立つ状況についての条件を満たすと仮定する。
●  プログラムカウンタが正確に更新されることを証明する。
●  プロセッサが次の命令を実行することができる状態に戻ることを証明する。
●  アーキテクチャ記述に従って結果が計算されることと、フォワーディングをコントロールする信号が正確にセットされることとを証明する。
●  プログラム・ステータス・ワードが正確に修正されることを証明する。
●  結果が適切なレジスタファイル（或いはレジスタ）へ正確に書き戻されることを証明する。
●  インプリメンテーションが、データバスの転送方向と、そのアドレスと、書き込みデータ（書き込み転送の場合）とを正確に決定することを証明する。
【００７３】
仮想レジスタおよびレジスタファイル
本発明におけるさらなる要素は、「仮想レジスタ」或いは「仮想レジスタファイル」である。この概念は、プログラム・ステータス・ワード、レジスタファイル、或いは、割り込みコンフィグレーションレジスタまでをも含むような、アーキテクチャレジスタに関係するすべての発行を検証する役目をする。
【００７４】
この記述の全体にわたって、アーキテクチャレジスタは、配列に組織されたレジスタファイルであるとみなされる。レジスタが配列に組織されなければ、それは、あたかもそれが１つの要素のみを用いてレジスタファイルに属するかのように扱われるであろう。従って、仮想レジスタは仮想レジスタファイル内に組織される。
【００７５】
仮想レジスタファイルは、インプリメンテーション状態をアーキテクチャ状態のレジスタへマッピングするマクロである。ステージs中の命令について、仮想レジスタは、ステージs中の命令が実行される前に、ステージs中の命令がアーキテクチャ内に観測するレジスタファイル値を提供する。したがって、仮想レジスタファイルは、パイプラインステージに依存して定義される。
【００７６】
仮想レジスタファイルは、パイプラインステージ中の命令がプログラム中に現れる順番で、仮想レジスタファイルがパイプラインステージをテストするように構築される。ステージがインプリメンテーションレジスタ用のまだ書き戻されていないデータを含むか否かを確認するために、それぞれのステージが検査され、最初のステージ中に見つかったデータが返される。パイプラインを通じて命令がさらに継続するにつれて、ステージのうちの１つがデータの生成を知らせる命令を含む場合がある。この場合、仮想レジスタは、それぞれのデータが現在利用可能ではないことを示す特別の値「無効」を返す。検査されたステージが何もデータを含まない場合、もしくは少なくともデータを知らせる場合、対応するインプリメンテーションレジスタからのデータが返される。
【００７７】
単一のパイプラインプロセッサについては、他の命令シーケンスがあり得ないので、ステージは、ステージs+1から開始する番号から昇順に検査される。したがって、ユーザが仮想レジスタファイルを提供する必要はない。複数のパイプラインステージを備え、１つの命令が、別の１つのパイプライン中において実行される別の１つの命令を追い越す可能性を有するような、より手の込んだスーパースカラ・プロセッサについては、命令シーケンスはプロセッサ状態から推定されなければならない。
【発明を実施するための最良の形態】
【００７８】
図１に、この発明に係る例示的なプロセスを示す。第１のステップ２０１では、インプリメンテーション記述が読み込まれ、内部フォーマット２０２に変換される。インプリメンテーション記述は、例えばＲＴＬを表現するいくつかのハードウェア記述言語によって与えられる場合がある。他のインプリメンテーション記述は、ネットリスト、もしくはサイクル的に正確な動作の記述であり得る。
【００７９】
アーキテクチャ記述はステップ２０３において読み込まれる。アーキテクチャ記述の内容は、以下に記述する規則に従う。ステップ２０４において、対応情報２０４が読み込まれる。対応情報は、設計上の決定を表現し、インプリメンテーション記述とアーキテクチャ記述との間の対応を確立する。このことは以下に記述されるであろう。プロパティ生成ステップ２０５において、プロパティのセット２０６が、アーキテクチャ記述、インプリメンテーション記述２０２、および事前に読み込まれた対応情報から生成される。
【００８０】
その後、生成されたプロパティのセットは、ステップ２０７においてインプリメンテーション記述に対して検証される。検証ステップ２０７は、フォーマル検証ツール（例えば、モデルチェッカーもしくはプロパティチェッカー）で実行することができるが、本発明は、インプリメンテーションに対するプロパティを検証する他の任意の方法、例えばシミュレーション等にも及ぶ。フォーマル検証については、生成されたプロパティのセットの、或るプロパティの適合が証明され得ないことが一旦判明すれば、検証ステップ２０７は終了することができる。ステップ２０４、２０５および２０７は、アーキテクチャ記述とインプリメンテーション記述との間の等価性を実証する。
【００８１】
検証の結果は、アーキテクチャ記述とインプリメンテーション記述とが等価の場合、ステップ２０９において表示され、プロパティのうちの１つが、アーキテクチャ記述とインプリメンテーション記述との間の等価性の欠如を潜在的に指摘する証明に失敗するものである場合、ステップ２０８において表示される。後者、即ち等価性の欠如の場合、インプリメンテーション記述もしくはアーキテクチャ記述にバグがあるのか、それとも対応情報にバグがあるのか識別することを可能にする分析情報が設計者に返される。
【００８２】
利用モデル
事前に設計されたインプリメンテーションのフォーマル検証については、図１に示す方法が一度実行され、そして、プロパティチェッカによって検証ステップ２０７が実行されるであろう。インプリメンテーションの設計と平行したフォーマル検証について、図１に示すプロセスが、同じ対応情報と、アーキテクチャ記述に記述された、ますます多くの命令とを繰り返し実行するであろう。そのアーキテクチャ記述エントリーに記述される命令の数は、インプリメンテーションの開発状態を反映する。このアプローチを用いて、プロセッサの開発は、フォワーディングおよびストールの生成のような中心メカニズムから始まり、そして、割り込みのサポートおよび命令を用いて、開発を段階的に拡張することができる。この例の利点は、プロセッサ設計のあらゆるステップがかように検証され、プロセッサ設計におけるエラーが、プロセッサの設計サイクルの初期に修正され得ることである。
【００８３】
シミュレーションベースの検証について、ステップ２０７は、アサーションベースの検証と共通の手続を使用するシミュレーションにおいて生成されたプロパティを確認することにより実行される。
【００８４】
アーキテクチャ記述
アーキテクチャ記述は、入力in、出力out、状態AS（複数のアーキテクチャレジスタおよびプログラムカウンタから構成される）、次の状態関数NSTATE、および出力関数OUTを用いて、オートマトンを表現する。
【００８５】
オートマトンは、初期値を有する状態AS@1から始まり、入力in@1,in@2,in@3,…を受信する。オートマトンは、out@i=OUT(AS@i,in@i)と、AS@i+1=NSTATE(AS@i,in@i)とによって、状態値のシーケンスAS@2,AS@3,…と、出力値のシーケンスout@1,out@2,out@3,…とを定義する。オートマトンの遷移はアーキテクチャサイクルと呼ばれるであろう。j番目のアーキテクチャサイクルは、入力in@jを消費し、状態AS@j+1と出力out@jとを生成するものである。
【００８６】
アーキテクチャ記述は、インタフェースにグループ化された、次に示す入力および出力を含む。
【００８７】
命令メモリインタフェース
IMEM_ADDRESS：命令メモリへ命令アドレスを提供する出力。この命令アドレスの下では、１つの命令を見つけることができると仮定されている。
IW：同じメモリトランザクション内に示された命令アドレスIMEM_ADDRESSへ、命令メモリからの命令「word read」を提供する入力。
【００８８】
データメモリインタフェース
DMEM_ADDRESS：データメモリへデータアドレスを提供する出力。
DMEM_ACCESS_VALID：データメモリへのアクセスを有効にするビット出力。
DMEM_RW：データメモリへの読み込み（「０」）アクセスと書き込み（「１」）アクセスとを区別するビット出力。
DMEM_WDATA：当該サイクルにおいてデータメモリに書き込まれるデータを提供する出力。
DMEM_RDATA：DMEM_RWが「０」である場合に、同じメモリトランザクション内のアクセスへ、データメモリから返されたデータを提供する入力。
【００８９】
このデータメモリインタフェースについての動作はマクロで捕らえられる。
DMEM_IDLE :=                       DMEM_ACCESS_VALID = ‘0’;
DMEM_READ(addr) :=               DMEM_ACCESS_VALID = ‘1’ and
DMEM_ACCESS_RW = ‘0’ and
DMEM_ADDRESS = addr;
DMEM_WRITE(addr, wdata) :=       DMEM_ACCESS_VALID = ‘1’ and
DMEM_ACCESS_RW = ‘1’ and
DMEM_ADDRESS = addr and
DMEM_WDATA = wdata;
割り込みインタフェース
IRPT：例えば割り込みの到着に関する信号のように、割り込みに関係する入力信号のセット。
【００９０】
アーキテクチャの状態
オートマトンの状態は、アーキテクチャレジスタファイル（単一のアーキテクチャレジスタに縮退可能なアーキテクチャレジスタの配列である）と、アーキテクチャプログラムカウンタPCとによって与えられる。アーキテクチャレジスタファイルの要素はR[k]と呼ばれるであろう。
【００９１】
アーキテクチャの遷移、即ち、命令、割り込みおよび初期化
オートマトンのトランザクションはアーキテクチャ記述エントリーのリストによって与えられる。初期化については、１つのアーキテクチャ記述エントリーが、割り込み実行については、１つのアーキテクチャ記述エントリーが、そして、命令実行を記述するための多くのアーキテクチャ記述エントリーが存在する。
【００９２】
アーキテクチャ記述エントリーはすべて、条件TRIGGERmおよびアクティビティブロックACTmから構成される。条件TRIGGERmが満たされてアーキテクチャレジスタおよびプログラムカウンタが更新される場合、アクティビティブロックは、アーキテクチャレジスタおよびプログラムカウンタがどのように更新されるのかを記述する。m=0についてのアーキテクチャ記述エントリーは、割り込み実行と、命令実行を記述するm>0についてのアーキテクチャ記述エントリーと、プロセッサの初期化を記述するACTinitおよびTRIGGERinitから構成されるアーキテクチャ記述エントリーとを記述する。
【００９３】
初期化についてのアーキテクチャ記述エントリーは、リセット動作を有する条件TRIGGERinitと、次のフォームのアクティビティブロックとを含む。
ACTinit= 
PC = initPCand 
R1[k1] = initR1,k1 and 
R2[k2] = initR2,k2  and 
…
初期化についてのアーキテクチャ記述エントリーは、アーキテクチャプログラムカウンタPC@1についての初期値から構成されるアーキテクチャ状態、即ちAS@1についての初期値と、すべてのアーキテクチャレジスタR[k]@1についてのすべての初期値とを提供する。
【００９４】
割り込みアーキテクチャ記述エントリーは、アーキテクチャレジスタおよびアーキテクチャの割り込み入力IRPTには依存し得るが、PC、IW、或いはDMEM_RDATAには依存しない条件TRIGGER0を含む。対応するアクティビティブロックACT0は、論理積のフォームを有する。この論理積は、すべてのレジスタファイルについて、次の２つのレジスタファイルエントリーのうちの１つを含み、以下に記述されるように、PCについてのエントリーと、３つの可能なデータメモリエントリーのうちの１つとを更新する。レジスタファイルRについてのレジスタファイルエントリーは、レジスタアドレスINDEX0,Rにおいて、Rが値UPDATE0,Rで更新されることを定義する。
【００９５】
ASSIGN0,R:= 
for each k in the index_range of R
if k = INDEX0,R
then next(R[k]) = UPDATE0,R
else next(R[k]) = R[k]
end for each
ここで、INDEX0,RおよびUPDATE0,Rは、アーキテクチャレジスタ、PC、DMEM_RDATA、およびアーキテクチャ割り込み入力IRPTに依存し得る。或いは、レジスタファイルエントリーは、レジスタファイルがその値を保存することを定義する。
【００９６】
NO_ASSIGNR:= 
foreach k in  the index_range of R
next(R[k]) = R[k]
end foreach
PCについての更新エントリーは次のフォームである。
【００９７】
ASSIGN0,PC:= 
next(PC) = UPDATE0,PC
ここで、UPDATE0,PCは、アーキテクチャレジスタ、DMEM_RDATA、およびアーキテクチャ割り込み入力IRPTに依存し得る。
【００９８】
データメモリエントリーは、
DMEM_IDLE
もしくは
DMEM_READ(ADDR0)
のフォーム、或いは、アーキテクチャレジスタ、PC、およびアーキテクチャ割り込み入力IRPTに依存し得るデータメモリアドレスADDR0および書き込みデータWDATA0を用いた
DMEM_WRITE(ADDR0, WDATA0)
の何れかのフォームである。
【００９９】
このアクティビティブロック内にDMEM_READ(ADDR0)が明示される場合、アクティビティブロックACT0内ではDMEM_RDATAのみが起こり得る。
【０１００】
命令エントリー（m>=1）は、条件TRIGGERmおよびアクティビティブロックACTmから構成される。条件は次のフォームである。
【０１０１】
TRIGGERm:= 
not TRIGGER0and
TRIGGER_IWmand
TRIGGER_STATEm
TRIGGER_IWmは、アーキテクチャ命令語IWにのみ依存し得る。TRIGGER_STATEmは、アーキテクチャレジスタ、PC、DMEM_RDATA、およびIWにのみ依存し得る。
【０１０２】
TRIGGER_IWmは、命令のオペコードがIWからどのようにデコードされるかを記述する。命令実行の記述が、アーキテクチャ状態に依存するさらなる細分化を要求する場合、アーキテクチャ状態に関する条件が、TRIGGER_STATEmに捕らえられる。そのような細分化は、ジャンプ命令を記述するために、或いは、命令が適切に実行され得ない場合にエラー訂正ルーチンへジャンプすることが可能な命令を記述するために必要である。
【０１０３】
すべてのマクロ、特に、マクロINDEXm,R、UPDATEm,R、ADDRm、およびWDATAmが、すべてのアーキテクチャレジスタ、PC、およびIWに依存し得る点と、アーキテクチャ割り込み入力IRPTに依存してはならない点とを除いて、アクティビティブロックは、割り込みのアクティビティブロックについて上記に記述されたフォームに類似する。アクティビティブロックがDMEM_READ(ADDRm)を明示する場合、さらにINDEXm,RおよびUPDATEm,RがDMEM_RDATAに依存し得る。
【０１０４】
UPDATEm,PCは、すべてのアーキテクチャレジスタ、PC、およびIWに依存し得るが、DMEM_RDATAには依存しない。
【０１０５】
１つのアーキテクチャ仕様エントリーについてのTRIGGER_STATEm、INDEXm,R、UPDATEm,R、UPDATEm,PC、ADDRm、およびWDATAm関数中の任意のレジスタファイルへの参照は、次のように番号付けられるであろう。マクロTRIGGER_STATEm、INDEXm,R、UPDATEm,R、UPDATEm,PC、ADDRm、およびWDATAmは、サブ表現に分解される。これらサブ表現のいくつかは、アーキテクチャレジスタファイルへの参照、即ち、それらはフォームR<[index function]>である。これら参照は、すべてのアーキテクチャエントリーmについて番号付けられるであろう。インデックス関数<index function>は、VINDEXm,iと呼ばれるであろう。ここで、iは、番号付けられたレジスタファイルアクセスの番号である。
【０１０６】
例えば、関数UPDATEm,R=R1[IW[3:0]+R2[IW[7:4]は、関数VINDEXm,i=IW[3:0]およびVINDEXm,i+1=IW[7:4]を用いる２つのレジスタファイルアクセスを有する。２つのレジスタファイルアクセスの１つはR1に対し、もう１つはR2に対する。
【０１０７】
アーキテクチャ記述は、あらゆる命令についてそのアーキテクチャ記述が完全であるというフォームの整合性条件を満足しなければならない。この整合性条件は、同じTRIGGER_IWに属するすべてのアーキテクチャ記述エントリーのアーキテクチャ状態に関する条件TRIGGER_STATEが、完全な場合分けを形成すること、即ち、同じTRIGGER_IWに属する条件TRIGGER_STATEの分離が常に満たされることを要求する。
【０１０８】
no_resetの制約
リセットがどのように非アクティブに保持されるのかを記述するブーリアンマクロno_resetが提供されなければならない。このブーリアンマクロは、リセット動作に関する証明を除いたすべての証明中に存在するであろう。
【０１０９】
命令およびデータメモリについてのアクセスプロトコル記述
実装されたパイプラインは、２つのメモリポート、即ち、命令を読み込むための１つのポートと、データを読み込む又は書き込むためのもう１つのポートとを持つと予想される。双方のポートにおけるプロトコルは、パイプライン動作に関連して記述される。方向と、アドレスと、そして適用可能であれば、ステージがストールしない場合の書き込みデータとを生成するマクロと共に、パイプラインステージの番号が、それぞれのポートについて提供されなければならない。そのうえ、おそらく別のステージが、読み込みアクセスの場合に読み込みデータを生成するマクロと共に提供されなければならない。単純なプロトコルについては、要求されたマクロが、プロセッサ入力と、命令バス又はデータバスを形成するプロセッサ出力とに依存して定義され得る。より複雑なプロトコルは、パイプラインとバスポートとの間に、バスインタフェースモジュールを必要とする。この場合、パイプラインとバスインタフェースモジュールとの間のインタフェースは、アクセスプロトコル記述を用いて特徴付けられるであろう。要望に応じて、アドレス及びデータが正確に転送されることを示すために、バスインタフェースモジュールの検証が実行され得る。
【０１１０】
アクセスプロトコル記述は、関連するパイプラインステージと信号の動作とを記述しなければならない。パイプラインステージは定数によって提供される。この目的のために、パイプラインステージは、1からnに連続的に番号付けられるであろう。
●  定数iaは、>=1であり、命令アドレスが命令バスに送られるところのステージの番号を表示する。
●  定数ivは、>=iaとなるように選択される。定数ivは、命令が命令バスから返されるところのステージの番号を表示する。多くの場合、定数ivはia+1に等しい。非同期式メモリの状況下では、定数ivは定数iaの値を取り得る。
●  定数daは、データメモリアクセスが開始されるところのステージの番号を記述し、そのところにおいて、アドレスと、そして適用可能であれば、書き込みデータとが提供される。メモリアクセスを取り消すことができないので、ステージdaは、割り込み又はジャンプ命令の何れによっても取り消され得ないことが必要である。
●  定数dvは、読み込みデータがデータメモリから返されるところのステージの番号を記述する。非同期式メモリについては、定数dvは定数daに等しくなることが可能であり、そうでなければ、定数dvは、>=daの値を取るであろう。
【０１１１】
命令fetchについて、命令がステージiaに存在し次のステージに移ることが可能な時点における命令メモリインタフェース信号の動作を記述するためのブーリアンマクロibus_read(address)が提供されなければならない。このブーリアンマクロibus_read(address)は、命令メモリへのインタフェース信号にのみ依存し得る。読み込み要求が開始されない場合、ブーリアンマクロibus_idleは、任意の時点におけるこれらインタフェース信号の動作を記述する。命令がステージivに存在し次のステージに移ることが可能な場合、マクロiwは、そのクロックサイクルにおける信号、もしくは命令語を形成する表現を明示する。
【０１１２】
ステージivがその命令を前進させることが可能で、且つ、この時点においてマクロibus_read(address)が満たされる場合は常に、インプリメンテーションは、インタフェース上で命令メモリへのリードアクセスを実行する。
【０１１３】
状況はデータ転送に類似する。命令がdaステージに存在し次のステージに移ることが可能な時点におけるデータメモリインタフェース信号の動作を記述する、ブーリアンマクロdbus_read(address)が定義されなければならない。書き込みは、ブーリアンマクロdbus_write(address,wdata)によって記述され、マクロdbus_idleは非アクティブを記述する。マクロdbus_rdataは、命令がステージdvに存在し前方に移ることが可能な時点におけるデータの読み込みを形成する信号又は表現を明示する。
【０１１４】
インプリメンテーションのステップdvが、ステージdvが現在処理する命令を前進させることが可能で、且つ、この時点においてマクロdbus_read(address)が満たされる場合は常に、インプリメンテーションは、データメモリ内の所定のアドレスから読み込みデータの転送を実行する。ステップdvが現在の命令を前方に移動することが可能で、且つ、マクロdbus_write(address,wdata)が満たされる場合は常に、インプリメンテーションは、所定のアドレスおよび書き込みデータwdataを用いて書き込みデータの転送を実行する。他のすべての場合では、データ転送は実行されない。これは、等価性の定義により必要とされる、インプリメンテーションのデータ転送のシーケンスの抽出を可能にする。
【０１１５】
外部ストール条件
プロセッサは環境によって停止され得る。プロセッサを停止させる理由は、命令メモリ又はデータメモリの待ち状態であり得る。プロセッサを停止させるために、プロセッサは、環境から１つ或いは複数の停止信号を受信する。これら停止信号がプロセッサを停止させる必要性を生じる条件は、設計者によるマクロexternal_stallの定義によって、検証に入力されなければならない。
【０１１６】
検証は、外部ストール条件external_stallが決してアクティブにならないことに責任を負うであろう。
【０１１７】
対応情報
次に、図１のステップ２０４において設計者が提供しなければならない対応情報を記述する。この対応情報はインプリメンテーションの決定を捕らえ、デザインプロセスから容易に利用可能である。そのうえ、対応情報が検証によって確認されるという意味で、この対応情報はフェイルセーフである。本発明のフォーマル検証に基づく例について、このことは、不適切な対応情報が、検証を誤って失敗とすることはできるが、誤って成功とすることができないことを意味する。
【０１１８】
パイプラインステージの分類
パイプラインのステージが1〜nで番号付けされているとしよう。パイプラインステージの役割は、次のように記述されるであろう。
●  decは命令実行が実際に開始するステージである。多くの場合、このステージはフォワーディングパスがターゲットとする場所である。命令バスにおけるタイミングに依存するが、多くの場合、ステージdecはステージivもしくはステージiv+1である。如何なる場合も、ステージdecの番号は>=ivとなるであろう。
●  jmpm：すべてのアーキテクチャ記述エントリーmについて、プログラムカウンタが次の命令の値にセットされるステージが明示される。単純な命令（算術命令のような）については、これは1であり、ジャンプ及び割り込みについては、それは/=1であろう。
●  int=jmp0：これは、割り込みが受理されるか否かを決定するステージを記述する。すべてのmについて<=intとなる値jmpmを有する。データバスへのアクセスを取り消すことができないので、ステージdaの番号>=intである必要がある。
●  vstagem,i：m>=1について、これは、アーキテクチャ仕様エントリーmのi番目のレジスタファイルアクセスがなされるステージに関する検証への情報、即ち、VINDEXm,iに関するレジスタファイルアクセスを提供する。多くの場合、フォワーディングパスはすべて、プロセッサのデコードステージをターゲットとする。この場合、すべてのmおよびiについて、ステージvstagem,i=decである。しかしながら、より手の込んだプロセッサは、ステージdecより後のステージへのフォワーディングを可能にする。この場合、vstagem,iは>decの値にセットされ得る。TRIGGER0において読み込まれるすべてのレジスタ値について、vstage0,i=intであり、割り込み実行を記述するアクティビティブロックであるACT0において参照されるすべてのレジスタについて、vstage0,i>=intであることが必要である。
●  writebackR：上記した仮想レジスタファイルの点について、すべてのアーキテクチャレジスタファイルRについて、書き戻しステージが提供されなければならない。本発明のこの例は、すべてのレジスタファイルRについて、int<=writebackRを要求する。
【０１１９】
ストール条件
[1,n]内のすべてのステージsについて、このステージsがストールする条件が、マクロstallsで提供されなければならない。このマクロstallは、すべてのインプリメンテーション信号に依存し得る。
【０１２０】
マクロが値１をとる場合、ステージsはストールする。それは、次のインプリメンテーションクロックサイクルにおいて、ステージsが現在の命令をさらに処理し続けることを意味する。マクロが値０をとる場合、ステージsはストールしない。（時には「ステージはノーストールを有する」と呼ばれる）。これは、ステージsが現在の命令を次のステージへ渡すこと（或いは、ステージsがパイプライン中の最後のステージnである場合、現在の命令をドロップすること）を意味する。
【０１２１】
取り消し条件
[1,n]内のすべてのステージsについて、ステージsが取り消される条件が、マクロcancelsで提供されなければならない。このマクロcancelは、すべてのインプリメンテーション信号に依存し得る。
【０１２２】
マクロが値１をとる場合、ステージsは取り消される。それは、ステージsから命令が取り除かれ、インプリメンテーションを確実にする動作が、命令が利用可能でなかったとすることを意味する。
【０１２３】
ステージsが取り消される場合、すべてのステージ1,…s-1もまた取り消される必要がある。
【０１２４】
以下において、略語primary_cancels=not cancels+1and cancelsが、[1,n-1］内のsについて用いられるであろう。
【０１２５】
Full
[2,n]内のすべてのステージsについて、マクロfullsが提供されなければならない。それは、ステージsが現在、命令又は割り込みを実行する場合、値１を取り、そうでなければ値０を取る。マクロfullは、すべてのインプリメンテーション信号に依存し得る。
【０１２６】
開始状態
プロセッサインプリメンテーションが新しい命令を開始する際の状態を記述するブーリアンマクロprocess_new_instruction_stateが提供される。
【０１２７】
プログラムカウンタ
インプリメンテーション状態をインプリメンテーションプログラムカウンタpcの値へマッピングするマクロpcが提供されなければならない。このマクロpcは、一般的に、インプリメンテーションプログラムカウンタを格納するいくつかのインプリメンテーション信号に等しいと定義されるであろう。
【０１２８】
仮想レジスタファイル
アーキテクチャレジスタファイルRのすべてについて次の情報が提供される。
●  インプリメンテーションレジスタファイルcurrentR(k)。ここで、kはアーキテクチャレジスタファイルへのインデックスである。
●  ステージwritebackR。これは、値がインプリメンテーションレジスタファイルcurrentRに書き込まれるであろうステージを提供する。
●  dec+1とステージwritebackRとの間（およびそれらを含む）のすべてのステージsについて、次の○に示すマクロ。
○  ブーリアンマクロresult_writeR,s。これは、ステージs中の命令が新しいデータを作成する場合、真である。ステージsが空の場合、このマクロresult_writeR,sは偽を返す。
○  マクロresult_destR,s。マクロresult_destR,sが真の場合、このマクロresult_destR,sは、ステージsの中の命令が書き込まれるレジスタファイルアドレスを含む。
○  ブーリアンマクロresult_validR,s。これは、ステージs中の命令が、今パイプラインを通じてシフトされる新しいデータを既に生成している場合、真である。ステージsが空の場合、このマクロresult_validR,sは偽である。
○  マクロresult_dataR,s。これは、マクロresult_validR,sが真の場合、現在ステージs中にある命令の、Rについての結果を生成する。
【０１２９】
これらマクロから、検証プロセスは、仮想レジスタ関数を次のように作成する。ステージs中の命令について、アーキテクチャレジスタファイルRについての仮想レジスタファイルのk番目の要素は、[dec,writebackR-1]内のステージsについて、次のように与えられる。
【０１３０】
dataR,writebackR(k) @ t = currentR(k) @ t
and    dataR,s(k) @ t =
(if result_writeR,s+1 and result_destR,s+1 = k
then result_dataR,s+1
else dataR,s+1(k)) @ t
この定義の背後にある理論的根拠は、ステージが昇順に確認されることである。値がまだインプリメンテーションレジスタファイルに書き込まれる場合、この値は、それにもかかわらず、対応するアーキテクチャ状態の値になるであろう。したがって、この関数はフォワーディングの検証に関与する。
【０１３１】
しかしながら、仮想レジスタが無効になる場合がある。これは、アーキテクチャ記述に従って結果を計算するために、命令のうちのいくつかが複数のステージを要求する場合である。そして、現在の命令が、要求された値を生成しないステージに依然として存在する間に、１つの命令が既に値を要求することがあり得る。この場合、仮想レジスタは特別な無効値を返す。個別のマクロはそのような状況にフラグを立てるために使用される。個別のマクロは次の通りである。
【０１３２】
validR,writebackR(k) @ t = true
validR,s(k) @ t = 
(if (result_writeR,s+1 and result_destR,s+1 = k)
then result_validR,s+1 
else validR,s+1(k)) @ t       for the stages s in [dec, writebackR - 1] and
validR,s(k) @ t = false   for the stages s in [1, dec-1].
プロパティ生成
次に述べるものは、プロパティが生成される図１のプロパティ生成ステップ２０５の記述である。この目的のためにプロパティスキーマが提供される。プロパティスキーマは、プロパティがどのようにして生成されるかの記述である。この目的のために、特別の条件が満たされる場合にのみ、プロパティスキーマは、プロパティのテキストのある部分を繰り返すための、或いは、プロパティテキストのプロパティの他の部分を書くためのメタコマンドを含む。そのうえ、プロパティスキーマは、アクセスプロトコル記述および対応情報を構成する定数およびマクロに、プレースホルダーを提供する。
【０１３３】
プロパティ生成ステップ２０５は、特定のアーキテクチャ記述および特定のインプリメンテーション記述が存在する場合に実行され得る。プロパティ生成ステップ２０５は、関連する対応情報および関連するアクセスプロトコル記述を伴う。そして、プロパティ生成ステップは次のステップを含む。
１．  メタコマンドすべての実行、即ち、メタコマンドによって規定されるプロパティテキストの或る部分の繰り返し又は省略。
２．  同じ名前のマクロを有するプレースホルダーのインスタンス化。これらマクロは、対応情報およびアクセスプロトコル記述によって提供される。或いは、マクロは、プロパティスキーマに関する方法でアーキテクチャ記述から導かれる。
３．  例えばia、iv、da、dv、int、およびjmpm等の、プロパティテキスト中或いはマクロテキスト中に生じるパイプラインステージの番号用のプレースホルダーすべての、アクセスプロトコル記述或いは対応情報によって提供される実際の番号への置き換え。
【０１３４】
これは生成されたプロパティを提供し、この生成されたプロパティは、等価性を実証するために証明されるであろう。
【０１３５】
単純な命令用のプロパティスキーマ
jmpm=1であるすべてのアーキテクチャ記述エントリーm>0について、プロパティは、このセクションにおいて議論されるであろうプロパティスキーマsimple_instructionに従って生成される。
【０１３６】
プロパティスキーマsimple_instructionは、現在の命令を現在実行するパイプラインステージがストールせずに、現在の命令が前進することを可能にする時点を記述する時点t1,t2,t3,…を導入する。
【０１３７】
このセクションにおいて扱われる命令についての例は、add命令である。アーキテクチャ記述は、add命令がアーキテクチャレジスタファイルからの２つのアーキテクチャレジスタの内容を合計し、アーキテクチャレジスタファイルにその結果を書き込むことを記述する。
【０１３８】
関連するプロパティを記述するために、インプリメンテーション状態に依存するマクロtrigger0、trigger_iwm、trigger_statem、updatem,R、indexm,R、updatem,PC、vindexm,i、addrmおよびwdatamが、アーキテクチャ記述マクロTRIGGER0、TRIGGER_IWm、TRIGGER_STATEm、UPDATEm,R、INDEXm,R、UPDATEm,PC、VINDEXm,i、ADDRmおよびWDATAmから導かれる。
【０１３９】
マクロtrigger0は、マクロTRIGGER0から次のように導かれる。サブ表現が、信号IRPTからの参照アーキテクチャ割り込み入力、またはフォームR[VINDEX0,i]で表される、番号付けられたアーキテクチャレジスタファイルアクセスのうちの１つのどちらかに達するまで、或いは定数に達するまで、マクロTRIGGER0の表現が構文上分解される。TRIGGER0の定義によれば、これらはすべて可能なサブ表現である。サブ表現が定数である場合、サブ表現は置き換えられない。サブ表現がR[VINDEX0,i]である場合、それは、表現dataR,int(vindex0,i)によって置き換えられる。この表現dataR,int(vindex0,i)は、仮想レジスタ関数dataR,intと、trigger0がTRIGGER0から生成される方法で、VINDEX0,iから再帰的に生成されるアドレス関数vindex0,iとから構成されている。アーキテクチャ割り込み入力へのすべての参照は、対応するインプリメンテーション割り込み入力への対応する参照に置き換えられる。すべてのアーキテクチャ割り込み信号IRPTのセットは、すべてのインプリメンテーション割り込み信号irptのセットに置き換えられる。その後、置き換えられたサブ表現を有する表現が、プロパティマクロtrigger0を形成する。
【０１４０】
別のマクロtrigger_iwm、trigger_statem、updatem,R、indexm,R、updatem,PC、vindexm,i、addrmおよびwdatamが、次のように、マクロTRIGGER_IWm、TRIGGER_STATEm、UPDATEm,R、INDEXm,R、UPDATEm,PC、VINDEXm,i、ADDRmおよびWDATAmから導かれる。定数、IW、PC、DMEM_RDATA、或いはフォームR[VINDEXm,i]で表されるアーキテクチャレジスタファイルの参照であるサブ表現が得られるまで、さらに、表現が構文上分解される。サブ表現が定数ならば、それは置き換えられないであろう。サブ表現がIWならば、それはiw@tivに置き換えられ、また、ivは、アクセスプロトコル記述に従って、パイプラインステージの番号に置き換えられるであろう。それが生じる場合、サブ表現DMEM_RDATAはdbus_rdata@tdvに置き換えられ、また、dvは、アクセスプロトコル記述に従って、パイプラインステージの番号に置き換えられるであろう。PCはpc@t0+1に置き換えられる。R[VINDEXm,i]は、仮想レジスタファイル関数dataR,vstage(m,i)(vindexm,i)@tvstage(m,i)に置き換えられる（表現を読み取りやすくするために、vstagem,iの代わりにvstage(m,i)と書いている）。ここで、vstagem,iは対応情報に明示される。vindexm,iの生成と同じ方法で、表現VINDEXm,iが再帰的に処理される。そして、置き換えられたサブ表現を有する表現が、派生マクロを形成する。
【０１４１】
次の例はプロパティスキーマを図示する。即ち、次の例は、上記の置き換えおよび上記の対応情報を与えられて、どのようにプロパティが生成されるかの記述を提供する。メタコマンドは、プロパティコードの繰り返し或いは条件付き生成を明示するために提供される。//が説明テキストに先行するであろう一方、#はそのようなメタコマンドに先行する。また、規則的な反復は、「…」で表示される。
【０１４２】
図２に、このプロパティのグラフィカルな表現を示す。これは、ストール信号に従って命令がどのようにパイプラインを下に移動するかを示す。
【０１４３】
エントリー「dependencies:no_reset」は、リセットが非アクティブに保持されるという付加的な仮定の下で、このプロパティが証明されるという事実を強調する。プロパティスキーマの部分の参照を可能にするために、行番号が導入される。
【０１４４】
関連するプロパティは、次のプロパティを読み込む。
1   property simple_instruction;
dependencies: no_reset;
for time_points: 
5             t0= t,
t1> t0,
t2> t1, 
…
tn> tn-1;
10
assume:
// The time points where the instruction moves forward
at     t0:                stall1 = 0 || cancel1 = 1;
during [t0+1, t1-1]:      stall1= 1;
15     at     t1:                  stall1= 0;
during [t1+1, t2-1]:      stall2= 1;
at     t2:                  stall2= 0;
during [t2+1, t3-1]:      stall3= 1;
at     t3:                  stall3= 0;
20     ...
at     tn:                  stalln= 0;
// assume that no preceding property cancelled this one
during [t0+1, t1]:        cancel1= 0;
25     during [t1+1, t2]:          cancel2= 0;
during [t2+1, t3]:        cancel3= 0;
...
during [tn-1+1, tn]:      canceln= 0;
30     // assume that the processor is ready to execute next instruction
at     t0:                  process_new_instruction_state;
// assume that instruction execution is not interrupted.
during [t0+1, tint]:      not trigger0;
35
<fetch> // This is a cutpoint, see ITL section
// Assume that iw contains the instruction
// that should be handled in this property.
40     at     tiv:                 trigger_iwm;
<validate_regs> 
at     tdec:         trigger_statem;
45
prove:
at     tia:                 ibus_read(pc @ t0+1);
<fetch>
50
// Prove that the virtual register file values are valid
// whenever they are to decide upon trigger_state.
# for each reference z to an architecture register file in
# TRIGGER_STATEm:
55            at tvstage(m,z):          validR,vstage(m,z)(vindexm,z);
# end for each;
<validate_regs> 
60     // Prove that the virtual register file values are valid
// whenever they are required.
# for each reference z to an architecture register file in
# UPDATEm,R, INDEXm;R, ADDRm, or WDATAm:
at tvstage(m,z):          validR,vstage(m,z)(vindexm,z);
65     # end for each;
at t1:                      process_new_instruction_state;
at t1+1:                           pc = updatem,PC;
70     // Prove that the full signals are correctly created.
during [t1+1, t2]:        full2= 1;
during [t2+1, t3]:        full3= 1;
...
during [tn-1+1, tn]:      fulln= 1;
75
// Prove that this instruction will not initiate cancels.
during [t1+1, t2]:        primary_cancel1= 0;
during [t2+1, t3]:        primary_cancel2= 0;
...
80     during [tn-1+1, tn]: primary_canceln-1= 0;
// For all registers that get updated, prove their correct
// handling in the pipeline.
85     # for each register file R with ASSIGNm,R in the architecture
# description entry: 
# for each stage s = dec + 1, dec + 2, ... writebackR-1
at     ts:                  if result_validR,s = 1
then next(result_validR,s+1) =  1
91                                        end if;
# end for each stage
# for each stage s = dec + 1, dec + 2, ... writebackR
during [ts-1+1, ts]:      result_writeR,s = 1;
during [ts-1+1, ts]:      result_destR,s= indexm,R;
95            during [ts-1+1, ts-1]:    if (result_validR,s = 1)
then next(result_validR,s) =  1
end if;
during [ts-1+1, ts]:    if (result_validR,s = 1)
then result_dataR,s = updatem,R;
100                                       end if;
# end for each stage 
at twritebackR+1:               currentR(indexm,R) = updatem,R
# end for each register
# for each register file R with NO_ASSIGNR in the arch. entry:
105       # for each stage s = dec + 1, dec + 2, ... writebackR 
during [ts-1+1, ts]:      result_writeR,s = 0;
# end for each stage
# end for each register
# if the architecture description entry contains DMEM_READ(ADDRm)
110           at tda:                   dbus_read(addrm);
# else if it contains DMEM_WRITE(ADDRm, WDATAm)
at tda:                   dbus_write(addrm, wdatam);
# else // it contains DMEM_IDLE
at tda:                   dbus_idle;
115    # end if
left_hook:       t0;
right_hook:      t1;
end property;
５〜９行目は時間変数t0,t1,t2,…tnを導入する。１２〜２１行目は、これら時間変数t0,t1,t2,…tnを、命令実行を前進させることが可能な時点に関連付ける。これはすべてのステージについて遂行される。stalls条件およびcancel0条件は、対応情報で提供される。
【０１４５】
２４〜２８行目は、ステージが命令を実行している間、ステージが取り消されないことを要求する。さらに、ステージのすべてについて要求が明示される。canceliエントリーは対応情報から提供される。
【０１４６】
３１行目は対応情報で満たされる。それは、命令の開始を可能にするコントローラの状態についての検査に集中する。
【０１４７】
３４行目は割り込みが受理されないことを要求する。trigger0は上記記述に従って導かれる。
【０１４８】
３６行目のカットポイントfetchは、４７行目のその唯一の証明部分と共に、命令バスの読み込みが、読み込まれている実際の命令から独立していることを保証する。
【０１４９】
この命令は、４０行目のtrigger_iwmによってデコードされる。trigger_iwmは上記のセクションに定義される。デコードは、ステージがストールしない時点に関連し、そこでは、命令が命令メモリから到着する。
【０１５０】
ここで、さらにカットポイントvalidate_regsを導入し、関連するプロパティが、プロパティスキーマの４６〜５６行目を証明する。これらの行は、条件trigger_statemによって評価された仮想レジスタファイルの値が、この決定から独立して有効であることを保証する。trigger_statemが自明のこととして真の場合、その後、エントリーがなされないであろうことを５４〜５５行目が明示するので、カットポイントfetchより先に生成されるプロパティを用いて証明することは何もない。
【０１５１】
証明部分の６２〜６５行目は、命令の結果を計算するために使用される仮想レジスタファイルが、最初のステージから、パイプラインされた命令実行がそれらを必要とする前方のステージにわたって、有効とならなければならないことを必要とする。
【０１５２】
６７行目は、命令の評価が、次の命令を開始することができる状態に返ることを保証する。６８行目は、この次の命令が、右側のアドレスからフェッチされるであろうことを保証する。
【０１５３】
７１〜７４行目は、すべてのステージに及んで、対応情報からの関連するマクロfullsが、命令が実行されたことを示す１を生成することを証明する。
【０１５４】
７７〜８０行目は、すべてのステージに及んで、この命令が、前のステージへ取り消しを決して発行しないであろうことを証明する。
【０１５５】
８５〜１０３行目は、アーキテクチャ記述に従って値が割り当てられるすべてのレジスタファイルの仮想レジスタファイルが、右側の値を実際に受信し、パイプラインを通じてその値を伝達することを保証する。対応する関数は対応情報である。
【０１５６】
１０５〜１０７行目は、更新されていないレジスタファイルが正確に扱われるであろうことを保証する。
【０１５７】
８５〜１０７行目は、すべての可能なレジスタファイルに及ぶ。
【０１５８】
１０９〜１１５行目は、メモリと通信する権利を保証する。
【０１５９】
ジャンプ命令
jmpm/=1であるすべてのアーキテクチャ記述エントリーm>0について、プロパティは、プロパティスキーマjump_instructionに従って生成される。
【０１６０】
多くの場合、ジャンプ命令などは、アーキテクチャ記述の２つの部分に結びつくであろう。アーキテクチャ記述の一方の部分は、条件が満たされてジャンプが起こる場合の動作について記述する。アーキテクチャ記述の他方の部分は、条件が満たされずジャンプが起こらない場合の動作について記述する。ジャンプが起こらない場合、プログラムカウンタPCは通常の方法で、即ち、命令が命令メモリにおいて占有するバイト数で更新されるであろう。
【０１６１】
ジャンプが起これば、プログラムカウンタpcは異なった風に更新されるであろう。ジャンプ命令がジャンプを行うか否かを決定するパイプラインステージjmpm中にジャンプ命令が現れるまで、プログラムカウンタのこの更新は待機しなければならない。ジャンプ命令がジャンプを行うことを決定する場合、誤って推測された命令がパイプラインステージ<jmpm中に存在し得るので、パイプラインステージ<jmpm中の誤って推測された命令を取り消すことにより、それらは削除されなければならない。
【０１６２】
プログラムカウンタpcへの標準的でない更新に加えて、アーキテクチャ記述は、ジャンプ命令がアーキテクチャレジスタを更新して、単純な命令について上記記述した形式のメモリトラフィックを実行することを明示することができる。したがって、命令simple_instructionsについてのプロパティスキーマの大部分もまた、命令jump_instructionsについてのプロパティスキーマ中に発現するであろう。
【０１６３】
プロパティスキーマsimple_instructionsについて記述されたように、マクロtrigger0、trigger_iwm、trigger_statem、updatem,R、indexm,R、updatem,PC、vindexm,i、addrmおよびwdatamが導かれる。
【０１６４】
図３に、ジャンプ命令のタイミング関係を示す。パイプラインステージがジャンプ命令を実行する場合のタイミング関係が示される。図はさらに、プロセッサによって推測的にその実行が開始された命令を削除するために、パイプラインステージが取り消される場合のタイミング関係を示すであろう。読み取りを単純化するために、インデックスにおいてjmpmの代わりにjmpと書いている。
1   property jump_instruction;
dependencies: no_reset;
for time_points: 
5             t0= t,
t1 > t0,
t2> t1, 
…
tn> tn-1;
10
assume:
// The time points where the instruction moves forward
at     t0:                stall1 = 0 || cancel1 = 1;
during [t0+1, t1-1]:      stall1= 1;
15     at     t1:                  stall1= 0;
during [t1+1, t2-1]:      stall2= 1;
at     t2:                  stall2= 0;
during [t2+1, t3-1]:      stall3= 1;
at     t3:                  stall3= 0;
20     ...
at     tn:                  stalln= 0;
// assume that no preceding property cancelled this one
during [t0+1, t1]:          cancel1= 0;
25     during [t1+1, t2]:          cancel2= 0;
during [t2+1, t3]:          cancel3= 0;
...
during [tn-1+1, tn]:      canceln= 0;
30     // assume that the processor is ready to execute next instruction
at     t0:                  process_new_instruction_state;
// assume that instruction execution is not interrupted.
during [t0+1, tint]:      not trigger0;
35
<fetch> // This is a cutpoint, see ITL section
// Assume that iw (the freeze variable) contains the instruction
// that should be handled in this property.
40     at     tiv:                 trigger_iwm;
<validate_regs> 
at     tdec:         trigger_statem;
45
prove:
at     tia:                 ibus_read(pc @ t0+1);
<fetch>
50
// Prove that the virtual register file values are valid
// whenever they are to decide upon trigger_state.
# for each reference z to an architecture register file 
#in TRIGGER_STATEm:
55            at tvstage(m,z):          validR,vstage(m,z)(vindexm,z);
# end for each;
<validate_regs> 
60     // Prove that the virtual register file values are valid
// whenever they are required.
# for each reference z to an architecture register file 
# in UPDATEm,R, INDEXm,R, ADDRm, or WDATAm:
at tvstage(m,z):          validR,vstage(m,z)(vindexm,z);
65     # end for each;
at t1:                      process_new_instruction_state;
at tjmp+1:                  pc = updatem,PC;
70     // Prove that the full signals are correctly created.
during [t1+1, t2]:        full2= 1;
during [t2+1, t3]:        full3= 1;
...
during [tn-1+1, tn]:      fulln= 1;
75
// Prove that wrongly fetched instructions are cancelled.
at     tjmp:         primary_canceljmp-1= 1;
// Prove that the cancel creates empty stages
80     at     tjmp + 1:          full2= 0;
at     tjmp + 1:            full3= 0;
...
at     tjmp + 1:            fulljmp= 0;
85
// Prove that this instruction will not initiate further cancels.
during [tjmp+1, tjmp+1]:  primary_canceljmp = 0;
during [tjmp+1+1, tjmp+2]:       primary_canceljmp+1 = 0;
during [tjmp+2+1, tjmp+3]:       primary_canceljmp+2 = 0;
90     ...
during [tn-1+1, tn]:      primary_canceln-1 = 0;
// For all registers that get updated, prove their correct
95     // handling in the pipeline.
# for each register file R with ASSIGNm,R in the architecture 
# description entry: 
# for each stage s = dec + 1, dec + 2, ... writebackR-1
at     ts:                  if result_validR,s = 1
100                                       then next(result_validR,s+1) =  1
end if;
# end for each stage
# for each stage s = dec + 1, dec + 2, ... writebackR
during [ts-1+1, ts]:      result_writeR,s = 1;
105           during [ts-1+1, ts]:      result_destR,s= indexm,R;
during [ts-1+1, ts-1]:    if (result_validR,s = 1)
then next(result_validR,s) =  1
end if;
during [ts-1+1, ts]:      if (result_validR,s = 1)         
110                                       then result_dataR,s = updatem,R;
end if;
# end for each stage 
at twritebackR+1:               currentR(indexR) = updatem,R;
# end for each register
115    # for each register file R with NO_ASSIGNR in the arch. entry: 
# for each stage s = dec + 1, dec + 2, ... writebackR
during [ts-1+1, ts]:      result_writeR,s = 0;
# end for each stage
# end for each register
120    # if the architecture description entry contains DMEM_READ(ADDRm)
at tda:                   dbus_read(addrm);
# else if it contains DMEM_WRITE(ADDRm, WDATAm)
at tda:                   dbus_write(addrm, wdatam);
# else // it contains DMEM_IDLE
125           at tda:                   dbus_idle;
# end if
left_hook:       t0;
right_hook:      tjmp;
130 end property;
１〜７１行目は、プロパティスキーマsimple_instructionと等しく、そこに説明される。
【０１６５】
７７行目は、ジャンプ命令を現在実行するステージよりも下位の番号を有するステージが、すべて取り消されることを証明する。これは、対応情報中のcancelマクロに関するセクションにおいて与えられた、primary_cancelの定義から得られる。
【０１６６】
８０〜８３行目は、ステージ１からステージjmpmに及んで、取り消されたステージが確かに空であることを証明する。
【０１６７】
８７〜９１行目は、ステージjmpmからn-1に及び、このジャンプ命令がそれ以上の取り消しを発行しないであろうことを保証する。
【０１６８】
このプロパティスキーマの９４〜１３０行目は、先のプロパティスキーマの８４〜１２０行目と等しく、そこに説明される。
【０１６９】
割り込み
割り込みに関するアーキテクチャ記述エントリー０について、いくつかのプロパティは、プロパティスキーマinterrupthに従って生成される。これは、値h=1,2,…を取る付加的な変数hによって記述される。
【０１７０】
割り込みはプロセッサ外部から到着する。アーキテクチャ記述の単純化された視点では、割り込みは、いくつかの命令Instと同時に到着する。割り込みがプロセッサによって受理されるか否かは、マクロTRIGGER0（既に導入された）によって、命令Instが実行される前の時点におけるアーキテクチャのステータスを使用して決定される。アーキテクチャのステータスは、例えば、割り込みがマスクされる（即ち観測されない）か否かを示すことができる。
【０１７１】
インプリメンテーション記述へのマッピングは単純ではない。パイプラインは、複数の命令に同時に作用する。どの命令が、割り込みの実行によって置き換えられるべき命令であるとみなされるかを決定することが、実行される必要がある。アプローチは、割り込みが受理されるステージintを定義することである。このステージintは、通常、ジャンプ命令のうちのいずれかが他のステージを取り消すことが可能な最後のステージである。したがって、すべてのjmpmについて、jmpmの値が<=intである必要がある。
【０１７２】
割り込みがプロセッサによって受理される場合に、ステージintが満杯であれば、このステージint中の命令は置き換えられるであろう。ステージintが空の場合、最も高い番号が<intである空でないステージ中の命令は、置き換えられるであろう。以下において、空でないステージ中のこの最も高い番号は、hで表示されるであろう。ステージ１が常に満杯（即ち空でない）であると見なされることに注意する。
【０１７３】
マクロtrigger0は、プロパティスキーマsimple_instructionについて記述された方法で、TRIGGER0から導かれる。マクロtrigger0が割り込みを受理する際の時点は、tirptと表示されるであろう。この時点の後、パイプラインは、パイプラインステージint，int+1などにおいて割り込みを実行する。tint,tint+1,…は、割り込み実行がステージint，int+1,…のそれぞれの１つにある場合の時点を表示し、ストール信号によって前進することが可能である。多くの場合、tirptはtintになるであろうが、このことは必要ではない。tirptの前の、時点t1,t2,…th-1は、時点tirptにおいてステージh中に存在する命令が、それぞれのステージのストール信号によって前進することが可能なところの時点を反映する。そのうえ、続いて起こる証明について、時点th,th+1,…tint-1はtirptであると定義される。
【０１７４】
マクロupdate0,R、index0,R、update0,PC、vindex0,z、addr0およびwdata0が、さらに、アーキテクチャ記述マクロから次のように導かれる。
【０１７５】
UPDATE0,R、INDEX0,R、UPDATE0,PC、VINDEX0,z、ADDR0およびWDATA0がサブ表現へ分解される。定義により、これらサブ表現は、定数、フォームR[VINDEX0,z]で表されるレジスタファイルアクセス、PC、DMEM_RDATA或いはアーキテクチャ割り込み入力IRPTである。派生マクロを得るために、これらサブ表現は次のように置き換えられる。
●  定数は変更されない。
●  R[VINDEX0,z]がdataR,vstage(0,z)(vindex0,z)@tvstage(0,z)に置き換えられる。ここで、vindex0,zは、ここに記述された手順を再帰的に適用することにより、VINDEX0,zから生成される（vstage0,z>=intが要求されることに注意する）。
●  PCがpc@t0+1に置き換えられる（これは常に、割り込みによって削除される最も古い命令のプログラムカウンタPCであることに注意する）。
●  DMEM_RDATAがdbus_rdata@tdvに置き換えられる。
●  IRPTからのアーキテクチャ割り込み信号が、irpt@tirpt中の対応する信号に置き換えられる。
【０１７６】
そして、置き換えられたサブ表現を有する表現が、派生マクロを形成する。
【０１７７】
図４に、生成された可能な割り込みプロパティのタイミング構造を示す。それは、割り込みがストールと共に起こる必要がないことを示す。
【０１７８】
hがあらゆる値、即ちh=1,…intを取ることができる１つのプロパティスキーマがある。
1   property interrupth;
dependencies: no_reset;
for time_points: 
5      t0 = t,
t1> t0,
t2 > t1,
...
th-1> th-2,
10
tirpt> th-1,
th = tirpt,
th+1 = tirpt,
15            ...,
tint-1 = tirpt,
tint>= tirpt,
20            tint+1 > tint, 
…
tn> tn-1;
assume:
25     at     t0:                stall1 = 0 || cancel1 = 1;
during [t0+1, t1-1]: stall1 = 1;
at     t1:                  stall1= 0;
during [t1+1, t2-1]:      stall2= 1;
at     t2:                  stall2= 0;
30     during [t2+1, t3-1]: stall3= 1;
at     t3:                  stall3= 0;
....
during [th-2+1, th-1-1]:  stallh-1= 1;
at     th-1:         stallh-1= 0;
35
during [th-1+1, tirpt-1]: stallh= 1 and not trigger0;
at     tirpt:        trigger0;
during [tirpt, tint-1]:   stallint= 1;
at     tint:         stallint= 0;
40     during [tint+1, tint+1-1]:  stallint+1 = 1;
at     tint+1:              stallint+1= 0;
during [tint+1+1,tint+2-1]: stallint+2 = 1;
at     tint+2:              stallint+2= 0;
...
45     during [tn-1+1, tn-1]:      stalln = 1;
at     tn:                  stalln= 0;
during [t0+1, t1]:          cancel1= 0;
during [t1+1, t2]:        cancel2= 0;
50     during [t2+1, t3]:          cancel3= 0;
...
during [th-1+1, tirpt-1]: cancelh= 0;
during [tirpt+1, tint]:   cancelint= 0;
during [tint+1, tint+1]:  cancelint+1= 0;
55     ...
during [tn-1+1, tn]:      canceln= 0;
// assume that the processor is ready to execute next instruction
at     t0:                  process_new_instruction_state;
60
// Focus h on the highest nonempty stage.
at     tirpt:        fullh+1 = 0;
at     tirpt:        fullh+2= 0;
...
65     at     tirpt:        fullint= 0;
prove:
at tint:                           process_new_instruction_state; 
70     // New PC from interrupt
at tint+1:                  pc = update0,PC;
// Prove that the full signals are correctly created.
during [t1+1, t2]:        full2= 1;
75     during [t2+1, t3]:          full3= 1;
...
during [th-1+1, tirpt-1]: fullh= 1;
during [tirpt+1, tint]:   fullint= 1;
80     during [tint+1, tint+1]:    fullint+1 = 1;
during [tint+1+1, tint+2]:       fullint+2= 1;
...
during [tn-1+1, tn]:      fulln= 1;
85     // Prove that all instructions in the pipeline get removed          
at     tirpt:        primary_cancelint-1= 1;
at     tirpt+1:             full2= 0;
at     tirpt+1:             full3= 0;
90     ...
at     tirpt+1:             fullint-1= 0;
at     tirpt+1:             if prev(stallint) = 0 
then fullint= 0 
95                                 end if;
// Prove that the virtual register file values are valid
// whenever they are required.
// In the index subscripts vstageR,k will be written vstage(R,k).
100    # for each reference to an architecture register file in
# UPDATE0,R, INDEX0,R, ADDR0, or WDATA0:
at tvstage(0,z):          validR,vstage(0,z)(vindex0,z);
# end for each;
105    // Prove that there will not be a second interrupt.
during [tirpt+1, tint]:          trigger0= 0;
// For all registers that get updated, prove their correct
// handling in the pipeline.
110    # for each register file R with ASSIGN0,R in the arch. entry: 
at     tint:                if (tirpt /= tint and 
result_validR,int = 1) 
then next(result_validR,int+1) =  1
end if;
115       # for each stage s = int+1, int+2, ... writebackR-1
at     ts:                  if result_validR,s = 1
then next(result_validR,s+1) =  1
end if;
# end for each stage
120
during [tirpt+1, tint-1]: if (result_validR,int = 1)
then next(result_validR,int) =  1
end if;
during [tirpt+1, tint]:   result_writeR,int = 1;
125           during [tirpt+1, tint]:   result_destR,int = index0,R;
# for each stage s = int + 1, int + 2, ... writebackR
during [ts-1+1, ts]:      result_writeR,s = 1;
during [ts-1+1, ts]:      result_destR,s= index0,R;
130           during [ts-1+1, ts-1]:    if (result_validR,s = 1)
then next(result_validR,s) =  1
end if;
during [ts-1+1, ts]:      if (result_validR,s = 1)                                                          then result_dataR,s = 
135                                                     update0,R;
end if;
# end for each stage 
at twritebackR+1:               currentR(index0,R) = update0,R;
# end for each register
140    # for each register file R with NO_ASSIGNR in the spec entry:
# for each stage s = dec + 1, dec + 2, ... writebackR
during [ts-1+1, ts]:      result_writeR,s = 0;
# end for each stage
# end for each register
145    # if the interrupt description contains DMEM_READ(ADDR0)                          at tda:                   dbus_read(addr0);
# else the interrupt description contains 
# DMEM_WRITE(ADDR0, WDATA0)
at tda:                   dbus_write(addr0, wdata0);
150    # else // no transaction to the data memory
at tda:                   dbus_idle;
# end if
left_hook:       t0;
155 right_hook:    tint;
end property;
生成されたプロパティは、命令がどのように実行を開始するかを記述し、一方では、命令がその後どのように割り込み実行に置き換えられるかを記述する。
【０１７９】
６〜９行目は、ステージ１からh-1に及び、後で置き換えられる命令が、パイプライン中を前進することが可能な時点についての時間変数を導入する。h=1の場合、これらラインはエントリーを明示しない。
【０１８０】
１１行目は、割り込みが受理される際の時間変数tirptを導入する。１３〜１６行目は、hからint-1までのすべてのステージに及び、関連する時間変数tsを導入する。h=intの場合、これら１３〜１６行目はエントリーを明示しない。
【０１８１】
１７行目は、割り込み実行が次のパイプラインステージへ前進する際の時間変数tintを明示する。この時間変数はtirptに一致することができる。
【０１８２】
tirptを除いた、tにいくつかのインデックスを加えたフォームで表されるすべての時点が、アクセスプロトコル記述および対応情報で導入した定数に従ってインデックスを評価することにより、時点t0,t1,…tnのうちの１つを参照することに注意する。しかし、tirptは、他の時点のいずれとも等しくなる必要のない、切り離された時点である。
【０１８３】
２０〜２２行目は、int+1とnとの間のすべてのステージに及び、割り込み実行が次のステージへシフトされる際の時点を導入する。
【０１８４】
これに対して、２５〜４６行目は、信号の動作に従って、適切な時点を用いて時間変数をインスタンス化する。２６〜３４行目はステージ１からh-1に及び、h=1の場合、エントリーが無い状態に縮退する。３６及び３７行目は、置き換えられる命令がステージhにある場合に受理される割り込みの時点として、tirptを導入する。３８及び３９行目は、割り込み実行が前方にシフトされるまで、割り込み実行がステージintにおいてどのように待機するかを表現する。４０〜４６行目は、ステージint+1からnに及び、割り込み実行がどのように前方にシフトされるかを表現する。
【０１８５】
６９行目は、生成されたプロパティが、新しい命令が実行され得る状態から開始すると仮定する。
【０１８６】
６２〜６５行目は、ステージh+1からintに及び、h=intの場合、エントリーが無い状態に縮退し得る。それは、ステージh中にある命令が、確かに最も高位の命令であることを保証する。fullsマクロは対応情報において明示される。
【０１８７】
証明部分では、６９行目において、回路が、新しい命令実行が開始されるところの状態を返すことが示されるであろう。
【０１８８】
７４〜７７行目は、ステージ２からhに及び、h=1の場合、エントリーが無い状態に縮退する。それらは、その後割り込み実行に置き換えられる命令によって、パイプラインステージがどのように満たされるかを示す。fullsマクロは対応情報に由来する。
【０１８９】
７９〜８３行目は、割り込み実行によってステージがどのように満たされるかを表現する。
【０１９０】
８６行目は、ステージint以下のすべてのステージがどのように取り消されるかを示す。８８〜９３行目は、ステージ２からint-1のすべてに及び、取り消し命令がこのステージを確かに空にしたことを証明する。９３行目は、ステージintのstallマクロが０である際に割り込みが受理される場合の、取り消し命令の影響をステージintへ拡張する。
【０１９１】
マクロtrigger0において参照される仮想レジスタの値は、常に有効である必要がある。これは、以下に示すプロパティスキーマinterrupt_regs_validR,kに従って、個別のプロパティにより証明される。したがって、他のアーキテクチャ記述マクロ中の値が、それらが必要とされるステージにおいて有効となることを要求するので十分である。これは１００〜１０３行目において行われる。
【０１９２】
１０６行目は、現在の割り込みが次のステージint+1にシフトする前に、別の割り込みの受理を妨げるいくつかのメカニズムが存在することを要求する。
【０１９３】
１０８〜１５６行目は、プロパティスキーマsimple_instructionの８４〜１２０行目について記述されたのと同様の方法で、レジスタファイルおよびデータバス転送に関する割り込み実行の影響を取り扱う。
【０１９４】
リセット
インプリメンテーションのリセット値に関するプロパティを生成するために、アーキテクチャリセット信号をインプリメンテーションリセット信号に置き換えることにより、マクロTRIGGERinitからマクロtriggerinitが導かれる。
property reset;
assume:
at     t: triggerinit;
prove:
at     t+1: full2 = 0;
at     t+1: full3 = 0;
...
at     t+1: fulln = 0;
# For each register R[k]
at t+1:     currentR(k) = init_valR,k;
# end for each register;
at     t+1:   PC = init_valPC;
at     t+1:   dbus_idle;
at     t+1:   process_new_instruction_state;
right_hook: t+1;
end property;
下記の証明で使用するために、生成されたリセットプロパティは、時点t1,t2,…tnに関連付けられ、tに等しいと定義される。
【０１９５】
補助プロパティスキーマ
対応情報からのマクロに関する制限は、次のプロパティスキーマに捕らえられる。これらプロパティスキーマのすべてについて、プロパティスキーマsimple_instructionについて提示された方法で、マクロTRIGGER0からマクロtrigger0が導かれる。
【０１９６】
cancel_correct：このスキーマから生成されるプロパティは、cancels命令についての対応情報が正確に形成されることを保証する。或るステージが取り消される場合、その先のステージもすべて取り消されなければならない。
property cancel_correct;
dependencies: no_reset;
prove:
at     t:     for each i in 2..n:
if canceli = 1
then canceli-1 = 1
end if;
end for each;
end property;
stall_empty：このプロパティスキーマは、fullsマクロに対応する対応情報によって、命令を実行しないステージに、空であることを示すフラグが正確に立てられることを保証する。マクロtrigger0は、上記したプロパティにおいて使用されるマクロである。
property stall_empty;
dependencies: no_reset;
prove:
at     t:     for each i in 2 .. n
if (not (fulli-1 or (i-1 = int and trigger0)) 
or stalli-1) and 
(not (fulli or (i = int and trigger0)) 
or not stalli))
then 
next(fulli) = 0;
end for each;
end property; 
stall_full：このプロパティスキーマは、ステージ中に隣接する２つの命令がマージされないであろうことを保証する。
property stall_full;
dependencies: no_reset;
prove:
at     t:     for each i in 2 .. n:
if (
(fullior (i = int and trigger0) and 
(fulli-1 or (i-1 = int and trigger0) and
not stalli-1) 
then stalli = 0 
end if;
end for each;
end property;
full_slot：このプロパティスキーマは、fulls対応情報が、命令を実行するステージに正確にフラグを立てることを保証する。
property full_slot;
dependencies: no_reset;
prove:
at     t:     full1= 1 and
for each i in 1 .. n-1: 
if ((fulli = 1 or (i = int and trigger0)) 
and stalli= 0 and canceli = 0)
then next(fulli+1) = 1 
end if;
end for each and 
for each i in 2 .. n:
if ((fulli = 1 or (i = int and trigger0)) 
and stalli= 1 and canceli = 0)
then next(fulli) = 1
end if;
end for each;
end property; 
empty_write：このプロパティスキーマは、空のパイプラインステージが仮想レジスタファイルに書き込むことができないことを保証する。empty_writeプロパティスキーマは、アーキテクチャレジスタファイルのすべてについて繰り返されなければならない。
# for each register R file in the architectural state
property empty_writeR;
dependencies: no_reset;
prove:
at     t:     if (fulldec+1 = 0) then result_writeR,dec+1 = 0 end if and   
if (fulldec+2 = 0) then result_writeR,dec+2 = 0 end if and
...
if (fullwritebackR = 0) then result_writeR,writebackR = 0 end if;
end property;
# end for each register;
write_back：このプロパティスキーマは、すべてのアーキテクチャレジスタファイルについてのインプリメンテーションレジスタファイルcurrentR(k)が更新されない場合、それが変わらないであろうことを保証する。
# for each register R file in the architectural state
property write_backR;
dependencies: no_reset;
prove:
at     t:     for each k in <index range of Ri>
if (stallwritebackR = 1 or
result_writeR,writebackR= 0 or 
result_destR,writebackR/= k)
then next(currentR(k)) = currentR(k)
end if;
end for each;
end property;
# end for each register;
empty_cancel：空のステージが取り消し命令を開始することができないようにするために、プロパティスキーマは取り消し状態を空にする。そのうえ、ステージint及びbeyondは、取り消し命令を全く開始することができない。これはステージ間の関係からの結果である。
property empty_cancel;
dependencies: no_reset;
prove:
at     t:     if (not full2) then primary_cancel1 = 0 end if and
if (not full3) then primary_cancel2 = 0 end if and
...
if (not fullint-1) then primary_cancelint-2 = 0 end if and
if (not (fullint or trigger0)) then 
primary_cancelint-1 = 0 end if and
cancelint= 0 and
cancelint+1 = 0 and
... and
canceln= 0;
end property;
interrupt_regs_valid：このプロパティスキーマは、割り込みが受理されるか否かを決定するために必要とされる値が常に有効であることを要求する。
# for each register R[k] evaluated in TRIGGER0.       
property interrupt_regs_validR,k;
dependencies: no_reset;
prove:
at     t:     validR,int(k);
end property;
# end for each
生存プロパティ
上記した証明は、ストール信号がストールを永久に生成しない場合にのみ、アーキテクチャとインプリメンテーションとの間の等価性を示す。続いてのセクションは、プロパティが生成されるところのプロパティスキーマに捧げられ、そのプロパティスキーマは、ストールが永久に続かないであろうことと、その結果として、すべての割り込み又は命令実行が、インプリメンテーションクロックサイクルの有限数だけ起こることとを示す。
【０１９７】
そのようなプロパティを直接証明することができるアルゴリズムは、最先端技術に存在する。しかしながら、これらアルゴリズムは複雑さの点で制限されている。
【０１９８】
w1,w2,w3,…wnを、wk>wk+1および0<w1を満たすウェイトのセットとする。正確な選択は重要ではない。次に、我々は割り当てwn-k=k+1を選択する。
【０１９９】
パイプライン中のステージs後のトータルウェイトtotalsは、>sであるすべてのfullステージのウェイトの合計である。
【０２００】
totals=fulls+1 * ws+1 + fulls+2 * ws+2 + ... fulln * wn  
トータルウェイトtotalsのこの定義の助けを借りて、次のプロパティスキーマが使用されて、ステージs中のストールが永久に続かないことを示すためのプロパティを生成する。
property liveness_stalls;
assume:
at t:         external_stall = 1;
prove:
at t+1:       (totals <= prev(totals)) or stalls=0;
end property;
property liveness_nostalls;
assume:
at t:         external_stall = 0;
prove:
at t+1:       (totals < prev(totals)) or stalls = 0;
end property;
これらプロパティスキーマは、外部のストールが存在しない場合はいつでも、トータルウェイトtotalsが実際に減少すること、或いは、対応性の点において、パイプラインステージsのstallsが存在しないことを示す。外部のストールが存在する場合は、トータルウェイトtotalsは、stallsが存在しない場合にのみ増大することができる。言いかえれば、stallsが永久にアクティブで、且つ、外部のストールが永久にアクティブでない場合は、トータルウェイトtotalsは負の数にならなければならないであろう。それは矛盾である。したがって、上記した２つのプロパティスキーマは、概して、環境がプロセッサをいつまでもストールさせない場合、ステージsへのストール信号がいつまでもアクティブにならないことを証明する。実行される正確なフォワーディングパスについての明示的なユーザ入力を、プロパティスキーマが要求しないことに注意する。言いかえれば、命令がストールされる場合と命令がストールされない場合との正確な条件を、ユーザが退屈にモデル化する必要がない。上記したプロパティスキーマは、パイプライン化された任意のプロセッサが満たさなければならない最小限の要求を形成する。
【０２０１】
実際、これら２つのプロパティスキーマは、如何なるフォワーディングも全く使用せずに、プロセッサの生存性までをも証明する。ウェイトtotalsは０に達するまで減少するであろう。その場合、ステージsの前に命令はこれ以上存在せず、それゆえに、ステージsをストールさせる内的な理由はこれ以上存在しない。その結果、ステージs中の命令は、メモリストールがない状態でステージs+1に進むであろう。
【０２０２】
証明
このセクションは、すべての生成されたプロパティの証明が、アーキテクチャ記述とインプリメンテーションとの間の等価性を証明するのに十分であることを示す。
【０２０３】
証明の概念
証明によって検査された状況は、アーキテクチャ記述およびインプリメンテーション記述の等価性の定義に従う。同じ命令の内容を有する命令メモリが、インプリメンテーションおよびアーキテクチャの両方に対して接続される。命令メモリは、まるでその命令メモリがアーキテクチャ用の非同期式メモリであったかのように扱われる。これは、命令メモリが、命令メモリから同じサイクル中のリクエスタへ、要求された情報を返すことを意味する。インプリメンテーション記述について、命令メモリはいくつかのレイテンシを有することができ、インプリメンテーションは、ストールを有すること、或いは、アドレスを発行することにより、パイプラインステージ中の異なる命令で命令を読み込むことを考慮する。
【０２０４】
同様に、アーキテクチャおよびインプリメンテーションについて、同じ初期値を用いたデータメモリが与えられる。さらに、アーキテクチャ記述の視点では、データメモリは非同期式であり、読み込みデータが要求されるサイクルの読み込みデータを返す。データは、データが次のサイクルにおいて利用可能であるように書かれている。インプリメンテーションについて、データメモリはいくつかのレイテンシを有することができ、このレイテンシには、ストールを有すること、或いは、パイプラインステージ中の異なるものでアドレスデータおよび読み込みデータを扱うことが考慮される。
【０２０５】
本発明に従ってプロパティが生成され、そして、例えばプロパティチェッカー等のフォーマル検証ツールを用いて、すべてのプロパティがインプリメンテーションに適合することが証明されるであろう。
【０２０６】
証明は、生成されたプロパティがどのようにインプリメンテーションの実行トレースに一致するかを検査するであろう。これら実行トレースは、メモリトラフィックと、割り込み信号irptの動作とを含む。実行トレースは、マクロtriggerinitに従ってリセット動作から開始し、以後、さらなるリセットのアクティブ化を提供しない。証明は、すべての実行トレースが、次のプロパティスキーマreset、simple_instruction、jump_instructionおよびinterrupthから生成されるプロパティのチェーンP0,P1,P2,P3,…に一致し得る（専門用語セクションの意味で）ことを示すであろう。以下、これら生成されたプロパティはメインプロパティと呼ばれるであろう。
【０２０７】
さらに、インプリメンテーションの動作が、プロパティにのみ基づいてただ一つ予測され得ることが示されるであろう。インプリメンテーション記述に対して一旦プロパティが証明されると、インプリメンテーション記述を廃棄することができる。また、それらの論理的な相互関係を考慮に入れて、プロパティについて推論することにより、インプリメンテーション動作を予測することができる。生成されたプロパティ間の論理的な相互関係は、最終パラグラフからの制限に従って、インプリメンテーション割り込みirpt、入力iwによって表わされる命令メモリの内容、読み込みデータ入力dbus_rdataによって表わされるデータメモリの内容、stalls条件の動作、およびリセット動作だけが与えられると、データメモリ及び命令メモリへのアクセスを一意的に予測する。
【０２０８】
証明のこの部分について、メインプロパティのチェーンP0,P1,P2,P3,…は、上記したセクションからの補助プロパティスキーマから生成されたプロパティを用いて記入される、基礎的な構造として役立つ。以下、これらプロパティは補助プロパティと呼ばれるであろう。
【０２０９】
生成されたプロパティがシミュレーションによって検査される場合、プロパティ間のこの論理的に緊密な相互関係は、少なくともバグのうちの１つが、あらゆる次の命令又は割り込みの実行に影響し得る場合、それぞれのプロパティによって、命令又は割り込みの実行を崩壊させるインプリメンテーション中のバグのうちの１つが識別されるであろう効果を有する。
【０２１０】
実行トレースに一致するメインプロパティのチェーンP0,P1,P2,P3,…は、リセット動作（P0）に関するアーキテクチャ記述エントリーのシーケンスと、命令及び割り込み（i>0を満たすPi）の実行とに関連する。これは、インプリメンテーションの割り込み入力irptからアーキテクチャの割り込み入力IRPTへの割り込みマッピングの定義を可能にする。この目的のために、メインプロパティのチェーンP0,P1,P2,P3,…の一致が、プロパティP0,P1,P2,P3,…の各々の時間変数のインスタンス化を必要とすることに注意しなければならない。実行シーケンス中のプロパティスキーマinterrupthから生成されるすべてのプロパティPjについて、割り込み入力IRPT@jはirpt@tirptになる。ここで、tirptは、Pjの基礎となるプロパティスキーマからの時間変数である。この時間変数は、プロパティのチェーンP0,P1,P2,P3,…が実行トレースに一致する方法により、１つの時点にインスタンス化される。
【０２１１】
プロパティスキーマsimple_instruction又はjump_instructionから生成されたすべてのプロパティPjについて、IRPT@jはirpt@tintになる。これは、インプリメンテーションとアーキテクチャとの間の等価性の定義によって要求される割り込みマッピングの存在を示す。
【０２１２】
アーキテクチャが、アーキテクチャ記述中に定義されたリセット状態から開始し、且つ、アーキテクチャが、上記定義されるような割り込み信号IRPTを用いて提供される場合、証明は、アーキテクチャが、アーキテクチャ記述エントリーの同じシーケンスを実行するであろうことを示すであろう。証明はさらに、仮想レジスタファイルから導かれて、証明をするうちに記述されるであろう翻訳語に従って、この実行が同じデータを取り扱うことを示すであろう。
【０２１３】
このことから、同じシーケンス中で、同じアドレスデータと同じ書き込みデータとを用いて、データメモリアクセスがなされるであろうことが推定可能である。このことは、次に、読み込みトランザクションのすべてに同じデータが読み込まれることを強制する。これで等価性証明を終える。
【０２１４】
プロパティの後のデータ
対応情報に定義された仮想レジスタファイルを用いて、インプリメンテーション状態がどのようにアーキテクチャ状態へマッピングされるかが、今示されるであろう。マッピングの結果として、それぞれのメインプロパティは、仮想レジスタファイルが、そのメインプロパティによって記述される命令又は割り込みの実行によってどのように修正されるかを記述する。
【０２１５】
この目的のために、ステージ関数Sが導入される。t1<=t2,t2<=t3,…tw-1<=twである所定の有限数の時点のシーケンスt1,t2,…twについて、メインプロパティにおいて時点のシーケンスt1,t2,…twが生じる場合、関数S(t)は、関数S(t)が次のものを返すように定義される。
●  t<=t1の場合、値１
●  tが区間[ti-1+1,ti]内にある場合、値i
●  t>twの場合、w+1
プロパティスキーマsimple_instructionおよびjump_instructionの状況下において、tがt1とtnとの間に位置することが提供されると、関数S(t)は、命令が時間に依存して実行されるところのステージの番号を返す。このため、この関数S(t)は、時点のシーケンスt1,t2,…twについてのステージ関数と呼ばれる。
【０２１６】
プロパティスキーマinterrupthの状況下において、t>=tirptが提供されると、S(t)は、割り込みが時間に依存して実行されるところのステージの番号を返す。
【０２１７】
実行トレースをカバーするメインプロパティのチェーン中のすべてのプロパティ、すべてのアーキテクチャレジスタファイルR、および、right_hook<v<w<=twritebackR+1であるすべての時点v及びwについて、仮想レジスタファイルに関する次の整合性表現が、適合することが示されるであろう。
【０２１８】
validR,S(v)-1(k) @ v -> validR,S(w)-1(k) @ w
and    validR,S(v)-1(k) @ v -> (dataR,S(v)-1(k) @ v = dataR,S(w)-1(k) @ w)
一旦これが示されれば、さらなる結論は次のとおりである。定義により、表現validR,writebackR(k)=1であるため、少なくとも時点u=twritebackR+1について、時点uにおける表現validR,S(u)-1(k)は真になる。初期の時点において表現validR,writebackR(k)が真になる場合、時点uにおけるdataR,S(u)-1(k)は、この時点uから前方への時点twritebackR+1まで定数になるであろう。従って、メインプロパティの後の仮想レジスタファイルの値であるとして、仮想レジスタファイルが有効になった後の、仮想レジスタファイルが有する或る特定の値について証明することが正確である。
【０２１９】
主な帰納法仮定
証明は帰納法によって行われる。帰納法仮定は、すべてのj>=0について、次の推測が適合する。
１．  証明概念に関するセクションからのリセット制限に続くすべての実行トレースについて、実行トレースの最初の部分に一致するメインプロパティの有限のチェーンP0,P1,P2,…Pjが存在する。
２．  仮想レジスタファイルについての整合性表現が、メインプロパティPjについて適合する。
３．  すべてのアーキテクチャレジスタR[k]@j+1の値が、メインプロパティPjの後の仮想レジスタファイルの値に等しい。
４．  メインプロパティPjがインプリメンテーションの実行トレースに一致する方法で提供される時点right_hook+1において、j番目のアーキテクチャサイクルの後のアーキテクチャプログラムカウンタPC@j+1の値が、インプリメンテーションプログラムカウンタpcの値に等しい。
５．  Pjおよびj番目のアーキテクチャサイクルが、データメモリからの或いはデータメモリへの同じトランザクションを記述する。
６．  そのうえ、Pjの区間[right_hook+1,tint]内に受理される割り込みが存在しない。即ち、この区間内のすべての時点についてtrigger0=偽である。
【０２２０】
以下において、この帰納法仮定は主な帰納法仮定と呼ばれるであろう。
【０２２１】
ベースケース
ベースケースは、アーキテクチャ及びインプリメンテーション両方のリセットに関する。アーキテクチャのリセットは、アーキテクチャ記述中のリセットのアクティビティブロックであるACTinitに従って、レジスタファイル値を提供する。これは、レジスタファイル値R[k]@1を与え、そしてさらに、プログラムカウンタ値PC@1を与える。レジスタ値およびプログラムカウンタの値PCは、最初のアーキテクチャ状態AS1を形成する。
【０２２２】
インプリメンテーションに関するリセットプロパティの適用は、すべての時点t1,t2,…tnを、リセットがアクティブ化される時点tにセットする。従って、インプリメンテーションのリセット状態は、時点t+1に到達する。
【０２２３】
主な帰納法仮定の推測１は、すべての実行トレースが関数triggerinitに従ってリセット動作から開始されることが要求されるので、このような状況において自明である。したがって、プロパティスキーマresetから生成されたプロパティP0が適合する。そのうえ、プロパティP0はデータメモリアクセスを記述しない。
【０２２４】
主な帰納法仮定の推測２は、この場合、区間[right_hook,twritebackR+1]が１つの要素のみを含むので、このような状況において自明である。
【０２２５】
推測３は、アーキテクチャ中のすべてのアーキテクチャレジスタが、インプリメンテーション中のcurrentR@t+1と同じ値にリセットされるという事実の直接的な結果である。
【０２２６】
推測４は、アーキテクチャ及びインプリメンテーションの両方のプログラムカウンタのリセットのため、適合する。
【０２２７】
推測５は、リセットがデータバス要求を発行しないので、適合する。
【０２２８】
推測６は、区間[right_hook+1,tint]が空であるので、適合する。
【０２２９】
ベースケースはプロパティスキーマresetによって検査される。それは、pc及びすべての仮想レジスタファイルが、リセット後のアーキテクチャと同じ値を含むことを保証する。
【０２３０】
帰納法ステップ
帰納法ステップは、j番目のアーキテクチャサイクルについて帰納法仮定が適合すると仮定する。帰納法ステップが、j+1番目のアーキテクチャサイクル及びメインプロパティPj+1についても適合することが、今示されなければならない。この目的のために、メインプロパティのチェーンP0,P1,P2,…Pj+1が実行トレースの最初の部分に一致するような、すべての実行トレースについてのメインプロパティPj+1が存在することが示されなければならない。その後、アーキテクチャが、関連するアーキテクチャ記述エントリーを実行し、同じデータを生成することが示されなければならない。
【０２３１】
以下において、メインプロパティPjの時点は、T0,T1,T2,Tnで表示されるであろう。Tq=メインプロパティPjのright_hookであるn以下の最も高いインデックスであるように、qが選択されるであろう。
【０２３２】
Pj+1の候補
ストール信号の生存性のために、stall1@t’1=0である第１の時点t’1>Tqが存在し、stall2@t’2=0である第２の時点t’2>t’1が存在し、時点t’3,…t’nについても同様に存在する。マクロtrigger0が区間[Tint+1,t’int-1]内のどこかで満たされる場合、この区間[Tint+1,t’int-1]内には、少なくとも１つの受理された割り込みが存在する。tirptを、割り込みが受理される区間内の第１の時点、即ち、trigger0@tirpt=1であるような第１の時点とする。この状況において、Pj+1になることが可能な唯一の候補は、プロパティスキーマinterrupthから生成されたメインプロパティのうちの１つである。ここで、Sはt’1,t’2,…t’nについてのステージ関数であり、h=S(tirpt)である。しかしながら、そのようなプロパティの適用範囲は、まだ確認を必要とする。この確認を容易にするために、時点t0,t1,…tnは、このプロパティスキーマにおいて使用される方法で定義される。即ち、t0=Tq,t1=t’1,t2=t’2,…th-1=t’h-1,th=tirpt,th+1=tirpt,…tint-1=tirptであり、tintは、stallint@tint=0を満たし且つ>=tirptである第１の時点であり、tint+1は、stallint+1@tint+1=0を満たし且つ>tintである第１の時点であり、tint+2,tint+3,…tnについても同様である。
【０２３３】
区間[Tint+1,t’int-1]の全体にわたって、マクロtrigger0が０である場合、割り込みマッピングは、IRPT@j+1がirpt@t’intになるように定義される。この状況において、irpt@t’intは、trigger0@t’intが１又は０かどうかに応じて、受理された割り込みを譲り渡すことができる又はできない。受理された割り込みが存在する場合、tirpt=tintであるプロパティスキーマinterruptintから生成されたプロパティは、Pj+1の候補である。割り込みがない場合、プロパティスキーマsimple_instruction又はjump_instructionから生成されたプロパティは、Pj+1の候補である。しかしながら、そのようなプロパティの適用範囲は、まだ確認を必要とする。この確認を容易にするために、時点t0,t1,…tnは、t0=Tq,t1=t’1,t2=t’2,…tn=t’nであると定義される。
【０２３４】
一旦証明が終了すると、上記したセクションは、等価性の定義によって要求される、インプリメンテーションの割り込み入力からアーキテクチャの割り込み入力へのマッピングを提供する。
【０２３５】
空の領域
PjとPj+1の候補との間のタイミング関係は、いくつかの図中に例示される。
●  図５は、プロパティスキーマsimple_instructionから生成された２つのメインプロパティPjおよびPj+1を示す。
●  図６は、プロパティスキーマreset(q=n)、jump_instruction(q=jmpm)、simple_instruction、interrupt(tirpt=tintの場合、q=int、tirpt<tintの場合、q=int-1)、もしくはsimple_instructionからプロパティが生成され、引き続き、プロパティスキーマsimple_instruction又はjump_instructionからプロパティが生成される一般的な場合を示す。q=1の場合、図６は図５に縮退する。
●  図７は、プロパティスキーマreset、simple_instruction、jump_instruction、もしくはinterrupthのうちから１つのプロパティが生成され、引き続き、プロパティスキーマinterrupthからプロパティが生成される一般的な場合を示す。ここで、qは上記説明したように割り当てられる。
【０２３６】
これらの図は、命令固有の演算と、命令固有の演算間のペア（時間、ステージ）の領域とを示す。所定のステージsについて、このペアの領域は、[2,q]内のステージsについては、Tq+1=t0+1から開始し、s>qであるステージについては、Ts+1から開始する。所定のステージsの１つについて、その領域は、上記で包括的に導入された時点ts-1において終了するまで、右側に拡張する。
【０２３７】
この領域について、その領域内の時点tにおいてステージsが空であること、即ち、区間[max(Tq,Ts)+1,ts-1]内のすべてのtについて、fulls@t=0であることが示されるであろう。これは２つの結論を有する。第１に、取り消しの欠如に関する仮定部分が満たされることが示され得る。第２に、Pjの後の仮想レジスタの値が、Pj+1によって要求されている仮想レジスタ値になることが示されるであろう。
【０２３８】
空の領域に関する証明は、二次元の帰納法によって実行されるであろう。ステージが増大する方向の帰納法は、帰納法の時間経過によりそれら自身を証明するベースケース及びステップケースによって実行されるであろう。
【０２３９】
以下において、プロパティスキーマの補助的なものから生成されるプロパティと、補助プロパティスキーマ自身とは区別されない。したがって、プロパティ<name>は、「補助プロパティスキーマ<name>から生成されたプロパティ」についての略語として書かれるであろう。補助プロパティスキーマから生成されるプロパティは常に１つだけ存在するので、これは明白である。
【０２４０】
ステージsにわたる帰納法についてのベースケースは、s=2である。
●  時間にわたる帰納法についてのベースケースはt=max(Tq,T2)+1である。
○  2<=qの場合、Pjは、プロパティスキーマjump_instruction、interrupth、もしくはresetのうちの１つから生成される。これがq=1に関連付けられるため、Pjはプロパティスキーマsimple_instructionから生成され得ない。従って、T2<=Tqであり、また、メインプロパティPjの証明部分から、full2@Tq+1=0である。
○  q=1の場合、区間が空でないかどうかだけを証明することがあり、このことはT2<t1を要求し、stall2@T2=0である。さらに、t1が、stall1を用いないT1後の次の時点であると定義されたので、stall1@T2=1である。そして、プロパティstall_emptyから、それはfull2@T2+1=0に従う。
●  時間にわたる帰納法についてのステップケース：wを[T2+1,t1-1]内の時点とする。帰納法仮定は、full2@w=0の仮定を可能にする。そして、stall1@w=1であり（t1が、T1後のステージ１の最初のノーストールであるので）、プロパティstall_emptyから、それはfull2@w+1=0に従う。
【０２４１】
これは、ステージにわたる帰納法についてのベースケースを証明する。
【０２４２】
sからs+1への帰納法ステップ：sを区間[2,n-1]内のいくつかのステージとする。帰納法仮定から、[max(Tq,Ts)+1,ts-1]内のすべての時点について、fulls=0に従う。
【０２４３】
ステージにわたる帰納法ステップは、さらに、帰納法の時間経過によって証明される。
●  ベースケースt=max(Tq,Ts+1)+1は、qおよびs+1の関係にわたる帰納法のケースを要求する。
○  第１に、s+1<=qが検査される。これは、プロパティPjがプロパティスキーマreset、jump_instruction、もしくはinterrupthから生成されることを意味する。それは、fulls+1@Tq+1=0を直接証明する。
○  q<s+1の場合、Ts+1<tsであるならば、区間[max(Tq,Ts+1)+1,ts]は要素のみを含む。qの定義からTs<Ts+1であり、従ってstalls+1@Ts+1=0である。ts-1とTs+1との関係について、場合分けが行われる必要がある。
■  ts-1<Ts+1の場合、Ts+1は区間[ts-1+1,ts-1]内に存在する。したがって、stalls@Ts+1=1である。そして、プロパティstall_emptyは、fulls+1@Ts+1+1=0と結論され得る。
■  Ts+1<=ts-1の場合、時点Ts+1は区間[ts+1,ts-1]内に存在する。したがって、ステージにわたる帰納法仮定は適用可能であり、fulls@Ts+1=0を示す。Ts+1において受理される割り込みが存在しない場合、或いは、s/=intの場合、プロパティstall_emptyが適用可能であり、fulls+1@Ts+1+1=0を示す。s=int、且つTs+1において割り込みが受理される場合、Ts+1=tirptである。tintはtirpt以上であり、ノーストールを有する最初の時点であると定義される。tint>Tint+1と予想されるので、stalls@Tint+1=1に従う。したがって、プロパティstall_emptyは、さらに、fullint+1@Tint+1+1=0を示す。
●  ステップ：区間[max(Tq,Ts+1)+1,ts-1]内のいくつかの時点wについて、fulls+1@w=0が証明されるとする。
○  fulls+1@w+1を決定するために、Ts+1<tsであれば、時間w=tirptにおいて受理される割り込みのみが関連性を有することができる。したがって、s=intである。そのうえ、stallint@tirpt=1である。これは、プロパティstall_emptyの適用を可能にし、このことは、fulls+1@tirpt+1=0を与える。
○  残りの場合について、時間wにおいて受理された割り込みは、それゆえに除外され得るか、或いは、プロパティstall_emptyの適用には無関係である。
■  w<=ts-1の場合、ステージsに関する帰納法仮定は適用可能であり、fulls@w=0を与える。したがって、プロパティstall_emptyは適用可能であり、これはfulls+1@w+1=0を示す。
■  ts-1<wの場合、wは[ts-1+1,ts-1]内にある。この区間内には、stalls@w=1が存在し、したがって、プロパティstall_emptyの適用が、fulls+1@w+1=0を提供する。
【０２４４】
これは帰納法ステップを証明する。
【０２４５】
これは要求全体を証明する。
【０２４６】
取り消し
tを、t0+1=Tq+1とtnとの間の（および含む）時点とする。U(t)を、T1,T2,…Tnに関連付けられたステージ関数とする。L(t)を、t1,t2,…tnに関連付けられたステージ関数とする。
【０２４７】
明らかに、少なくともL(t)<=U(t)である。以下に示されるであろうが、これは、L(t)<U(t)に強められ得る。
【０２４８】
cancelL(t)@t=0が証明されるであろう。これは、区間[L(t),max(U(t),n)]内のすべてのsについて、cancels@t=0を証明することにより行われる。
【０２４９】
このことは、ステージsにわたる帰納法により、見ることができる。
●  ベース：t<=Tnの場合、メインプロパティPjの仮定部分がcancelU(t)@t=0を提供し、証明部分がprimary_cancelU(t)-1@t=0を提供する。Pjが適用可能であると示されたので、仮定部分はその状況を記述する。これはcancelU(t)-1@t=0を示す。t>Tnの場合、U(t)=n+1であり、canceln@t=0が、プロパティemtpy_cancelから得られる。これはベースケースを証明する。
●  ステップ：区間[L(t)+1,U(t)-1]内のいくつかのステージsについて、cancels@t=0であるとする。int<sの場合、帰納法仮定は、プロパティemtpy_cancelから直接的に得られ、cancels-1@t=0である。このようにしてprimary_cancelが定義されるので、s<=intの場合、cancels-1@t=cancels@t、もしくはprimary_cancels-1@tである。帰納法仮定からcancels@t=0であり、プロパティempty_cancelからprimary_cancels-1@t=0であり、よってcancels-1=0である。これは、ステップケース、よって要求全体を証明する。
【０２５０】
この証明の結果は、候補プロパティPj+1の次の条件が満たされることを示す。
【０２５１】
during [t0+1, t1]: cancel1 = 0;
during [t1+1, t2]: cancel2 = 0; 
during [t2+1, t3]: cancel3 = 0;
...
during [tn-1+1, tn]: canceln = 0;
スロットの解体
時点tおよびステージsからのスロットは、
at     t:                          stalls= 0; 
during [ts+1, ts+1-1]:           stalls+1= 1;
at     ts+1:                       stalls+1 = 0;
...
during [tn-1+1, tn]:             stalln= 1;
at     tn:                         stalln= 0;
を用いて、時点(t,ts+1,ts+2,…tn,tn+1)のシーケンスであると定義される。
【０２５２】
命令及び割り込みはスロット内において実行される。命令スロットはステージ１内の時間t1から開始し、プロパティPjがプロパティスキーマsimple_instructionもしくはjump_instructionから生成された場合、命令スロットは、すべてのt>=Tqについて、fulls@tによりマークされることが証明される。割り込みスロットはステージint内の時間tintから開始し、プロパティPjがプロパティスキーマinterrupthから生成された場合、割り込みスロットは、fulls@tによりマークされることが証明される。命令実行の場合にt1,t2,…tnによって定義される命令スロットと、割り込みの場合にtint,tint+1,…tnによって定義される割り込みスロットとについて、プロパティfull_slotは、fulls=1@tが、時間tにおける命令又は割り込みをステージsが実行することを意味することをも示す。
【０２５３】
これは、２つの命令実行又は割り込み実行の命令スロット又は割り込みスロットが、決してマージしないであろうことを示す。fulls@t=1およびfulls@t’=1である異なる時点tおよびt’において、同じステージsから開始する２つのスロットが存在するとすると、すべてのステージiについて、区間[ti+1,ti+1]及び[t’i+1,t’i+1]が解体されるという意味で、スロットが解体される。
【０２５４】
これは次のように見ることができる。t<t’且つ、スロットがオーバラップするいくつかの時点及びいくつかのステージが存在すると仮定すると、区間[ts’-1+1,ts’]及び[t’s’-1+1,t’s’]が交差するところの最初のステージがいくつか存在する。これら両方の区間内の最後の時点を除くすべての時点については、stalls’=1であるので、ts’=t’s’と結論され得る。よって、[t’s’-1+1,t’s’]は[ts’-1+1,ts’]のサブセットである。プロパティfull_slotの結果から、[ts’-1+1,ts’]内のすべての時点について、fulls’=1である。その他、区間がステージs’-1において交差するであろうことと、s’が、そのような最も小さいステージであると仮定されたこととから、ts’-1<t’s’-1である。したがって、fulls’@t’s’-1=1およびfulls’-1@t’s’-1=1である。スロットの定義から、stalls’-1@t’s’-1=1でもあり、これは、プロパティstall_fullへの矛盾を形成する。
【０２５５】
これは、２つの命令実行が決してマージしないであろうことを示す。従って、L(t)<U(t)である。
【０２５６】
レジスタ値
すべてのアーキテクチャレジスタR[k]については、区間[tdec-1+1,twritebackR]内の２つの時点v<=wの両方について、
validR,L(v) @ v -> validR, L(w) @ w and
validR,L(v) @ v -> dataR,L(v)(k) @ v = R[k] @ j + 1
が証明される。
【０２５７】
最後の等式は、主な帰納法仮定からの結果である。さらに、TRIGGER0が依存するすべてのレジスタR[k]と、区間[Tint+1,tint]内のすべてのvとについて、
validR,int(k) @ v and (dataR,int(k) @ v = R[k] @ j + 1)
が証明されるであろう。
【０２５８】
この目的のために、レジスタR[k]のうちの１つと、区間[t0+1,tn]内の１つの時点とが検査される。区間[dec,writebackR]内のパイプラインステージsについて、validR,sおよびdataR,sのみが定義されるので、関数は、この制限を考慮するステージ関数U及びLから導かれなければならない。l(t)をmax(dec,L(t))、u(t)をmin(U(t)、writebackR+1)とすると、帰納法により、[l(t),u(t)-1]内のすべてのステージsについて、
validR,s(k) @ t = validR,u(t)-1(k) @ t
が証明される。
【０２５９】
証明：ベースケースs=u(t)-1において示されることは何もない。
【０２６０】
sからs-1へのステップ：[l(t)+1,u(t)-1]内のいくつかのsについて、上記した要求が適合するとすると、定義から、
validR,s-1(k)@ t = (if (result_writeR,s and result_destR,s = k)
then result_validR,s 
else validR,s(k)) @ t
である。
【０２６１】
プロパティempty_writeは適用可能であり、fulls@t=0を考慮すると、したがって、result_writeR,s=0であり、よって、validR,s-1(k)@t=validR,s(k)@tである。これはステップ及び要求を証明する。
【０２６２】
そのうえ、
validR,s(k) @ t -> dataR,s(k) @ t = R[k] @ j + 1
が証明されるであろう。
【０２６３】
ベースケース：この目的のために、要求は最初に、s=u(t)-1について証明されるであろう。これは帰納法仮定からの直接的な結果であるので、t<=Tn+1である限り、証明するものは何もない。tが区間[Tn+1,tn-1]内にある場合、fullwritebackR@t=0である。よって、プロパティempty_writeRは、result_writeR,writebackR@t=0の結果を提供し、プロパティwrite_backRは、dataR,writebackR(k)@t+1=dataR,writebackR(k)@t=R[k]@j+1と結論し得る。tが区間[tn-1+1,tn-1]内にある場合、同じ等式が、stalln=1およびプロパティwrite_backRから得られる。したがって、上記した要求はs=u(t)について適合する。
【０２６４】
sからs-1へのステップ：sからs-1へのステップについての推論は、validR,s(k)に関する推論に従う。定義により、
dataR,s-1(k) @ t =
(if result_writeR,s and result_destR,s = k 
then result_dataR,s
else dataR,s(k)) @ t
である。
【０２６５】
result_writeR,s@t=0（プロパティempty_writeから）であるので、dataR,s-1(k)@t=dataR,s(k)@t=R[k]@j+1である。
【０２６６】
プロパティinterrupt_regs_validR,kが妥当性を保証するので、validR,int(k)およびdataR,int(k)に関する要求は、最後の証明からの結果である。このセクションの最初の要求は、validR,s(k)、dataR,s(k)、定義によるvalidR,writebackR=1という事実、および帰納法仮定に関する推論からの結果である。
【０２６７】
プロパティスキーマinterrupthから生成されたプロパティの適用
次に、３つのプロパティスキーマsimple_instruction、jump_instructionもしくはinterrupthのうちの１つから生成されたプロパティPj+1が、常に適用可能であることが示されるであろう。プロパティPj+1の候補がプロパティスキーマinterrupthから生成されれば、そのプロパティが確かに適用可能であることが、今示されるであろう。
【０２６８】
プロパティからの時間変数が、上記定義されるような時点t0,t1,…tnおよびtirptを用いて実証される場合、stallsおよびtrigger0（プロパティスキーマinterrupth中の２５〜４６行）に関する条件はすべて満たされる。そのうえ、cancelsに関するセクションは、cancels（４８〜５６行目）に関する仮定部分が満たされることを示す。また、空の領域に関するセクションは、値fullh+1,fullh+2,…fullint（６２〜６５行目）に関する仮定を証明する。
【０２６９】
５９行目のprocess_new_instruction@t0に関する仮定は、メインプロパティPj中のprocess_new_instruction@Tqの証明によって破棄される。
【０２７０】
これは、プロパティスキーマinterrupthのうちの１つが適用可能であることを示す。
【０２７１】
割り込みマッピングとアーキテクチャレジスタおよび仮想レジスタに関する推論とは、TRIGGER0@j+1が、trigger0@tirptと同じ方法で同じ値を評価するであろうことを示す。したがって、アーキテクチャは、そのj+1番目のサイクル中で割り込みを実行するであろう。
【０２７２】
主な帰納法仮定がj+1について有効であることが、今示されなければならない。
【０２７３】
推測１は、すべての可能なメインプロパティへの注視を要求する。したがって、現在の証明の状態について、割り込みがあるべき場合は常にPj+1が存在することにのみ注目することができる。
【０２７４】
推測２は、Pj+1の後の仮想レジスタについて、整合性表現の証明を要求する。
【０２７５】
R[k]をアーキテクチャレジスタとする。v<=wを、区間[tint+1,twritebackR+1]内の２つの時点とし、Sを、時点t1,t2,t3,…tnに関連付けられたステージ関数とすると、 
validR,S(v)-1(k) @ v = 
(if (result_writeR,S(v)and result_destR,S(v) = k)
then result_validR,S(v) 
else validR,S(v)(k)) @ v
および
validR,S(w)-1(k) @ w = 
(if (result_writeR,S(w)and result_destR,S(w) = k)
then result_validR,S(w) 
else validR,S(w)(k)) @ w
である。
【０２７６】
メインプロパティPjは、result_writeR,s(v)@v=result_writeR,S(w)@wを決定する。双方が１である場合、双方がindex0,Rに等しいので、result_destR,S(v)@v=result_destR,S(w)@wである。ここで、index0,Rは、アーキテクチャオブジェクトを、或る特定の時点における信号を評価する表現で置き換えることによって、INDEX0,Rから導かれる。
【０２７７】
従って、validR,s(v)-1(k)@v=result_validR,s(v)@vおよびvalidR,s(w)-1(k)@w=result_validR,s(w)@v、或いは、validR,S(v)-1(k)@v=validR,s(v)(k)@vおよびvalidR,s(w)-1(k)@w=validR,S(w)(k)@wの何れかである。両方の場合において、含意
validR,L(v)-1(k) @ v -> validR,L(w)-1(k) @ w
が適合する。１番目はPj+1の証明部分からの結果であり、２番目はレジスタに関する推論からの結果である。
【０２７８】
同様の考察は、dataR,s(v)-1(k)@vとdataR,S(w)-1@wとの値の同一性を示す。validR,L(v)-1(k)@v=1の場合、result_writeR,S(v)@v=result_writeR,s(w)@wおよびresult_destR,S(v)@v=result_destR,S(w)@wである。このことは、メインプロパティPj+1の証明部分の直接的な結果である。したがって、どちらもvalidR,L(v)-1(k)@v=result_validR,L(v)@v=1である。よって、result_validR,L(w)@w=1であり、したがって、dataR,s(v)-1@v=update0,R@vおよびdataR,S(w)-1@w=update0,R@wである。すべてのアーキテクチャオブジェクトを、或る特定の時点におけるインプリメンテーション信号を参照する表現で置き換えることによって、UPDATE0,Rからupdate0,Rが導かれるので、この場合、双方の表現は等しい。
【０２７９】
dataR,s(v)@v=dataR,s(v)-1@vおよびdataR,S(w)@w=dataR,S(w)-1@wである場合、同一性は、レジスタファイル値に関する考察から得られる。これは、主な帰納法仮定の推測２を証明する。
【０２８０】
したがって、メインプロパティPj+1後のR[k]の値について証明することが可能である。この値は次のように計算される。tを、validR,L(t)-1(k)@t=1であるような、区間[tirpt+1,twritebackR+1]内の時点であるとすると、
dataR,L(t)-1(k) @ t =
(if result_writeR,L(t) and result_destR,L(t) = k 
then result_dataR,L(t)
else dataR,L(t)(k)) @ t
である。
【０２８１】
result_writeR,L(t)およびresult_destR,L(t)=k@tが満たされる場合、validR,L(t)-1(k)@t=result_validR,L(t)@tおよびdataR,L(t)-1(k)@t=result_dataR,L(t)である。そして、Pj+1の証明部分は、update0,Rが特定の時点における信号を評価するところにおいて、result_dataR,L(t)@t=update0,R@tirprを保証する。特定の時点は、update0,Rが、update0,R自身が評価される時点に依存しないUPDATE0,Rから導かれる方法によって定義される。また、k=index0,R@tirptであり、これもまた評価の時点に依存しない。証明部分エントリーは、update0,R内に読み込まれたすべての仮想レジスタ値が有効であることを保証する。したがって、主な帰納法仮定は、それらがR[k]@j+1の関連する値に等しいことを示す。よって、R[k]@j+2=dataR,L(t)-1(k)@tであるように、update0,R@t=UPDATE0,Rおよびindex0,R@t=INDEX0,R@j+1である。
【０２８２】
result_writeR,L(t)およびresult_destR,L(t)=kが満たされない場合、同様の考察は、R[k]@j+1=R[k]@j+2を示す。したがってまた、R[k]@j+2=dataR,L(t)-1(k)@tである。これは、主な帰納法仮定の推測３を証明する。
【０２８３】
同様に、命令Pj+1の後のPCとj+1番目のアーキテクチャサイクルのPCとの同一性が示されて、推測４を証明する。
【０２８４】
同様に、インプリメンテーション及びアーキテクチャが等しいメモリトランザクションを実行することが示され、それにより推測５を証明することができる。
【０２８５】
Pj+1の[right_hook+1,tint]間に受理された割り込みが存在しないという要求は、それぞれの証明部分から得られ、これは推測６を証明する。
【０２８６】
プロパティスキーマsimple_instructionもしくはjump_instructionから生成されるプロパティの適用
今、区間[Tint+1,tint]内において割り込みが受理されない場合を考える。この場合、上記定義された時点t0,t1,t2,…もまた存在し、プロパティスキーマsimple_instruction或いはjump_instructionスキーマから生成されたプロパティの時間変数が、それに応じて実証される場合、ストール動作（プロパティスキーマsimple_instructionおよびjump_instruction中の１３〜２１行目）に関する仮定がさらに満たされる。
【０２８７】
取り消し動作に関する推論は、関連する仮定（２４〜２８行目）が満たされることを示す。
【０２８８】
process_new_instruction@t0（３１行目）に関する仮定は、メインプロパティPj中のprocess_new_instruction@Tqの証明によって破棄される。
【０２８９】
これは、部分的なプロパティsimple_instruction.fetchもしくはjump_instruction.fetchの仮定部分が満たされることを示す。したがって、帰納法仮定により、PC@j+1に等しいアドレスpc@t1を用いて、命令メモリへのリードアクセスが実行されることが証明される。したがって、命令メモリは、インプリメンテーションについて同じ命令語iw@tivを返し、アーキテクチャについてIW@j+1を返す。
【０２９０】
この検査の前提条件として、命令メモリは有効な命令のみを返すことが上記に言及される。したがって、少なくとも１つ、あるいはさらに、TRIGGER_IWm=1を有する複数のアーキテクチャ記述エントリーが存在する。これらアーキテクチャ記述エントリーのすべてについて、部分的なプロパティsimple_instruction.validate_regsもしくはjump_instruction.validate_regsの仮定trigger_iwmが、今満たされる。これは、すべてのtrigger_statemが、有効な仮想レジスタ値に基づいて評価されることを示す。上記した割り込みについての推論と同様に、trigger_statem@tdec=TRIGGER_STATEm@j+1と見ることができる。同じTRIGGER_IWmについてのおそらく複数のTRIGGER_STATEmが、完全な場合分けを形成することは、この検査の要求に属する。したがって、TRIGGER_STATEmおよびTRIGGER_IWmが両方とも満たされるところの、１つの仕様エントリーmが存在する。このエントリーについて生成されるプロパティは、Pj+1になるであろう。その適用範囲は既に示されている。
【０２９１】
これは、メインプロパティのチェーンP0,P1,P2,…Pjに既に一致する最初の部分を有するすべての実行トレースについて、実行トレースのより長い最初の部分に、メインプロパティのチェーンP0,P1,P2,…Pj+1を一致させるメインプロパティPj+1が、常に見つかり得ることを示す。
【０２９２】
これは、主な帰納法仮定の推測１を証明する。
【０２９３】
主な帰納法仮定の推測２、３、４および５は、プロパティスキーマinterrupthから生成されるプロパティについて、上記示したように示される。
【０２９４】
そして、メインプロパティのチェーンP0,P1,P2,…Pjに一致する任意の実行トレースが与えられると、Pjの時間変数のインスタンス化が存在する。そして、このインスタンス化により、帰納法仮定の推測６は、区間[Tq+1,tint]（TはPjの時点に関係する）内のすべての時点について、trigger0=0を仮定することが可能になる。Pj+1の時間変数t0について、t0<=Tintである。したがって、[t0+1,Tint]内のすべての時点について、trigger0=0である。区間[Tint+1,tint]内において受理された割り込みは、プロパティスキーマinterrupthから生成されたプロパティの適用に関するセクションによって扱われる。Pj+1がプロパティスキーマsimple_instructionもしくはjump_instructionから生成される場合、[Tint+1,tint]内において受理される割り込みは存在しない。これは、主な帰納法仮定の推測６を証明する。
【０２９５】
これで証明を終える。証明の重要な結論の１つは、すべての生成されたプロパティがインプリメンテーションに適合すると証明され得るように、対応情報が提供される場合、対応情報の正確な形態が無関係であることである。したがって、対応情報は、検証プロセスに、アーキテクチャ記述およびインプリメンテーション記述の等価でないペアについての等価性を、誤って出力させることができない。
【実施例】
【０２９６】
ユーザ入力は、次の特徴を有する例証用の小型プロセッサを使用して実証された。
●  ８つのレジスタを有する１つのレジスタファイルREGを備える。
●  プログラムカウンタPCを備える。
●  ４ステージのパイプラインによって実装される。
●  フォワーディングをサポートする。
●  データメモリによって開始されるストールをサポートする。
●  いくつかの典型的な命令をサポートする。これら命令は次にリストされ、命令のオペランドが記述されるであろう。完全な命令は、何が行われなければならないかを選択するためのオペコードと、そのオペコードに従って解釈される必要があるオペランドとから構成される。これらはすべて命令語からデコードされる。命令のリストは次の通りである。
○  NOT：コマンドによってレジスタが選択され、レジスタの内容がビット反転される。その結果はデスティネーションレジスタに格納される。デスティネーションレジスタのアドレスも命令によって与えられる。
○  ADD/SUB：コマンドによって２つのソースオペランドレジスタが選択される。その結果はデスティネーションレジスタに書き込まれる。デスティネーションレジスタのアドレスは命令によって与えられる。
○  LD：命令によってレジスタが選択され、いくつかのベースアドレスを提供する。命令によって提供されるオフセットが、ベースアドレスに加えられるであろう。これは、データメモリからデータがロードされるところのアドレスを与える。
○  ST：命令によってレジスタが選択され、ベースアドレスを提供する。命令によって提供されるオフセットが、ベースアドレスに加えられるであろう。これは、データメモリへの書き込み要求のアドレスを与える。命令はまた、レジスタのデータが格納されるところのレジスタのアドレスを提供する。
○  BEQZ：命令によってレジスタが選択される。このレジスタが０である場合、ジャンプが実行されるであろう。ジャンプの実行とは、命令によって提供されるオフセットが、命令メモリ内において命令が見つかるところのアドレスに加えられることを意味する。これは、次の命令のアドレスを与える。レジスタが０でない場合、ジャンプは実行されず、プログラムカウンタは命令のサイズによってインクリメントされるであろう。
●  命令BEQZの場合、プロセッサは命令が得られないと推測する。第２のステージにおいて、ソースレジスタファイルが０であるという条件が確認され、このことは、ステージ１における命令の取り消しを導くことができる。
●  割り込みは、信号int_valid_iを通じてプロセッサに到着する。レジスタREG[0]が０である場合、その割り込みは受理される。割り込みサービスルーチンの後にプロセッサが返さなくてはならないアドレスは、レジスタREG[0]内に格納されるであろう。割り込みの場合には、割り込みサービスルーチンの開始アドレスが、割り込み入力に属する入力int_addr_iによって提供される。
【０２９７】
アーキテクチャ
アーキテクチャ入力
標準化されたメモリ入力（上記の記述を参照）に加えて、アーキテクチャは、割り込みが到着し得るところの入力INT_VALID_I、割り込みサービスルーチンの最初のアドレスを定義する入力INT_ADDR_I、およびプロセッサをリセットするための入力RESET_Nを有する。
【０２９８】
アーキテクチャ状態
アーキテクチャ状態は、レジスタファイルREGおよびプログラムカウンタPCである。
【０２９９】
アーキテクチャ記述エントリー
初期化
プロセッサはresetをアクティブ化することによって初期化される。この初期化は次の表現によって捕らえられる。
TRIGGERinit:= RESET_N = 0;
初期化が完了した後、プロセッサは、すべてのアーキテクチャ状態が０を生成する状態である。したがって、対応するアクティビティブロックACTinitは次の通りである。
PC :=                0;
REG[0] :=            0;
REG[1] :=            0;
REG[2] :=            0;
REG[3] :=            0;
REG[4] :=            0;
REG[5] :=            0;
REG[6] :=            0;
REG[7] :=            0;
割り込み
割り込みが受理される条件は次で与えられる。
TRIGGER0:=         INT_VALID_I and REG[0] = 0;
次に続くアクティビティブロックACT0は、上記で述べられたことに従って、割り込み実行を記述する。
UPDATE0,PC:=              INT_ADDR_I;
UPDATE0,REG :=            PC;
INDEX0,REG :=             0;
DMEM_IDLE0
アクティビティブロックの最後のエントリーは、データメモリへのアクセスが実行されないという事実を参照する。
【０３００】
算術／論理命令
関連する命令についてのオペコードを含む定数add、sub、not、等などが定義されるであろう。
【０３０１】
算術／論理命令が実行される方法は、プロセッサ状態に依存せず、命令語にのみ依存する。これはトリガによって反映される。命令ADDについて、トリガは次のとおりである。
TRIGGER_IW1  :=    IW[15:11] = add;
TRIGGER_STATE1:=   true;
アクティビティブロックは、PCのインクリメントと、命令に従ったレジスタファイルREGの更新とを明示する。
UPDATE1,PC :=        (PC + 2)[7 :0];
UPDATE1,REG :=       (REG[IW[10:8]] + REG[IW[7:5]])[15:0]
INDEX1,REG :=             IW[4:2];
VINDEX1,1:=        IW[7:5];
VINDEX1,2:=        IW[10:8];
DMEM_IDLE1
同様に命令SUBについて
TRIGGER_IW2  :=    IW[15:11] = sub;
TRIGGER_STATE2:=   true;
UPDATE2,PC :=             (PC + 2)[7 :0];
UPDATE2,REG:=      unsigned((REG[IW[10:8]] - REG[IW[7:5]])[15:0])
INDEX2,REG :=             IW[4:2];
VINDEX2,1:=        IW[7:5];
VINDEX2,2:=        IW[10:8];
DMEM_IDLE2
命令NOT
TRIGGER_IW3  :=    IW[15:11] = not;
TRIGGER_STATE3:=   true;
UPDATE3,PC :=        (PC + 2)[7 :0];
UPDATE3,REG :=       ~ REG[IW[10:8]] 
INDEX3,REG :=             IW[4:2];
VINDEX3,1:=        IW[10:8];
DMEM_IDLE3
メモリ命令
メモリ命令の興味深い部分は、アクティビティブロックがエントリーDMEM_READもしくはDMEM_WRITEを含むことと、読み込み命令のアクティビティブロックが、読み込みデータ用のマクロDMEM_RDATAを使用することとである。
【０３０２】
命令LD
TRIGGER_IW4  :=    IW[15:11] = ld;
TRIGGER_STATE4:=   true;
UPDATE4,PC :=             (PC + 2)[7 :0];
UPDATE4,REG :=       DMEM_RDATA; 
INDEX4,REG :=        IW[10:8];
VINDEX4,1:=        IW[7:5];
DMEM_READ4((IW[4:0] + REG[IW[7:5]]) [7:0])
命令ST
TRIGGER_IW5  :=    IW[15:11] = st;
TRIGGGER_STATE5:=  true;
UPDATE5,PC :=             (PC + 2)[7 :0];
No assignment to REG
VINDEX5,1 :=              IW[10:8];
VINDEX5,2:=        IW[7:5]
DMEM_WRITE5((IW[4:0] + REG[IW[7:5]]) [7:0],  REG[IW[10:8]])
条件付きジャンプ
ジャンプが起こるか否かに依存して、条件付きジャンプは、本質的に異なる２つの動作を有する。これは、自明でないtrigger_stateマクロを有する２つのアーキテクチャ記述エントリーによって反映される。例示的な命令はBEQZである。
【０３０３】
ジャンプが起こらない
TRIGGER_IW6  :=    IW[15:11] = beqz;
TRIGGER_STATE6:=   REG[IW[10:8]] /= 0;
UPDATE6,PC :=             (PC + 2)[7 :0];
VINDEX6,1:=        IW[10:8];
No update for REG.
DMEM_IDLE6
ジャンプが起こる
TRIGGER_IW7  :=    IW[15:11] = beqz;
TRIGGER_STATE7:=   REG[IW[10:8]] = 0;
UPDATE7,PC :=             (PC + IW[7:0])[7 :0];
INDEX7,1:=         IW[10:8];
No update for REG.
DMEM_IDLE7
対応情報
パイプラインステージの分類
パイプラインステージの総数は次の通りである。
n             = 4
また、デコードは第２のステージにおいて行われる。
dec           = 2
ほとんどのアーキテクチャ記述エントリーはジャンプに言及しない。アーキテクチャ記述エントリーの最後の１つのみが、ジャンプが起こることに関係する。また、このジャンプは、第２のステージにおいて、取り消されるステージがステージ１のみであるように決定される。
jmp1          = 1
jmp2          = 1
jmp3          = 1
jmp4          = 1
jmp5          = 1
jmp6          = 1
jmp7          = 2
割り込みはステージ３において受理される。これは、他のすべての命令が割り込みによって取り消されるであろうのに対して、ステージ４の命令が、割り込みによって取り消されないであろうことを意味する。
int           = 3
１つのアーキテクチャレジスタファイルREGのみが存在し、データはステージ４から書き戻されるであろう。
writebackREG       = 4
プロセッサ内のデータはすべて、ステージ２であるデコードステージにフォワードされる。したがって、この命令がステージ２に存在し、且つ、ステージ２がストールしない場合、命令によって必要とされるデータはすべて有効でなければならない。
vstage1,1     = 2;
vstage1,2     = 2;
vstage2,1     = 2;
vstage2,2     = 2;
vstage3,1     = 2;
vstage4,2     = 2;
vstage5,2     = 2;
vstage6,1   = 2;
vstage7,1   = 2;
ストール条件
例証用のプロセッサは、各ステージ毎に、特定のストール信号を１つも持たない。代わりに、ストール条件がいくつかの信号から構成される。これはストールに関する対応情報によって捕らえられる。この対応情報は、関連するステージが命令を前進させない条件を説明する設計者から得られた。
stall1        :=     id_stall && id_full;
stall2        :=     id_stall;
stall3        :=     mem_stall || stall_i;
stall4        :=     mem_stall;
取り消し条件
プロセッサは特定の取り消し信号を持たない。さらに、取り消し条件は、単一の信号よりもむしろ、複数の表現によって表現される。
cancel1       :=     (!id_stall && opcode == beqz && full2) || int_valid_i;
cancel2       :=     int_valid_i;
cancel3       :=     0;
cancel4       :=     0;
Full条件
full2         :=     id_full && !id_squash;
full3         :=     ex_full;
full4         :=     ma_full;
開始状態
process_new_instruction_state := true;
プログラムカウンタ
pc            :=     if_pc;
レジスタ
プロセッサはレジスタファイルREGのみを持つ。
result_write_REG3    := ex_full && ex_write_reg && !int_valid_i;
result_write_REG4    := ma_full && ma_write_reg;
result_valid_REG3    := ex_full && !ex_read_from_mem;
result_valid_REG4    := ma_full && !mem_stall;
result_dest_REG3     := ex_dest_reg;
result_dest_REG4     := ma_dest_reg;
result_data_REG3     := ex_result;
result_data_REG4     := real_ma_result;
current_REG(unsigned reg_no) := register[reg_no];
アクセスプロトコル記述
命令メモリアドレスは第１のステージにおいて渡される。
ia            = 1
その実行が第２のステージにある場合、命令そのものが到着する。
iv            = 2
データメモリとのコミュニケーションは、アドレスを渡すためのステージ３と、読み込みデータを受信するためのステージ４とに分割される。
da            = 3
dv            = 4
これらマクロは、プロセッサがどのように命令メモリに読み込みを合図し、プロセッサ信号がどのようにデータメモリを読み込む、或いはデータメモリに書き込むかを説明する。
ibus_read(net[] pc) := imem_addr_o == pc;
iw :=         instruction_word; 
dbus_idle := !ex_dmem_enable_o || int_valid_i; 
dbus_read(net[] addr) := ex_dmem_enable_o 
&& ! ex_dmem_write_o
&& ex_result[7:0] == addr;
dbus_rdata := dmem_data_i; 
dbus_write(net[] addr, wdata) := ex_dmem_enable_o 
&& ex_dmem_write_o
&& ex_result[7:0] == addr
&& ex_dmem_data_o == wdata;
プロパティ生成
add命令についてのプロパティ生成が、このセクションにおいて述べられる。
【０３０４】
レジスタファイルREGに関する対応情報は、「仮想レジスタファイル」セクションに従って結合され、すべての適用可能なステージs、即ち、ステージ２、３、もしくは４について、マクロdata_REGs(k)およびvalid_REGs(k)を構築する。
【０３０５】
次に、適切なプロパティスキーマが選択される。アーキテクチャ記述エントリー１中に記述されるADD命令の場合、ユーザは、対応情報jmp1=1を用いて、アーキテクチャ記述ブロックがジャンプ命令を明示しないことを明示した。したがって、プロパティスキーマsimple_instructionが適用される。
【０３０６】
その後、アーキテクチャ状態がインプリメンテーション信号に置き換えられる必要がある。このステップにおいて、マクロTRIGGER0、TRIGGER_IW1、TRIGGER_STATE1、INDEX1,R、UPDATE1,R、UPDATE1,PC、VINDEX1,i、ADDR1およびWDATA1が、trigger0、trigger_iw1、trigger_state1、index1,R、update1,R、update1,PC、vindex1,i、addr1およびwdata1に置き換えられなければならない。この変換について記述された規則によれば、TRIGGER0についての置き換えは次の通りである。
【０３０７】
trigger0= int_valid_i and data_REG3(0)
対応情報に注目すると、関連する置き換えが以下に与えられるであろう。便利であればどこへでも、直接的な置き換えの結果は、より読み取りやすい形式と共に示される。
【０３０８】
ibus_read(iaddr)     = imem_addr_o = iaddr; 
trigger_iw1        = ((iw @ t2)[15:11] = add)
= (iw[15:11] @ t2 = add)
trigger_state1       = true;
update1,PC           = ((pc @ t1) + 2)[7:0];
update1,REG          = ((data_REG2 @ t2)((iw @ t2)[10:8])) + 
((data_REG2 @ t2)((iw @ t2)[7:5])) 
= (data_REG2(iw[10:8]) + data_REG2(iw[7:5])) @ t2;
index1,REG           = (iw @ t2)[4:2]
= iw[4:2] @ t2;
vindex1,1            = (iw @ t2)[10:8];
vindex1,2            = (iw @ t2)[7:5];
アクティビティブロックACT1がDMEM_IDLEを明示する（それは、メモリアクセスがなされないことを意味する）ので、DATA1およびWADDR1についての置き換えは必要ではない。
【０３０９】
今や、プロパティスキーマのプレースホルダーはすべて、マクロの形式で提供される。行われるであろう残りのことは、命令およびインプリメンテーションについてのプロパティスキーマを拡張することである。インプリメンテーションに対するプロパティの証明を通じて、要求されるプロパティにマクロが拡張され、この拡張は今や、要求されるプロパティを提供する。
property add_instruction;
dependencies: no_reset;
for time_points: 
t0 = t,
t1 > t0,
t2> t1, 
t3> t2,
t4> t3;
assume:
// Describe the slot that is occupied by the instruction
at     t0:                stall1 = 0 || cancel1 = 1;
during [t0+1, t1-1]:      stall1= 1;
at     t1:                  stall1= 0;
during [t1+1, t2-1]:      stall2= 1;
at     t2:                  stall2= 0;
during [t2+1, t3-1]:      stall3= 1;
at     t3:                  stall3= 0;
during [t3+1, t4-1]:      stall4= 1;
at     t4:                  stall4= 0;
// assume that no preceding property cancelled this one
during [t0+1, t1]:          cancel1= 0;
during [t1+1, t2]:        cancel2= 0;
during [t2+1, t3]:        cancel3= 0;
during [t3+1, t4]:        cancel4= 0;
// assume that the processor is ready to execute next instruction
at     t0:                  process_new_instruction_state;
// assume that instruction execution is not interrupted.
during [t0+1, t3]:        not trigger0;
<fetch> // This is a cutpoint, see ITL section
// Assume that iw contains the instruction
// that should be handled in this property.
at     t2:                  trigger_iw1;
<validate_regs> 
at     t2:                  trigger_state1;
prove:
at     t1:                  ibus_read(pc @ t0+1);
<fetch>
// Prove that the virtual register file values are valid
// whenever they are to decide upon trigger_state.
// ... trigger_state does not reference them here.
<validate_regs> 
// Prove that the virtual register file values are valid
// whenever they are required.
at     t2:                  validREG,2(vindex1,1);
at     t2:                  validREG,2(vindex1,2);
at t1:                      process_new_instruction_state;
at t1+1:                           pc = update1,PC;
// Prove that the full signals are correctly created.
during [t1+1, t2]:        full2= 1;
during [t2+1, t3]:        full3= 1;
during [t3+1, t4]:        full4= 1;
// Prove that this instruction will not initiate cancels.
during [t1+1, t2]:        primary_cancel1= 0;
during [t2+1, t3]:        primary_cancel2= 0;
during [t3+1, t4]:        primary_cancel3= 0;
// For all registers that get updated, prove their correct
// handling in the pipeline. 
at     t3:                  if result_validR,3 = 1
then next(result_validR,4) =  1
end if;
during [t2+1, t3]:        result_writeR,3 = 1;
during [t3+1, t4]:        result_writeR,4 = 1;
during [t2+1, t3]:        result_destR,3= index1,R;
during [t3+1, t4]:        result_destR,4= index1,R;
during [t2+1, t3-1]:             if (result_validR,3 = 1)
then next(result_validR,3) =  1
end if;
during [t3+1, t4-1]:             if (result_validR,4 = 1)
then next(result_validR,4) =  1
end if;
during [t2+1, t3]:        if (result_validR,3)
then result_dataR,3 = update1,R;
end if;
during [t3+1, t4]:        if (result_validR,4)
then result_dataR,4 = update1,R;
end if;
at t4+1:                           currentR(indexR) = update1,R
// there is no register in this example that does not get updated.
// the architecture description contains DMEM_IDLE
at tda:                            dbus_idle;
left_hook:    t0;
right_hook:   t1;
end property;
このプロパティのインスタンス化は、部分的なプロパティadd_instruction.fetchおよびadd_instruction.validate_regsの証明部分を等しくする。それは、部分的なプロパティadd_instruction.validate_regsの証明がスキップされることを意味する。
【０３１０】
参考文献
[BD94] Jerry R. Burch, David L. Dill: Automatic verification of Pipelined Microprocessor Control. CAV 1994: 68-80
[VB00] M. N. Velev and R. E. Bryant. Formal verification of superscalar microprocessors with multicycle functional units, exception, and branch prediction. In DAC. ACM, 2000.
[PJB99] Vishnu A. Patankar, Alok Jain, Randal E. Bryant: Formal Verification of an ARM Processor. VLSI Design 1999: 282-287
[BCBZ02] Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu: Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design 20(2): 159-186 (2002)
[SCLA+04] Oliver Schliebusch, Anupam Chattopadhyay, Rainer Leupers, Gerd Ascheid, Heinrich Meyr, Mario Steinert, Gunnar Braun, Achim Nohl: RTL Processor Synthesis for Architecture Exploration and Implementation. DATE 2004: 156-160
[SHNB+04] Oliver Schliebusch, Andreas Hoffmann, Achim Nohl, Gunnar Brown, Heinrich Meyr: Method and Apparatus for Translating to a Hardware Description Language from an Architecture Description Language, Patent, 
Publication number:WO2004017232
Publication date:2004-02-26
Applicant:COWARE INC (US)
Classification: - international:G06F17/50; G06F17/50; (IPC1-7): G06F17/50 - European: G06F17/50D
Application number:WO2003US25602 20030815 
Priority number(s):US20020403882P 20020816; US20030641457 20030814
[BCDM86] Browne, Clarke, Dill, Mishra: Automatic Verification of Sequential Circuits Using Temporal Logic. 
[BS01] Bormann, Spalinger: ”Formale Verifkation fur Nicht-Formalisten (Formal Verification for Non-Formalists”, Bormann, J. and Spalinger, C: (2001), Informationstechnik und Technische Informatik, Vol. 43, Issue 1/2001, Oldenburg Verlag.
[FKL03]: Foster, Krolnik, Lacey: Assertion Based Design: Kluwer 2003
[BW99]: Bormann, Warkentin: Verfahren zum Vergleich elektrischer Schaltungen, EP 1068580 B1.
[BB05]: Bormann, Busch: Verfahren zur Bestimmung der Gute einer Menge von Eigenschaften, verwendbar zur Verifikation und zur Spezifikation von Schaltungen, European Patent Application 05 020 124.3
[BB06]: Bruno, Blackmore: Verifying the Tricore2 Multithreaded Microprocessor, Design Con 2006
【図面の簡単な説明】
【０３１１】
【図１】図１は本発明に係る例示的なプロセスを示す。
【図２】図２はプロパティスキームsimple_instructionにおけるタイミングを示す。
【図３】図３はジャンプ命令のタイミング関係を示す。
【図４】図４は生成された割り込みプロパティの可能なタイミング構造を示す。
【図５】図５はプロパティスキーマsimple_instructionから生成された２つのメインプロパティPjおよびPj+1を示す。
【図６】図６はプロパティスキーマresetから生成されたプロパティの一般的な場合を示す。
【図７】図７はプロパティスキーマresetから生成されたプロパティのうちの１つの一般的な場合を示す。
【図８】図８はプロセッサの設計を示す。
【図１】
2008181490.tif 000003
【図２】
2008181490.tif 000004
【図３】
2008181490.tif 000005
【図４】
2008181490.tif 000006
【図５】
2008181490.tif 000007
【図６】
2008181490.tif 000008
【図７】
2008181490.tif 000009
【図８】
2008181490.tif 000010
【外国語明細書】
2008181490000001.pdf
2008181490000002.pdf
2008181490000003.pdf
2008181490000004.pdf