(57)【要約】【課題】検証対象で処理を実行する際に参照する参照データ値に依存して実行結果が未定義になる場合がある。実行結果が未定義となった場合、以降の処理がその実行結果を参照した場合その実行結果は両者で異なる値となる。その結果、実行結果の比較ができなくなり検証が継続できない。【解決手段】検証対象と期待値生成装置に同一のテストパターンを与えてシミュレーションし互いの実行結果を比較する検証装置において、シミュレーション中のデータを抽出する。そして、抽出データの解析結果に基づいて、シミュレーションを制御する。あるいは、未定義結果となった後のシミュレーションを制御する。これにより、未定義結果となる処理の実行を未然に防ぐ。【選択図】  図３
2005208762.tif 000002
【特許請求の範囲】
【請求項１】
１個以上のプロセッサを含む回路データ部と、シミュレーション装置と、期待値生成装置と、比較装置と、データ情報抽出装置と、実行制御装置とを有し、
前記シミュレーション装置は、前記プロセッサで実行可能な命令のシミュレーション動作を前記回路データ部で実行してシミュレーション結果を生成するものであり、
前記期待値生成装置は、前記命令をシミュレーションする際の期待値を生成するものであり、
前記比較装置は、前記シミュレーション結果と前記期待値とを比較するものであり、
前記データ情報抽出装置は、前記期待値生成装置が前記期待値を生成する際に参照する情報または生成した期待値を抽出するものであり、
前記実行制御装置は、前記データ情報抽出装置が抽出した情報に基づいて、前記命令がそのデータ制約条件を満たすか否かを判断し、その判断結果に基づいて前記シミュレーション装置と前記期待値生成装置とにおける前記命令の実行を制御するものである、ことを特徴とする検証装置。
【請求項２】
請求項１に記載の検証装置において、
前記実行制御装置は、前記データ情報抽出装置が抽出した情報を格納しているレジスタ値を観測することで、前記命令がそのデータ制約条件を満たすか否かを判断するものである、ことを特徴とする検証装置。
【請求項３】
請求項１記載の検証装置において、
前記実行制御装置は、前記判断結果に基づいて前記シミュレーション装置と前記期待値生成装置とにおける前記命令の実行を停止するものである、ことを特徴とする検証装置。
【請求項４】
請求項３記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令を前記データ制約情報格納部に照合することで、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記シミュレーション装置と前記期待値生成装置とを停止させる制御装置と、を有することを特徴とする検証装置。
【請求項５】
請求項１記載の検証装置において、
前記シミュレーション装置は、前記実行制御装置からの停止解除通知を受けるまで当該シミュレーション装置のシミュレーション動作を停止させる実行待機装置を有し、
前記期待値生成装置は、当該期待値生成装置を、直前に実行した命令の実行前の状態に遷移させる前状態戻り装置を有し、
前記実行制御装置は、
前記期待値生成装置での前記命令の実行結果である期待値が、実行結果として保証不可能な未定義結果となるか否かを判定する未定義結果判定装置と、
前記判断結果が、前記期待値が未定義結果であることを示す場合、前記実行待機装置によって前記シミュレーション装置の命令実行を停止させるとともに、前記前状態戻り装置によって前記期待値生成装置の状態遷移動作を実施させる制御装置と、を有することを特徴とする検証装置。
【請求項６】
請求項１記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令を前記データ制約情報格納部に照合することで、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、当該命令を、前記データ制約条件を有さない他の命令に置換したうえで、前記シミュレーション装置と前記期待値生成装置とで実行させる制御装置と、を有することを特徴とする検証装置。
【請求項７】
請求項１記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令を前記データ制約情報格納部に照合することで、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記命令を、その参照データがデータ制約条件を満たす命令に修正したうえで、その修正命令を前記シミュレーション装置と前記期待値生成装置とで実行させる制御装置と、を有することを特徴とする検証装置。
【請求項８】
請求項７に記載の検証装置において、
前記制御装置は、データ制約条件を満たさない参照データを有する命令の当該参照データを、データ制約条件を満たす他の参照データに置換したうえで、その命令を前記シミュレーション装置と前記期待値生成装置とで実行させるものである、ことを特徴とする検証装置。
【請求項９】
請求項８記載の検証装置において、
前記制御装置は、
前記参照データ解析装置によってデータ制約条件を満たさない参照データを有すると判定された命令の他の参照データ候補を探索する参照データ候補探索装置と、
前記参照データ候補探索装置で探索された前記他の参照データ候補が前記データ制約条件を満たすか否かを解析する参照データ候補解析装置と、
前記他の参照データ候補が前記データ制約条件を満たす場合、前記参照データを前記参照データ候補に置換する参照データ置換装置と、を有することを特徴とする検証装置。
【請求項１０】
請求項７に記載の検証装置において、
前記制御装置は、データ制約条件を満たさない参照データを参照する命令の当該参照データを更新する更新命令を作成したうえで、その更新命令を、前記命令より時間的に前において前記シミュレーション装置と前記期待値生成装置とで実行させるものである、ことを特徴とする検証装置。
【請求項１１】
請求項１０記載の検証装置において、
前記制御装置は、
前記参照データ解析装置によってデータ制約条件を満たさない参照データを参照すると判定された命令の当該参照データを、データ制約条件を満たす参照データに更新する更新命令を生成する命令生成装置と、
前記更新命令を、前記命令より時間的に前において前記シミュレーション装置と前記期待値生成装置とで実行可能に配置する命令配置装置と、を有することを特徴とする検証装置。
【請求項１２】
請求項１記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部のデータ制約情報に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記シミュレーション装置と前記期待値生成装置とにおいて前記命令の参照データを、そのデータ制約条件を満たすように強制的に更新する制御装置と、を有することを特徴とする検証装置。
【請求項１３】
請求項１記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部のデータ制約情報に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記シミュレーション装置と前記期待値生成装置とにおいて前記命令を実行した結果として得られるシミュレーション結果と期待値とを、互いに同一の値となるように更新する制御装置と、を有することを特徴とする検証装置。
【請求項１４】
請求項１記載の検証装置において、
前記データ情報抽出装置は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するものであり、
前記実行制御装置は、
前記命令がその実行時に参照する参照データの制約条件の有無と、その制約条件の内容とを格納するデータ制約情報格納部と、
前記データ情報抽出装置が抽出する前記命令と前記参照データとを、前記データ制約情報格納部に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析装置と、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析装置と、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記シミュレーション装置と前記期待値生成装置とにおいて前記命令を実行した結果として得られるシミュレーション結果と期待値とを更新する更新命令を生成したうえで、当該更新命令を、前記シミュレーション装置と前記期待値生成装置で実行させる制御装置と、を有することを特徴とする検証装置。
【請求項１５】
１個以上のプロセッサを含む回路データ部で命令のシミュレーション動作を実施してその命令のシミュレーション結果を求めるとともに、前記命令を用いて当該命令をシミュレーションする際の期待値を求めたうえで、前記シミュレーション結果と前記期待値との比較に基づいて前記回路データ部の検証を行う方法において、
前記期待値を生成する際に参照する情報または生成した期待値を抽出する抽出工程と、
前記抽出工程で抽出した情報に基づいて、前記命令がそのデータ制約条件を満たすか否かを判断する判断工程と、
前記判断工程による判断結果に基づいて、前記命令のシミュレーション動作と前記命令の期待値生成動作とを制御する制御工程と、を含むことを特徴とする検証方法。
【請求項１６】
請求項１５に記載の検証方法において、
前記制御工程は、前記抽出工程において抽出した情報を格納しているレジスタ値を観測することで、前記命令がそのデータ制約条件を満たすか否かを判断する工程である、ことを特徴とする検証方法。
【請求項１７】
請求項１５記載の検証方法において、
前記データ制約条件として、前記参照データの値域を制限する条件を含むものを用いる、ことを特徴とする検証方法。
【請求項１８】
請求項１５記載の検証方法において、
前記制御工程は、前記判断工程による判断結果に基づいて前記命令のシミュレーション動作と前記命令の期待値生成動作とを停止させる工程である、ことを特徴とする検証方法。
【請求項１９】
請求項１８記載の検証方法において、
前記抽出工程は、前記期待値生成動作を実行する前記命令と、その命令の期待値生成動作時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出する前記命令の前記参照データがデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記命令のシミュレーション動作と前記命令の期待値生成動作とを停止させる制御ステップと、を含むことを特徴とする検証方法。
【請求項２０】
請求項１９記載の検証方法において、
前記制御ステップは、次の命令として、前記データ制約条件の無い前記命令または前記データ制約条件を満たす前記命令が供給されるまで、前記命令のシミュレーション動作と前記命令の期待値生成動作とを停止させるステップである、ことを特徴とする検証方法。
【請求項２１】
請求項１５記載の検証方法において、
前記制御工程は、前記判断工程による判断結果に基づいて前記命令の次に実行される次命令のシミュレーション動作と当該次命令の期待値生成動作との実行を制御する工程である、ことを特徴とする検証方法。
【請求項２２】
請求項２１記載の検証方法において、
前記制御工程は、前記判断工程による判断結果に基づいて、前記命令のシミュレーション動作を停止させるとともに、当該命令の期待値生成動作を、動作実行前の状態に遷移させる工程である、ことを特徴とする検証方法。
【請求項２３】
請求項２２記載の検証方法において、
前記抽出工程は、前記命令の期待値生成動作によって得られる前記期待値を抽出する工程であり、
前記制御工程は、
前記命令の期待値生成動作によって得られる期待値が、前記命令の実行結果として保証不可能な未定義結果となるか否かを判定する未定義結果判定ステップと、
前記判断結果が、前記期待値が未定義結果であることを示す場合、前記命令のシミュレーション動作を停止させるとともに、当該命令の期待値生成動作を、動作実行前の状態に遷移させる前状態戻りステップと、
を含む、ことを特徴とする検証方法。
【請求項２４】
請求項１５記載の検証方法において、
前記抽出工程は、前記期待値生成動作で実行される命令とその命令の実行時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出した前記命令と前記参照データとを、前記命令がその実行時に参照する参照データの制約条件に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令がデータ制約条件を有する場合、当該命令の参照データを、当該命令がその実行時に参照する参照データの制約条件に照合することで、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、当該命令を、前記データ制約条件を有さない他の命令に置換したうえで、当該命令のシミュレーション動作と期待値生成動作とを実行する制御ステップと、を含むことを特徴とする検証方法。
【請求項２５】
請求項１５記載の検証方法において、
前記抽出工程は、前記期待値生成動作で実行される命令とその命令の実行時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出した前記命令と前記参照データとを、前記命令がその実行時に参照する参照データの制約条件に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、当該命令を、その参照データがデータ制約条件を満たす命令に修正したうえで、その修正命令のシミュレーション動作とその修正命令の期待値生成動作とを実行する制御ステップと、を含むことを特徴とする検証方法。
【請求項２６】
請求項２５記載の検証方法において、
前記制御ステップは、前記命令の前記参照データが前記データ制約条件を満たさない場合、当該命令の参照データを、前記データ制約条件を満たす他の参照データに置換するステップである、
ことを特徴とする検証方法。
【請求項２７】
請求項２６に記載の検証方法において、
前記制御ステップは、
前記参照データ解析ステップでデータ制約条件を満たさない参照データを有すると解析された前記命令の他の参照データ候補を探索する候補探索処理と、
前記候補探索処理で探索された前記他の参照データ候補が前記データ制約条件を満たすか否かを解析する候補解析処理と、
前記参照データを、前記データ制約条件を満たす前記他の参照データ候補に置換する参照データ置換処理と、を含むことを特徴とする検証方法。
【請求項２８】
請求項２５記載の検証方法において、
前記制御ステップは、前記命令の前記参照データが前記データ制約条件を満たさない場合、当該命令の参照データを、データ制約条件を満たす参照データに更新する更新命令を生成し、当該更新命令により前記参照データを更新したうえで、前記命令のシミュレーション動作と前記命令の期待値生成動作とを実行させるステップである、
ことを特徴とする検証方法。
【請求項２９】
請求項２８記載の検証方法において、
前記制御ステップは、前記命令の参照データがそのデータ制約条件を満たさない場合、当該命令の参照データを、データ制約条件を満たす参照データに更新する更新命令を生成する更新命令生成処理と、
前記更新命令が、前記命令のシミュレーション動作と前記命令の期待値生成動作との実行前に実行されるように、当該更新命令を配置する命令配置処理と、を含むことを特徴とする検証方法。
【請求項３０】
請求項１５記載の検証方法において、
前記制御工程は、前記判断工程により前記参照データが前記データ制約条件を満たさないと判断する場合、前記参照データを、前記データ制約条件を満たすデータに更新する工程である、ことを特徴とする検証方法。
【請求項３１】
請求項３０記載の検証方法において、
前記抽出工程は、前記期待値生成動作で実行される命令とその命令の実行時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出する前記命令と前記参照データとを、前記命令がその実行時に参照する参照データの制約条件に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、当該参照データを、データ制約条件を満たす参照データに強制的に更新したうえで、前記命令の前記シミュレーション動作と前記期待値生成動作とを実行させる制御ステップと、を有することを特徴とする検証方法。
【請求項３２】
請求項２４記載の検証方法において、
前記制御工程は、前記判断工程により前記参照データが前記データ制約条件を満たさないと判断する場合、前記命令のシミュレーション動作と前記命令の期待値生成動作とにより得られるシミュレーション結果と期待値とを、互いに同一の値となるように更新する工程である、ことを特徴とする検証方法。
【請求項３３】
請求項３２記載の検証方法において、
前記抽出工程は、前記期待値生成動作で実行される命令とその命令の実行時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出する前記命令と前記参照データとを、前記命令がその実行時に参照する参照データの制約条件に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記命令のシミュレーション動作と前記命令の期待値生成動作とにより得られるシミュレーション結果と期待値とを、互いに同一の値となるように更新する制御ステップと、を有することを特徴とする検証方法。
【請求項３４】
請求項３２記載の検証方法において、
前記制御ステップは、前記シミュレーション結果を前記期待値と同一の値に更新する、あるいは前記期待値を前記シミュレーション結果と同一の値に更新するステップである、ことを特徴とするプロセッサを含む回路データ部の検証方法。
【請求項３５】
請求項１５記載の検証方法において、
前記抽出工程は、前記期待値生成装置で実行される命令とその命令の実行時に参照される参照データとを抽出するステップを含み、
前記制御工程は、
前記抽出工程で抽出する前記命令と前記参照データとを、前記命令がその実行時に参照するデータ制約条件に照合することで、当該命令がデータ制約条件を有するか否かを解析する命令解析ステップと、
前記命令が前記データ制約条件を有する場合、当該命令の参照データがそのデータ制約条件を満たすか否かを解析する参照データ解析ステップと、
前記命令の参照データがそのデータ制約条件を満たさない場合、前記命令のシミュレーション動作と前記命令の期待値生成動作とにより得られるシミュレーション結果と期待値とを更新する更新命令を生成したうえで、当該更新命令を、前記シミュレーション動作と前記期待値生成動作との後で実行させる制御ステップと、を含むことを特徴とする検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、計算機上での半導体集積回路の検証に関する。
【背景技術】
【０００２】
半導体集積回路の検証方法として、ハードウェア記述言語等のモデル記述言語で記述された回路データを計算機上でシミュレーションすることで、回路データが正常動作するか否かを確認する検証方法がある。この検証方法では回路データを動作させるためにテストパターンを入力する必要がある。また、動作確認のために、実行結果の期待値を用意する必要がある。用意する期待値は、予め準備しておいたり、あるいは回路データの擬似モデルを用意したうえで、真の回路データに与えるテストパターンと同じテストパターンを擬似モデルにも与えることで得られる実行結果を期待値として用いたりする。
【０００３】
このような検証方法における従来技術として、テストパターンを順次実行させた時にエラーが発生した場合、エラーを発生させるテストパターンを登録することで以降のシミュレーションで同じエラーを起こすテストパターンを削除し検証の効率化を図る方法が知られている（特許文献１参照）。
【特許文献１】特許公報第３０５４８０２号
【発明の開示】
【発明が解決しようとする課題】
【０００４】
プロセッサの検証方法といった従来の検証方法では、除算命令を実行する際ににゼロ割り（除数をゼロにして除算処理すること）を行う可能性がある。そのため、特にランダムに生成したテストパターンを検証対象に与えるような検証環境では、除算命令を生成する際に除数がゼロにならないように特別な考慮をしなければならない。
【０００５】
従来の検証方法においてゼロ割りを実行した場合、プロセッサの仕様によっては除算の実行結果が保証されない（無保証になる）ことがある。ここでいう無保証とは、除算命令の実行結果に正しい除算としての演算結果（商や剰余）が格納されないことである。以下、本発明では、このような実行結果を未定義結果と呼ぶ。なお、期待値を出力するプロセッサの擬似モデルにおいても、ゼロ割りが実行されたときの実行結果は、真の回路データと同様、一般に未定義結果となる。
【０００６】
以上のようなプロセッサで実行する命令が実行時に参照するデータによっては実行結果が未定義結果となりうる命令はゼロ割りだけではない。なお、近年のプロセッサの演算器では入力データ値に制限を設けこの制限を違反した場合には演算の実行結果を保証しないことにより演算器の低電力化、低面積化を図っている場合もある。このような場合でも、検証方法において実行結果が未定義となる可能性は決して低くない。
【０００７】
プロセッサの回路データと擬似モデルにおいて、命令の実行結果が未定義（例えばゼロ割り）になった場合、期待値比較は不一致となって擬似エラーが発生する。さらに以降の命令でこの未定義結果を格納した記憶装置を参照する命令が実行された場合、当然その命令の実行結果が異なる。したがって、未定義結果が以降のシミュレーションに伝播し検証が継続できなくなる。特に、命令をランダムに生成するような検証環境では、未定義結果が発生した時点で検証が停止し、その結果として、多量のテストパターンを連続で与えるような長大なシミュレーションを行うことが難しくなり高品質な検証が行えない。
【０００８】
このように、検証方法では未定義結果の対応が課題となっている。なお、未定義結果は、プロセッサに命令を供給する時点では予測は困難である。ゼロ割りを例にすれば、除算命令は、除数として使用するレジスタ番号をオペランド（演算対象項目）に指定するだけの命令形態であって除数の値そのものを即値で指定する命令形態にはなっていない。そのため、ゼロ割りは除算命令実行時のレジスタ値に依存して発生し、除算命令供給時のレジスタ値そのものに依存して発生するものとはならない。
【０００９】
このことから明らかなように、未定義結果はプロセッサに命令を供給する時点で予測することが困難なパラメータであり、除算命令を供給する時点において除数がゼロではないと保証することは困難である。
【００１０】
なお、上述した特許文献１ではエラーが発生するテストパターンを予め登録しているが、上述した理由により、引用文献１であっても未定義結果（ゼロ割り）が発生するテストパターンを予測して、その未定義結果発生パターンを予め登録しておくことは困難であるため、課題を解決することは困難となる。
【課題を解決するための手段】
【００１１】
上記課題を解決するために、本発明では、供給される命令と、その命令が参照する参照データと、参照データのデータ制約条件とを用いて未定義結果の発生を予測する。そして、未定義結果が発生する際にはシミュレーション動作を停止させる。
【００１２】
なお一度停止したシミュレーション動作は実行する命令の実行結果が未定義結果とならないことが予測されるまでその動作を停止のままとする。これによりシミュレーション動作の停止／停止解除にともなう制御を極力少なくしこの制御に伴うシミュレーション全体の速度低下を防ぐ。
【００１３】
本発明の他の構成では、期待値生成動作に命令を与え、その実行結果（期待値）が未定義結果となった場合、期待値生成動作を、命令実行前の状態に戻し、検証対象のシミュレーション動作は命令実行を中止させる。
【００１４】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、参照データのデータ制約条件とを用いて未定義結果の発生を予測し、未定義結果が発生する際には命令を置換させる。
【００１５】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、参照データのデータ制約条件とを用いて未定義結果の発生を予測する。そして、未定義結果が発生すると予測される際には、命令のオペランドにおいて指定する参照データが格納されている記憶装置を、参照データのデータ制約条件を満足するデータが格納されている他の記憶装置に置換させる。
【００１６】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、その参照データのデータ制約条件を登録したデータ制約情報とを用いて、未定義結果の発生を予測する。そして、未定義結果が発生する際には参照データを格納した記憶装置に対しデータ制約条件を満足する値に更新する命令を先に実行させる制御を行う。
【００１７】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、その参照データのデータ制約条件を登録したデータ制約情報とを用いて、未定義結果の発生を予測する。そして、未定義結果が発生する際には参照データを格納した記憶装置を参照データが有するデータ制約条件を満足する値に更新する。
【００１８】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、その参照データのデータ制約条件とを用いて未定義結果の発生を把握する。そして、未定義結果が発生する際には実行結果を格納した記憶装置を適当な値に更新する。
【００１９】
なお、実行結果の更新については、シミュレーション結果と同一の値に期待値を更新しても良いし、期待値と同一の値にシミュレーション結果を更新しても良い。そのため、実行結果を更新する機能は検証対象のシミュレーション装置に設けてもよいし、期待値生成装置に設けてもよい。
【００２０】
本発明のさらに他の構成では、供給される命令と、その命令が参照する参照データと、その参照データのデータ制約条件を登録したデータ制約情報とを用いて未定義結果の発生を把握する。そして、命令生成制約に基づいて命令を生成する命令生成装置に対して、未定義結果を格納した記憶装置を更新する命令を強制発行させる。
【００２１】
なお、命令の強制発行については、未定義結果を格納した記憶装置を更新する命令を強制発行させる命令発行制約を作成し、命令生成装置に追加の命令発行制約として与える。
【００２２】
なお、命令の強制発行については、命令生成装置に対し、未定義結果を格納した記憶装置を更新する命令を強制発行させる制約を新規に作成するように制御する。
【００２３】
なお、命令の強制発行については、未定義結果を参照する命令が実行されるまでに発行すればよく未定義結果が発生した直後でなくても良い。よって未定義結果を格納した記憶装置を更新する命令の発行タイミングにはある程度自由度を持たせることができる。これにより、命令の強制発行による命令の実行順序のランダム性が薄れるのをある程度防ぐことが可能である。
【００２４】
本発明のさらに他の構成では、参照データにデータ制約条件を有する命令の参照データ値を用いて、データ制約条件を有する命令が参照可能な参照データ候補を決定し、それを命令発行制約とする。そして、そのようにして作成する命令発行制約に基づた命令を命令生成装置に生成させる。
【発明の効果】
【００２５】
本発明によれば、
・未定義結果の発生を抑制する、
・未定義結果が発生した以降のシミュレーションを制御することで未定義結果が発生したことによる影響を排除する、
といった作用を発揮することで、擬似エラーによる検証の中断を防ぐことができて高効率な検証が可能となる。
【００２６】
これにより、本発明では、プロセッサの検証のように、命令の実行時に参照する参照データの値がデータ制約条件を満足していないために実行結果が未定義となって期待値比較を行う際に擬似エラーが発生することを防止することができる。
【発明を実施するための最良の形態】
【００２７】
本発明の実施の形態を説明する前に従来の検証装置１００の構成とその検証方法を説明する。
【００２８】
従来の検証装置１００の構成を図１に示す。図１において検証装置１００は、検証装置本体２と、検証装置本体２の内部のデータ情報を抽出するデータ情報抽出装置３と、データ抽出装置３からのデータ情報を受けて未定義結果の影響を抑えるようにシミュレーションの制御を行う実行制御装置４とを備える。
【００２９】
検証装置本体２は、プロセッサを含む回路データ部５と、回路データ部５に含まれるプロセッサによって実行可能な命令を出力する命令供給装置６と、命令供給装置６から供給される命令を回路データ部５のプロセッサでシミュレーションするシミュレーション装置７と、同命令を用いて期待値を生成する期待値生成装置８と、シミュレーション結果と期待値とを比較する比較装置９とを備える。
【００３０】
シミュレーション装置７は、シミュレーションを行うシミュレーション実行部１０と、シミュレーション結果と命令実行時に参照する参照データとを格納する第１記憶装置１１とから構成される。期待値生成装置８は、命令供給装置６から供給される命令を実行して期待値を生成する期待値生成部１２と、期待値生成部１２が命令実行時に参照する参照データを格納するとともに、期待値生成部１２が生成する期待値を格納する第２記憶装置１３とを備える。
【００３１】
従来の検証装置１００を用いた検証方法を、図２を参照して説明する。図２は、従来の検証方法を示すフローチャートである。
【００３２】
従来の検証方法は、命令供給プロセス（Ｓ２０１）と、シミュレーションプロセス（Ｓ２０２,Ｓ２０３）と、期待値生成プロセス（Ｓ２０４,Ｓ２０５）と、比較プロセス（Ｓ２０６）とを含む。命令供給プロセスＳ２０１は、命令供給装置６がシミュレーション装置７と期待値生成装置８とに命令を供給するプロセスである。シミュレーションプロセス（Ｓ２０２,Ｓ２０３）は、供給された命令を用いてシミュレーション装置７がシミュレーションを実行したうえでそのシミュレーション結果を第１記憶装置１１に格納するプロセスである。期待値生成プロセス（Ｓ２０４,Ｓ２０５）は、供給された命令を用いて期待値生成装置８が期待値を求めたうえで求めた期待値を第２記憶装置１３に格納するプロセスである。比較プロセスＳ２０６は、比較装置９がシミュレーション結果と期待値とを比較するプロセスである。
【００３３】
シミュレーションプロセスと期待値生成プロセスとは次の点の異なる工程である。すなわち、シミュレーションプロセスとは、ハードウェア記述言語等のモデル記述言語で記述された回路データ部５をシミュレーション装置７でシミュレーションすることで、シミュレーション結果を生成するプロセスである。期待値生成プロセスとは、回路データ部５の擬似モデルを用意したうえで、回路データ部５に与えるテストパターンと同じテストパターンを擬似モデルで実行することで、その実行結果（期待値）を生成するプロセスである。
【００３４】
比較プロセスＳ２０６において比較装置９は、比較結果が一致しない場合、シミュレーションを停止させて、ユーザに結果の不一致を通知する。反対に、比較結果が一致する場合は、新たな命令をシミュレーション装置７と期待値生成装置８とに供給させる指令を命令供給装置６に出力する。ここで命令供給プロセスＳ２０１において命令供給装置６がシミュレーション装置７と期待値生成装置８とに供給する命令は、作業者自身が作成して命令供給装置６に入力した命令データでもよいし、命令供給装置６内においてランダムに生成された命令データであってもいい。
【００３５】
以上の検証方法では、シミュレーション結果と期待値との比較で不一致が起こらない限りシミュレーションは継続される。しかし、先に説明した命令の実行結果が未定義結果となった場合、比較プロセスにおいて比較結果が不一致になる。そうすると、比較プロセスにおいて擬似エラーと判断されてシミュレーション操作が停止される。さらに以降のシミュレーションでこの未定義結果を参照する命令が実行された場合、参照データが異なっているのでお互いの実行結果も当然異なったものとなり、その結果、比較プロセスでの比較結果は不一致と判定される。そのため、未定義結果が発生した以降、シミュレーションは継続されなくなる。
【００３６】
このように、従来の検証方法では、真のエラーによるシミュレーション停止以外にも未定義結果による擬似エラーが発生してもシミュレーションが停止してしまう。特に命令供給プロセスで命令をランダムに生成するような検証方法では、未定義結果が頻繁に発生することによりシミュレーションの連続実行が妨げられる恐れがある。
【００３７】
（第１の実施の形態）
本発明の第１の実施の形態の検証装置１Ａの構成を図３に示す。検証装置１Ａの構成は、基本的に従来の検証装置１００と同様であり、同一ないし同様の部分には同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＡを付して従来の検証装置１００と区別する。
【００３８】
以下、検証装置１Ａにおいて特徴となる構成について説明する。本実施形態の検証装置１Ａは、検証装置本体２Ａとデータ情報抽出装置３Ａと実行制御装置４Ａとを備える。検証装置本体２Ａは、基本的には、従来の検証装置１００における検証装置２と同様の構成を備える。第２記憶装置１３は、期待値生成部１２が命令実行時に参照する参照データと、期待値生成部１２が命令を実行した結果である期待値とを格納する。一般的なプロセッサにおいては、第２記憶装置１３は汎用レジスタから構成される。
【００３９】
データ情報抽出装置３Ａは、第２記憶装置１３に格納されている参照データと、命令供給装置６が出力する命令とを抽出して、実行制御装置４Ａに供給する。
【００４０】
実行制御装置４Ａは、データ制約情報格納部２０と、命令解析装置２１と、参照データ解析装置２２と、制御装置２３Ａとを備える。データ制約情報格納部２０は命令の制約条件が登録される。命令の制約条件とは、シミュレーション実行部１０と期待値生成部１２とによって命令が実行される際に参照される参照データの制約条件である。命令解析装置２１は、データ制約情報格納部２０に格納されている制約情報に基づいて、命令（データ情報抽出装置３Ａが抽出する）の詳細を解析する。参照データ解析装置２２は、データ制約情報格納部２０に格納されているデータ制約情報と命令解析装置２１による命令の解析結果とに基づいて、参照データ（データ情報抽出装置３Ａが抽出する）の詳細を解析する。制御装置２３Ａは、参照データ解析装置２２による解析結果に基づいてシミュレーション装置７と期待値生成装置８とを制御する。
【００４１】
データ制約情報格納部２０に格納されるデータ制約情報を図４に示す。データ制約情報格納部２０が格納するデータ制約情報は、命令とその制約条件とを含む。ここでいう命令とは、回路データ部５に含まれるプロセッサによって実行される命令であって、さらには命令実行時に参照する参照データに制約条件のある命令である。データ制約情報格納部２０は、このような制約条件を有する命令と、その制約条件とが選択的に格納される。図４では、各命令はオペコードにより分類されている。
【００４２】
ＤＩＶ命令（除算命令）の場合、オペランドの第１要素に被除数を、第２要素に除数を格納した汎用レジスタのレジスタ番号を指定しており、その参照データの制約条件が図４に示される。この場合、第２要素である除数はゼロ以外の値であることが制約条件として登録される。他の命令（ＭＵＬ,ＡＤＤＸ２,ＳＵＢＸ２,ＭＵＬＸ２,…）についても命令のオペランドで指定する参照データの制約条件が登録される。
【００４３】
以下、検証装置１Ａを用いた検証方法を図５,図６のフローチャートを参照して説明する。まず、命令供給装置６がシミュレーション実行部１０と期待値生成部１２とに命令を供給する（Ｓ５０１）。このとき、命令供給装置６は供給する命令をデータ情報抽出装置３Ａにも出力する。データ情報抽出装置３Ａは、供給される命令中に含まれる中間データを抽出する（Ｓ５０２）。検証装置１Ａにおいて中間データとは、具体的には命令そのものと、その命令が実行する際に参照する参照データとのことである。
【００４４】
データ情報抽出装置３Ａは抽出した中間データを実行制御装置４Ａに出力する。実行制御装置４Ａは入力された中間データを用いて次の処理を行う。まず、命令解析装置２１が中間データの解析を行う。解析結果に基づいて制御装置２３Ａは、検証装置本体２Ａの制御（動作続行／動作一時停止の切換制御）を行う（Ｓ５０３）。
【００４５】
ステップＳ５０３の制御結果が命令の実行動作の一時停止を示す場合、検証装置本体２Ａはその制御に従って検証動作を一時停止する。一方、ステップＳ５０３の制御結果が動作続行である場合、検証装置本体２Ａは従来のシミュレーション処理を実行する。具体的には、検証装置本体２Ａは、命令供給装置６から供給される命令をシミュレーション装置７と期待値生成装置８とで実行したうえで（Ｓ５０４,Ｓ５０６）、その実行結果（シミュレーション結果と期待値）を、第１記憶装置１１と第２記憶装置１３とに格納する（Ｓ５０５,Ｓ５０７）。第１記憶装置１１と第２記憶装置１３とに格納された実行結果は、比較装置９で互いに一致するか否かが比較される（Ｓ５０８）。これにより一連のシミュレーション動作が終了する。
【００４６】
次に、検証装置１Ａにおいて特徴となる中間データの解析動作とその解析結果に基づく制御動作を図６のフローチャートを参照して説明する。まず、命令解析装置２１において、データ情報抽出装置３Ａから受け取る中間データに制約条件があるか否かを判断する（Ｓ６０１）。制約条件の有無の判断は、具体的には、中間データが、データ制約情報格納部２０に格納（登録）されている制約付き命令に該当するか否かの判断により実施される。
【００４７】
Ｓ６０１の判断結果が、中間データは登録命令（制約付き命令）に該当しないことを示す場合、命令解析装置２１はそのことを制御装置２３Ａに通知する。否該当通知を受けた制御装置２３Ａは、その命令は未定義結果を起こす可能性が無いと判断する。そのうえで、制御装置２３Ａは、まず、シミュレーション装置７と期待値生成装置８との動作が一時停止中であるか否かを判断する（Ｓ６０２）。Ｓ６０２の判断結果が一時停止中でないことを示す場合、制御装置２３Ａは、シミュレーション装置７と期待値生成装置８との制御を行わない。ここでいう制御とは、具体的には、シミュレーション装置７と期待値生成装置８とを一時停止させることである。一方、Ｓ６０２の判断結果が一時停止中であることを示す場合、制御装置２３Ａは、シミュレーション装置７と期待値生成装置８との動作を再開させる（Ｓ６０３）。
【００４８】
一方、Ｓ６０１の判断結果が、中間データは登録命令（制約付き命令）に該当することを示す場合、命令解析装置２１は、そのことを参照データ解析装置２２に通知する。該当通知を受けた参照データ解析装置２２は以下に示す解析を行う。まず、その中間データ中に含まれる参照データから、その命令のオペランドで指定しているレジスタ番号のレジスタ値を抽出する。さらに、抽出したレジスタ値がデータ制約条件（データ制約情報格納部２０に格納されたデータ制約情報に登録されている）を満足しているか否かを判断し、その判断結果を制御装置２３Ａに通知する（Ｓ６０４）。
【００４９】
Ｓ６０４の処理によって通知される判断結果がデータ制約条件を満足しており無違反を示す場合、制御装置２３Ａは、その命令は未定義結果を起こす可能性が無いと判断したうえで、上述したＳ６０２,Ｓ６０３の処理を実施する。つまり、この処理では、シミュレーション装置７と期待値生成装置８との制御（一時停止）を実施しない。
【００５０】
一方、Ｓ６０４の処理によって通知される判断結果がデータ制約条件を満足しておらず違反を示す場合、制御装置２３Ａは、その命令は未定義結果を起こすと判断してシミュレーション装置７と期待値生成装置８との制御（一時停止）を実施する（Ｓ６０５）。
【００５１】
上述したＳ６０２,Ｓ６０３,Ｓ６０５の処理を実施することにより次のような効果が得られる。未定義結果を起こすと判断する命令が連続して供給される間において制御装置２３Ａは、シミュレーション装置７と期待値生成装置８とを一時停止状態のままとする。そして、未定義結果を起こす可能性が無いと判断する命令が供給された時点でその一時停止制御を解除（動作再開）する。このように制御装置２３Ａは、未定義結果になると判断される命令が連続して供給される期間においてシミュレーション装置７と期待値生成装置８とを一時停止状態のままとすることで、これら装置７,８の停止および停止解除の制御を行う時間を極力少なくして全体のシミュレーション速度の低下を防ぐ。
【００５２】
以上説明したように、本実施形態の検証装置１Ａは、命令の実行結果が未定義結果となる命令が実行される直前に、シミュレーション装置７と期待値生成装置８とを停止させることで、当該命令の実行を阻止する。これにより、未定儀結果となる命令が実行されることによって生じる不具合を防ぐことができる。
【００５３】
（第２の実施の形態）
図７は本発明の第２の実施の形態の検証装置１Ｂの構成を示す。期待値生成装置１Ｂは、基本的には、第１の実施の形態と同様の構成を備えており、同一ないし同様の部分には第１の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＢを付して第１の実施の形態と区別する。
【００５４】
検証装置１Ｂは、前状態戻り装置３０と実行待機装置３１と未定義結果判定装置３２とを備えることに特徴がある。前状態戻り装置３０は、期待値生成装置８Ｂを、直前に実行した命令の実行前状態に遷移させる装置である。このような前状態戻り装置３０の操作は、命令を実行する直前において、期待値生成装置８Ｂ内の第２の記憶装置１３の記録内容を一旦保持させたうえで、命令の実行後において、保持させておいたデータを第２の記憶装置１３の記録内容に戻すことにより可能である。
【００５５】
実行待機装置３１はシミュレーション装置７Ｂに設けられる。実行待機装置３１は、実行制御装置４Ｂからの、待機解除通知があるまでシミュレーション装置７Ｂにによる命令の実行を停止させる。第２の実施の形態では、期待値生成装置８Ｂによって先行的に命令を実行させたうえでその実行結果をデータ情報抽出装置３Ｂによって抽出させる。
【００５６】
未定義結果判定装置３２は、データ情報抽出装置３Ｂから得られる抽出情報から実行結果が未定義となったか否かを判定する。ここで、期待値生成部１２が実行の未定義結果の発生を通知するフラグを作成する場合には、未定義結果判定装置３２は、そのフラグの検出によって前記未定義を判定することができる。また、第１の実施の形態の検証装置１Ａと同様に、命令とその命令が実行される際に参照されるデータ情報とを解析することで、その命令の実行結果が未定義となったことを判定することもできる。
【００５７】
制御装置２３Ｂは、未定義結果判定装置３２の判定結果に基づいて次の制御を実施する。期待値生成装置８Ｂで実行した命令の実行結果が未定義の場合、制御装置２３Ｂは、前状態戻り装置３０を動作させて期待値生成装置８Ｂを命令実行前の状態に戻させる。ここで、期待値生成装置８Ｂによって先行的に命令を実行させているために、シミュレーション装置７Ｂは、命令実行結果の未定義判定時点において未だ命令を実行していない。このタイミングでその命令の実行結果が未定義であることが判明した制御装置２３Ｂは、未定義として判定した命令を、シミュレーション装置７Ｂで実行させない。
【００５８】
検証装置１Ｂでは、前もって実施した命令の実行結果の未定義判定に基づいて、期待値生成装置８Ｂを命令実行前の状態に戻し、さらにシミュレーション装置７Ｂでの命令実行を停止させる。つまり、検証装置１Ｂは、期待値生成装置８Ｂを先行的に実行させて実行結果の未定義を判定し、その判定結果に基づいて期待値生成装置８Ｂのリセットと、シミュレーション装置７Ｂの命令停止とを行う。これにより、検証装置１Ｂは、参照データがデータ制約条件を違反するために命令の実行結果が未定義結果となる命令の実行を阻止する。
【００５９】
以下、検証装置１Ｂを用いた検証方法を図８,図９のフローチャートを参照して説明する。図８は、検証装置１Ｂ全体の動作を示すフローチャートである。図９は、未定義結果判定装置３２の動作と制御装置２３Ｂの動作とを抜き出して示すフローチャートである。
【００６０】
まず、命令供給装置６がシミュレーション実行部１０と期待値生成部１２とに命令を供給する（Ｓ８０１）。
【００６１】
期待値生成装置８Ｂは、期待値生成部１２で命令を実行したうえでその実行結果である期待値を第２記憶装置１３に記憶させる（Ｓ８０２,Ｓ８０３）。この時点では、シミュレーション装置７Ｂは、命令を実行せずに待機している。
【００６２】
期待値生成部１２の命令実行実行結果である期待値は、データ情報抽出装置３Ｂによって抽出されて未定義結果判定装置３２に供給される（Ｓ８０４）。
【００６３】
未定義結果判定装置３２は、期待値生成部１２から得られる情報を解析してその期待値が未定義であるか否かを判定し、さらに、制御装置２３Ｂは、その解析結果に基づいてシミュレーション装置７と期待値生成装置８とを制御する（Ｓ８０５）。
【００６４】
ステップＳ８０５の処理の詳細を図９のフローチャートを参照して説明する。まず、未定義結果判定装置３２は、期待値生成部１２から得られる情報を解析してその期待値が未定義であるか否かを判定する（Ｓ９０１）。判定結果は制御装置２３Ｂに供給される。
【００６５】
制御装置２３Ｂは、未定義結果判定装置３２の判定結果に基づいて次の制御を実施する。すなわち、制御装置２３Ｂは、命令の実行結果（期待値）の判定結果に基づいてシミュレーション装置７Ｂの制御信号をシミュレーション装置７Ｂに送信する。ここでの制御信号とは次のものである。命令の実行結果（期待値）が未定義を含まない場合には、制御信号はシミュレーション装置７Ｂでの命令実行を許可する信号となり（Ｓ９０２）、命令の実行結果（期待値）が未定義を含む場合には、制御信号は、期待値生成装置８Ｂの状態を命令実行前に戻すとともに、シミュレーション装置７Ｂでの命令実行を禁止する（許可しない）信号となる（Ｓ９０４）。
【００６６】
以下、図８のフローチャートに戻って、上記制御信号を受けたシミュレーション装置７Ｂと期待値生成装置８Ｂの動作を説明する。期待値生成装置８Ｂは、シミュレーション装置７Ｂに先行して命令を実行しており、この時点（制御装置２３Ｂから制御信号を受信する時点）においてシミュレーション装置７Ｂは未だ命令を実行していない。制御信号を受信した実行待機装置３１は、受信した制御信号の内容を判断したうえで（Ｓ８０６）、その判断結果に基づいて次のようにシミュレーション装置７Ｂを制御する。
【００６７】
受信した制御信号が命令実行の禁止（不許可）を示す場合、実行待機装置３１は、その指示に従って、シミュレーション実行部１０による命令実行を開始させることなく停止状態のままとし、さらにステップＳ８０１に戻って次の命令が命令供給装置６から供給されるのを待機する。
【００６８】
一方、受信した制御信号が命令実行の許可を示す場合、実行待機装置３１は、検証装置本体２Ｂでの従来のシミュレーション処理を開始させる（Ｓ８０７）。そして、シミュレーション実行部１０での実行結果（シミュレーション結果）を、第１記憶装置１１に格納する（Ｓ８０８）。第１記憶装置１１と第２記憶装置１３とに格納された実行結果は比較装置９で互いに一致するか否かが比較される（Ｓ８０９）。これにより一連のシミュレーション動作が終了する。
【００６９】
このように、検証装置１Ｂは、先行的に命令を実行させて得られる期待値の未定義判定結果に基づいて期待値生成装置８Ｂのリセットと、シミュレーション装置７Ｂの命令停止とを行う。具体的にいえば、検証装置１Ｂは、前もって期待値生成部１２で実施した命令の実行結果が未定義であるか否かの判定結果に基づいて、期待値生成装置８Ｂを命令実行前の状態に戻す制御と、シミュレーション装置７Ｂでの命令実行を停止させる制御とを実施する。そのため、検証装置１Ｂでは、命令の実行結果が未定義結果となる命令の実行が未然に阻止される。これにより、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【００７０】
（第３の実施の形態）
本発明の第３の実施の形態の検証装置１Ｃの構成を図１０に示す。検証装置１Ｃの構成は、基本的に第１の実施の形態の検証装置１Ａと同様であり、同一ないし同様の部分には、第１の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＣを付して検証装置１Ａと区別する。具体的には、検証装置１Ｃは制御装置２３Ｃの制御方法に特徴があって、この制御方法が、検証装置１Ａの制御装置２３Ａと異なる。
【００７１】
検証装置１Ｃを用いた検証方法のフローチャートを図１１に示す。検証装置１全体としての制御は図５のフローチャートに示す検証装置１Ａの全体動作と同一である。但し、検証装置１Ｃは、ステップＳ５０３における中間データの解析動作とその解析結果に基づく制御動作とが、若干検証装置１Ｃと異なる。
【００７２】
検証装置１Ｃにおいて特徴となる中間データの解析動作と、その解析結果に基づく制御動作とが図１１のフローチャートに示されている。データ情報抽出装置３Ａは、抽出した中間データを命令解析装置２１と参照データ解析装置に供給する。
【００７３】
命令解析装置２１は、データ情報抽出装置３から受け取る中間データに制約条件があるか否かを判断する（Ｓ１１０１）。制約条件の有無の判断は、具体的には、中間データが、データ制約情報格納部２０に格納（登録）されている命令に該当するか否かの判断により実施される。
【００７４】
ステップＳ１１０１の判断結果が、中間データは登録命令に該当しないことを示す場合、命令解析装置２１はそのことを制御装置２３Ｃに通知する。通知を受けた制御装置２３Ｃは、その命令は未定義結果を起こす可能性が無いと判断する。以上の判断を下した制御装置２３Ｃは、シミュレーション装置７と期待値生成装置８との制御を行わない。したがって、シミュレーション装置７と期待値生成装置８とは、その命令を実行する。
【００７５】
一方、ステップＳ１１０１の判断結果が、中間データは登録命令（制約付き命令）に該当することを示す場合、命令解析装置２１は、そのことを参照データ解析装置２２に通知する。その通知を受けた参照データ解析装置２２は以下に示す解析を行う。参照データ解析装置２２は、データ情報抽出装置３Ａから供給される中間データ中に含まれる参照データから、その命令のオペランドで指定しているレジスタ番号のレジスタ値を抽出する。さらに、抽出したレジスタ値がデータ制約条件（データ制約情報格納部２０に格納されたデータ制約情報に登録されている）を満足しているか否かを判断し、その判断結果を制御装置２３Ｃに通知する（Ｓ１１０２）。
【００７６】
ステップＳ１１０２の処理によって通知される判断結果がデータ制約条件を満足しており無違反を示す場合、制御装置２３Ｃは、その命令は未定義結果を起こす可能性が無いと判断してシミュレーション装置７と期待値生成装置８との制御を行わない。したがって、シミュレーション装置７と期待値生成装置８とはその命令を実行する。
【００７７】
一方、ステップＳ１１０２の処理によって通知される判断結果がデータ制約条件を満足しておらず違反を示す場合、制御装置２３Ｃは、その命令は未定義結果を起こすと判断する。そのような判断を下した制御装置２３Ｃは、その命令を、データ制約条件を有していない他の命令に置換する制御を行う（Ｓ１１０３）。データ制約条件を有していない他の命令とは、例えば、ＮＯＰ（Ｎｏ  Ｏｐｅｒａｔｉｏｎ）命令であり、未定義となる命令を、このような命令に置換する。置換された他の命令は、制御装置２３２３Ｃから命令供給装置６を介してシミュレーション装置７と期待値生成装置８とに供給される。
【００７８】
シミュレーション装置７と期待値生成装置８とは、置換された命令を実行する。これにより、データ制約条件もなくシミュレーションに影響を与えない命令がシミュレーション装置７と期待値生成装置８とで実行される。そのため、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【００７９】
第１の実施の形態の検証装置１Ａでは、実行する命令が未定義結果となる場合、シミュレーション装置７と期待値生成装置８とを停止させていた。これに対して、本実施の形態の検証装置１Ｃでは、未定義結果となる命令を、データ制約条件を有していない他の命令に置換する制御を行う。未定義となる命令を、このような命令に置換することで、データ制約条件がなくシミュレーションに影響を与えない状態で命令を実行することができる。これにより、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【００８０】
なお、第３の実施の形態における検証装置１Ｃは、命令の実行結果が未定義となる場合に命令を置換する制御を実施する以外は第１の実施の形態の検証装置１Ａと同じ制御を実施する。
【００８１】
（第４の実施の形態）
本発明の第４の実施の形態の検証装置１Ｄの構成を図１２に示す。検証装置１Ｄの構成は、基本的に第３の実施の形態の検証装置１Ｃと同様であり、同一ないし同様の部分には第３の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＤを付して検証装置１Ｃと区別する。具体的には、検証装置１Ｄは制御装置２３Ｄの構成および制御装置２３Ｄによる制御方法に特徴があって、この構成および制御方法が、検証装置１Ｃの制御装置２３Ｃと異なる。
【００８２】
検証装置１Ｄ全体としての制御方法（検証方法）は図５のフローチャートに示す第３の実施の形態の検証装置１Ｃの制御方法（検証方法）と同一である。そのため、検証装置１Ｄの制御方法（検証方法）全体の説明は省略する。
【００８３】
本実施形態の検証装置１Ｄの制御装置２３Ｄは、命令の実行結果が未定義となると判断する場合に、命令実行時に参照する参照データを他の参照データに置換する処理を行うことに特徴がある。検証装置１Ｄの制御処理における要部の処理動作を図１３,図１４に示す。この処理動作は、第３の実施の形態の検証装置１Ｃにおける要部の処理動作と基本的に類似している。そのため、同一のステップには同一の符号を付している。しかしながら、次の処理において、検証装置１Ｆは検証装置１Ｃと異なる。
【００８４】
第３の実施の形態の検証装置１Ｃでは、図１１の処理Ｓ１１０３に示されるように、実行結果が未定義となる命令を、データ制約条件を有していない他の命令に置換していた。本実施形態の検証装置１Ｄでは、このような命令置換処理を図１３に示すように、参照データ置換処理Ｓ１１０３Ｄに入れ替えている。
【００８５】
検証装置１Ｄでは、実行結果が未定義結果となる命令が実行時に参照する参照データを、参照データになることが可能な他のデータに置換している。具体的には、その命令の実行時に参照するデータのレジスタ番号を、命令のオペランドで指定している参照データの場所（汎用レジスタのレジスタ番号）を取り得ることが可能な他のレジスタ番号（第４の実施の形態ではこれを参照データ候補と呼ぶ）に変更させている。この置換処理が参照データ置換処理Ｓ１１０３Ｄである。
【００８６】
このような制御を実施するために検証装置１Ｄの制御装置２３Ｄは、参照データ候補を探索する参照データ候補探索装置４０と、探索した参照データ候補がデータ制約条件を満足しているか否かを解析する参照データ候補解析装置４１と、参照データ候補がデータ制約条件を満足している場合、参照データを参照データ候補に置換する参照データ置換装置４２とを備える。
【００８７】
制御装置２３Ｄにおける参照データ置換処理ステップＳ１１０３の詳細を、図１４のフローチャートを参照して説明する。
【００８８】
プロセッサで実行される命令のオペランドでは、一般に、命令実行時に参照される参照データを格納しているレジスタ番号が指定される。そこで、参照データ解析装置２２によって命令の実行結果が未定義になると判断された場合、制御装置２３Ｄでは、まず、実行結果が未定義となる命令の参照データのレジスタ番号から置換可能な他のレジスタ番号が存在するか否かが探索される（Ｓ１４０１）。この探索操作は参照データ候補探索装置４０が実施する。
【００８９】
Ｓ１４０１で置換可能なレジスタ番号がないと判断する場合は、その命令は削除される（Ｓ１４０２）。命令の削除操作は参照データ置換装置４２が実施する。
【００９０】
一方、Ｓ１４０１で置換可能なレジスタ番号があると判断する場合、置換候補のレジスタ番号に位置する参照データ候補がデータ制約条件を満たしているか否かを判断する（Ｓ１４０３）。この判断は、参照データ候補解析装置４１が実施する。Ｓ１４０３で、参照データ候補がデータ制約条件を満たしていると判断する場合、実行結果が未定義となる参照データを参照データ候補に変更する。つまり、命令で用いる参照データを、実行結果が未定義となると判断する候補から、未定義とならないと判断する候補に置換する（Ｓ１４０４）。この置換操作は、参照データ置換装置４２が実施する。
【００９１】
Ｓ１４０３で、参照データ候補がデータ制約条件を満たしていないと判断する場合、Ｓ１４０１に戻って、さらに他の参照データ候補があるか否かを判断する。このようなＳ１４０１〜Ｓ１４０４の操作を実施することで、参照データを、データ制約条件を満たしているデータに置換する。
【００９２】
通常、プロセッサには複数の汎用レジスタが用意されており命令のオペランドで指定しているレジスタ番号は置換可能である。このようなプロセッサの特徴を利用して、検証装置１Ｄでは、参照データを、データ制約条件を満たしているデータに置換している。なお、置換できない場合には本発明の他の実施形態による対策、例えば第３の実施の形態による命令の置換を行えば良い。
【００９３】
以上、検証装置１Ｄでは、命令の実行結果が未定義となる命令の参照データを他のデータに置換することで、命令の実行結果が未定義結果となる命令の実行が阻止される。これにより、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【００９４】
（第５の実施の形態）
本発明の第５の実施の形態の検証装置１Ｅの構成を図１５に示す。検証装置１Ｅの構成は、基本的に第３の実施の形態の検証装置１Ｃと同様であり、同一ないし同様の部分には、第３の実施の形態と検証装置１Ｃと同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＥを付して検証装置１Ｃと区別する。
【００９５】
検証装置１Ｅは制御装置２３Ｅの構成および制御装置２３Ｅによる制御方法に特徴がある。制御装置２３Ｅは、命令生成装置４３と命令配置装置４４とを備えていることとこれらの装置４３,４４を用いた制御方法とが、検証装置１Ｃの制御装置２３Ｃと異なる。
【００９６】
検証装置１Ｅ全体としての制御方法（検証方法）は図５のフローチャートに示す第３の実施の形態の検証装置１Ｃの制御方法（検証方法）と同一である。そのため、検証装置１Ｅの制御方法（検証方法）全体の説明は省略する。
【００９７】
本実施形態の検証装置１Ｅの制御装置２３Ｅは、命令の実行結果が未定義となると判断する場合に、参照データを変更する命令を新たに生成したうえで生成した参照データ変更命令を未定義となる命令より前に実行する位置に配置する命令生成配置処理を実施することに特徴がある。検証装置１Ｅを用いた制御方法（検証方法）の要部を図１６に示す。検証装置１Ｅ全体としての制御は図５のフローチャートに示す第３の実施の形態の検証装置１Ｄの制御方法（検証方法）と基本的に類似している。そのため、同一のステップには同一の符号を付している。しかしながら、次の処理において、検証装置１Ｅは検証装置１Ｃと異なる。
【００９８】
制御装置２３Ｅでは、命令の実行結果が未定義となると判断する場合に、参照データを変更する命令を新たに生成したうえで生成した参照データ変更命令を未定義となる命令より前に実行する位置に配置する処理Ｓ１１０３Ｈに入れ替えている。以下、検証装置１Ｅで実施する命令生成配置処理の詳細を、図１７のフローチャートを参照して説明する。
【００９９】
まず、命令のオペランドで指定している参照データの場所（汎用レジスタのレジスタ番号）をその命令が持つデータ制約条件の範囲内の値に更新する命令を生成する（Ｓ１７０１）。この操作は、命令生成装置４３が実施する。そのうえで、その更新命令を、未定義結果となる命令より先に配置する（Ｓ１７０２）。この操作は、命令配置装置４４が実施する。このようにして変更された命令が制御装置２３Ｅから命令供給装置６を介して期待値生成装置８に供給されて、期待値生成装置８で実行される。
【０１００】
これにより、データ制約条件を満足しないデータを参照する命令が、データ制約条件を満足するデータを参照する命令に変更された状態で期待値生成装置８とシミュレーション装置７とで実行されることとなり、その結果として、未定義結果の発生が防止される。
【０１０１】
命令生成装置４３で生成される参照データ更新命令は、具体的には次のような構成として生成される。例えば、データ制約条件を満足する更新データをレジスタに格納するメモリアクセス命令が参照データ更新命令として生成される。この場合、命令毎にデータ制約条件を満足する更新データの値をあらかじめデータメモリ等に格納しておく必要がある。また、データ制約条件を満足する値を即値とするオペランドで指定するＭＯＶ命令が参照データ更新命令として生成される。
【０１０２】
これにより検証装置１Ｅでは、命令の実行結果が未定義結果となる命令の参照データを未定義とならないデータに更新する命令を生成したうえで、その参照データ更新命令を、未定義結果となる命令よりも先に実行させる。これにより、未定義結果の発生を防ぐことが可能となり、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【０１０３】
（第６の実施の形態）
本発明の第６の実施の形態の検証装置１Ｆの構成を図１８に示す。検証装置１Ｆの構成は、基本的に第３の実施の形態の検証装置１Ｃと同様であり、同一ないし同様の部分には第３の実施の形態の検証装置１Ｃと同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＦを付して検証装置１Ｃと区別する。具体的には、検証装置１Ｆは制御装置２３Ｆの構成および制御装置２３Ｆによる制御方法に特徴があって、この構成および制御方法が、検証装置１Ｃの制御装置２３Ｃと異なる。
【０１０４】
検証装置１Ｆ全体としての制御方法（検証方法）は図５のフローチャートに示す第３の実施の形態の検証装置１Ｃの制御方法（検証方法）と同一である。そのため、検証装置１Ｆの制御方法（検証方法）全体の説明は省略する。
【０１０５】
本実施形態の検証装置１Ｆの制御装置２３Ｆは、命令の実行結果が未定義となると判断する場合に、命令実行時に参照する参照データの更新処理を実施することに特徴がある。検証装置１Ｆの制御処理における要部の処理動作を図１９に示す。この処理動作は、第３の実施の形態の検証装置１Ｃにおける要部の処理動作と基本的に類似している。そのため、同一のステップには同一の符号を付している。しかしながら、次の処理において、検証装置１Ｆは検証装置１Ｃと異なる。
【０１０６】
第３の実施の形態の検証装置１Ｃでは、実行結果が未定義となる命令を、図１１のステップＳ１１０３に示されるように、データ制約条件を有していない他の命令に置換していた。本実施形態の検証装置１Ｆでは、このような命令置換処理を次のような参照データ更新処理Ｓ１１０３Ｆに入れ替えている。
【０１０７】
参照データ更新処理Ｓ１１０３Ｆにおいては、参照データを格納している第１，第２の記憶装置１１，１３を強制的にその命令が持つデータ制約条件の範囲内の値に更新させている。そのため、参照するデータがデータ制約条件を満足していない命令であったとしても、参照データがデータ制約条件を満足するデータに更新されたうえで、その更新参照データが命令によって実行されることになる。これにより、未定義結果の発生を防ぐことができる。検証装置１Ｆにおいて命令の参照データを強制的に更新するために、第１記憶装置１１（シミュレーション装置７側）と第２記憶装置１３（期待値生成装置８側）とは、記録内容（参照データ）を強制的に更新させる機能を有するものとする。
【０１０８】
以上説明したように、検証装置１Ｆでは、命令の実行結果が未定義となる命令の参照データを強制的に命令が持つデータ制約条件の範囲内の値に更新することで、命令の実行結果が未定義結果となる命令の実行が阻止される。これにより、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【０１０９】
（第７の実施の形態）
本発明の第７の実施の形態の検証装置１Ｇの構成を図２０に示す。検証装置１Ｇの構成は、基本的に第３の実施の形態の検証装置１Ｃと同様であり、同一ないし同様の部分には第３の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＧを付して検証装置１Ｃと区別する。具体的には、検証装置１Ｇは制御装置２３Ｇの構成および制御装置２３Ｇによる制御方法に特徴があり、この構成および制御方法が、検証装置１Ｃの制御装置２３Ｃと異なる。
【０１１０】
検証装置１Ｆを用いた制御方法（検証方法）を、図２１，図２２のフローチャートに示す。これらのフローチャートは、第３の実施の形態の検証装置１Ｃの制御方法（検証方法）である図５と図１１のフローチャートと基本的には類似している。そのため、同一のステップには、同一の符号を付している。しかしながら、本実施形態の検証装置１Ｇの制御装置２３Ｇは、命令の実行結果である期待値が未定義となるとシミュレーション実行前に判断（推定）する場合に、未定義結果となる命令を、データ制約条件を有していない他の命令に置換する処理（図５におけるステップＳ５０３および図１１におけるステップＳ１１０３）は実施しない。その代わり、実際に命令を実行することで得られる実行結果（期待値やシミュレーション結果）を未定義とならない値に強制的に変更する処理（図１８におけるステップＳ５０３Ｇおよび図１９におけるステップＳ１１０３Ｇ）を実施する。但し、ステップＳ５０３Ｇ，Ｓ１１０３Ｇは、命令の抽出テップＳ５０２の直後に実施される処理ではなく、シミュレーション装置７や期待値生成装置８で命令を実施した後に行われる。
【０１１１】
具体的には、第１，第２の記憶装置１１，１３に格納している命令の実行結果（期待値やシミュレーション結果）を、強制的にその命令において定義可能な値に更新させる。これにより、参照するデータがデータ制約条件を満足していない命令であったとしても、その命令の実行結果が定義可能データ（未定義とならないデータ）に更新されることになる。これにより、未定義結果の発生を防ぐことができる。
【０１１２】
以上説明したように、検証装置１Ｇでは、未定義となった命令の実行結果を強制的に未定義とならないデータに更新することで、命令の実行結果が未定義結果となる命令の実行が阻止される。これにより、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【０１１３】
但し、上記強制更新動作を実施するに際しては、シミュレーション結果と期待値とを同じ値に更新する必要がある。そのためには、両者を適当な同一値に更新するか、もしくは片方を参照してそれと同じ値にもう一方を更新する必要がある。
【０１１４】
このような強制更新機能を発揮させるために検証装置１Ｇでは、第１記憶装置１１（シミュレーション装置７側）と第２記憶装置１３（期待値生成装置８側）とは、記録内容（参照データ）を強制的に更新させる機能を有するものとされる。但し、シミュレーション結果を参照してそれと同一の値へ期待値を更新させる場合には、シミュレーション装置７あるいは期待値生成装置８の何れか片方に上記強制更新機能があれば良い。
【０１１５】
本実施形態の検証装置１Ｇでは、命令解析装置２１と参照データ解析装置２２とを用いて未定義結果の発生を判定したが、第２の実施の形態における未定義結果判定装置３２を用いて未定義結果の発生を判定することもできる。つまり、期待値生成装置８における命令の実行結果情報から未定義結果の発生を判定し、命令の実行結果を更新することも可能である。
【０１１６】
（第８の実施の形態）
本発明の第８の実施の形態の検証装置１Ｈの構成を図２３に示す。検証装置１Ｈの構成は、基本的に第３の実施の形態の検証装置１Ｃと同様であり、同一ないし同様の部分には第３の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＨを付して検証装置１Ｃと区別する。具体的には、検証装置１Ｈは、命令生成制約作成装置５０Ｈと、命令発行制約作成装置５１Ｈと、命令生成装置５２とを備える。命令生成制約作成装置５０Ｈと命令生成装置５２とは、検証装置本体２Ｈに設けられる。命令発行制約作成装置５１Ｈは実行制御装置４Ｈに設けられる。検証装置１Ｈは制御装置２３Ｈの構成および制御装置２３Ｈによる制御方法（検証方法）に特徴がある。
【０１１７】
検証装置１Ｈにおいては、命令は命令生成制約作成装置５０Ｈが生成する命令生成制約に基づいて命令生成装置５２により生成されて命令供給装置６に与えられる。命令生成制約とは、命令が生成される際の命令の種類や、オペランドとして選択可能なレジスタ番号の条件を示している。命令生成制約としては、”加算命令のオペランドで選択可能な汎用レジスタの番号はレジスタ０からレジスタ８までである”ことや、”ＶＬＩＷ方式のプロセッサであれば加算命令は同時に２個以上実行させることはできない”等がその例として挙げられる。
【０１１８】
命令生成装置５２は、命令生成制約の範囲内で命令をランダムに生成することが可能であり、プロセッサに与える命令を全てランダムに生成したり、手で作成した命令とランダムに生成した命令を混在させてプロセッサに供給することが可能である。
【０１１９】
検証装置１Ｈ全体として制御方法（検証方法）は図２１のフローチャートに示す第７の実施の形態の検証装置１Ｇの制御動作と同一である。そのため、検証装置１Ｈの制御方法（検証方法）全体の説明は省略する。
【０１２０】
本実施形態の検証装置１Ｈの制御装置２３Ｈは、命令の実行結果（シミュレーション結果および期待値）が未定義となると判断する場合に、実行結果を更新する追加命令を生成して命令供給装置６に供給する処理を実施することに特徴がある。検証装置１Ｈの制御方法（検証方法）における要部を図２４に示す。この処理方法は、第３の実施の形態の検証装置１Ｃにおける要部の処理方法と基本的に類似している。そのため、同一のステップには同一の符号を付している。しかしながら、次の処理において、検証装置１Ｈは検証装置１Ｃと異なる。
【０１２１】
検証装置１Ｈの制御装置２３Ｈは、命令の実行結果（期待値）が未定義となると判定する場合、未定義結果となる命令を、データ制約条件を有していない他の命令に置換する処理（図５におけるステップＳ５０２および図１１におけるステップＳ１１０３）は実施しない。その代わりとして、制御装置２３Ｈは、その命令の実行後に実行する更新命令を生成する処理（ステップＳ１１０３−１Ｈ）と、生成した更新命令を命令供給装置６に配給してその更新命令をシミュレーション装置７および期待値生成装置８で実行させる処理（ステップＳ１１０３−２Ｈ）とを実施する。
【０１２２】
更新命令とは、シミュレーション装置７や期待値生成装置８による命令実行結果（シミュレーション結果や期待値）を強制的に更新する命令である。制御装置２３Ｈは、命令の実行結果が未定義になると参照データ解析装置２２が判定した場合、命令生成装置５２にその未定義となる実行結果の更新命令の発行を意味する命令発行制約を発行させる。更新命令の具体例としては、未定義となる実行結果を格納している第１,第２記憶装置１１,１３からその実行結果を読み出して適当な値に更新させるメモリアクセス命令や、ＭＯＶ命令によりその実行結果を格納している第１,第２記憶装置１１,１２の記録データを適当な値に更新する命令を、挙げることができる。
【０１２３】
以上の更新命令の強制を意味する命令発行制約を命令生成装置５２に強制的に発行させてその命令発行制約を命令供給装置６に与える。命令供給装置６は、その命令発行制約に基づいて更新命令を生成して命令供給装置６に与える。命令供給装置６はその更新命令をシミュレーション装置７と期待値生成装置８とに供給してこれら装置７,８で更新命令を実行させる。これにより、実行結果が未定義となる命令が実行されたとしても、その実行結果（未定義）を参照する命令が実行される後処理として、その実行結果（未定義）を定義可能なデータに強制的に更新する処理が追加実施されることとなる。その結果、シミュレーション装置７による命令の実行結果と期待値生成装置８による命令の実行結果との間の不一致に起因する擬似エラーは防止される。
【０１２４】
なお、本実施の形態の制御方法は、図２３の検証装置１Ｈの構成の他、図２５の検証装置１Ｈ'でも同様に実施することができる。検証装置１Ｈ'は、基本的に検証装置１Ｈと同じ構成を備えており、同一ないし同様の部分には同一の符号を付している。しかしながら、若干異なる構成を有する部分には（'）を付している。
【０１２５】
検証装置１Ｈでは、制御装置２３Ｈの指示に基づいて命令発行制約作成装置５１Ｈが更新命令の命令発行制約を作成して命令生成装置５２に与える制御が実施される。これに対して、検証装置１Ｈ'では、命令発行制約を作成する命令発行制約作成装置５１Ｈは設けられない。これに代わって、制御装置２３Ｈ'は、命令生成制約作成装置５０Ｈ'に、以下に説明する命令生成制約の作成と、作成した命令生成制約の命令生成装置５２への供給とを強制する。
【０１２６】
制御装置２３Ｈ'が命令生成制約作成装置５０Ｈ'に強制する命令生成制約とは、未定義となった命令の実行結果（シミュレーション結果や期待値）の更新命令を命令生成装置５２によって強制発行させる制約である。これにより、検証装置１Ｈ'では、検証装置１Ｈと同様、未定義結果が発生した場合において、命令生成装置５２が未定義結果の更新命令を発行する。
【０１２７】
なお、検証装置１Ｈ,１Ｈ'では、未定義結果が生成された直後に未定義結果の更新命令を強制発行させる必要はない。特に命令生成装置５２がランダムに命令を生成する場合、未定義結果の生成直後にその更新命令を強制発行させると命令の生成順序に規則性が発生され命令をランダムに与える検証のランダム性が失われる。よって未定義結果を更新する命令は、未定義結果を参照する命令が実行される前に実行させても良い。その際に“未定義結果を参照する命令”の実行を把握するには、未定義結果が発生した時点で“未定義結果を参照する命令”を発行禁止にし、未定義結果の更新命令が発行された後に“未定義結果を参照する命令”の発行禁止を解除することが考えられる。
【０１２８】
本実施の形態では命令解析装置２１と参照データ解析装置２２とを用いて未定義結果の発生を判定したが、第２の実施の形態における未定義結果判定装置３２を用いても判定可能である。つまり期待値生成部１２における命令の実行結果情報から未定義結果の発生を判定し、その判定結果に基づいて更新命令を強制発行させることも可能である。
【０１２９】
（第９の実施の形態）
本発明の第９の実施の形態の検証装置１Ｊの構成を図２６に示す。検証装置１Ｊの構成は、基本的に第８の実施の形態の検証装置１Ｈと同様であり、同一ないし同様の部分には第８の実施の形態と同一の符号を付し、それらについての説明は省略する。ただし、同様の動作を行うものの若干異なる動作を行う部分には、その符号の末尾にＪを付して検証装置１Ｈと区別する。具体的には、検証装置１Ｈは、命令生成制約作成装置５０Ｊと、命令発行制約作成装置５１Ｊと、命令生成装置５２と、参照データ候補決定装置６０とを備える。また、データ情報抽出装置３Ｊによる制御方法（検証方法）が、第８の実施の形態におけるデータ情報抽出装置３Ａと異なる。命令生成制約作成装置５０Ｊと命令生成装置５２とは、検証装置本体２Ｈに設けられる。命令発行制約作成装置５１Ｊは実行制御装置４Ｈに設けられる。
【０１３０】
データ情報抽出装置３Ｊは、第２記憶装置１３からデータ制約条件を持つ命令毎に次のデータ値を抽出する。ここで抽出するデータ値とは、参照データとして選択可能なレジスタ番号とそのレジスタが格納しているデータ値である。参照データとして選択可能なレジスタ番号とは次のものをいう。例えばＤＩＶ命令では除数がゼロ以外であるというデータ制約条件を持っている。このＤＩＶ命令を実行時に除数として選択可能な汎用レジスタ番号が、前記参照データとして選択可能なレジスタ番号を示している。例えば、任意のデータ制約条件に基づいて命令実行時に選択可能な汎用レジスタ番号がレジスタ０からレジスタ３１までである場合を想定する。この場合、データ情報抽出装置３Ｊは、レジスタ０からレジスタ３１において現在格納しているデータ値を抽出する。データ情報の抽出は、データ制約条件を持つ命令毎に実施される。このようなデータ情報抽出を実現するため、データ情報抽出装置３Ｊは、データ制約情報格納部２０からデータ制約条件を読み出しつつデータ情報抽出を実施する。
【０１３１】
実行制御装置４Ｊは、データ情報抽出装置３Ｊから供給されるデータ情報と、データ制約情報格納部２０から供給されるデータ制約情報とから参照データ候補を決定する。ここでいう参照データ候補とは、データ制約条件をもつ命令が参照可能なレジスタ番号のことである。参照データ候補は命令毎に決定される。この動作は参照データ候補決定装置６０によって実施される。参照データ候補とは次のことが保証されたレジスタをいう。すなわち、”その候補の値がその命令のデータ制約条件を満足しておりその候補の値を参照データにしてその命令を発行しても未定義結果が発生しない”、という保証がなされたレジスタを、参照データ候補という。制御装置２３Ｊは、参照データ候補決定装置６０によって決定された参照データ候補を参照データとする命令の発行制約の作成指示を命令発行制約作成装置５１Ｊに行う。命令発行制約作成装置５１Ｊは、制御装置２３Ｊにより指示された命令発行制約を作成して命令生成装置５２に供給する。命令生成装置５２は、命令発行制約作成装置５１Ｊから供給される命令発行制約に基づいて命令を生成して命令供給装置６に供給する。命令供給装置６は、供給された命令をシミュレーション装置７と期待値生成装置８とに供給して実行させる。
【０１３２】
以下、検証装置１Ｊを用いた制御方法（検証方法）を、図２７のフローチャートと、図２８のフローチャートとを参照して説明する。なお、検証装置１Ｊを用いた検証方法は、基本的には第３の実施の形態の検証装置１Ｃの動作（図５参照）と同様である。そのため、同一の動作を実行する工程（ステップ）には、同一のステップ番号を付し、それらに付いての説明は省略する。但し、検証装置１Ｊでは、中間データの抽出（Ｓ５０２Ｊ）と、その抽出結果の解析とその解析結果に基づく制御（Ｓ５０３Ｊ）とを、命令の供給（Ｓ５０１）より時間的に前に実施している。以下、ステップＳ５０２Ｊ,Ｓ５０３Ｊの動作の詳細を、図２８のフローチャートを参照して説明する。
【０１３３】
まず、検証装置１Ｊを用いた検証方法の概要を説明する。データ情報抽出装置３Ｊが命令の中間データの抽出を行う。ここでいう中間データとは、前述したように、データ制約条件を持つ命令が参照データとして選択可能なレジスタ番号とそのレジスタが格納しているデータ値である。
【０１３４】
実行制御装置４Ｊは、データ情報抽出装置３Ｊから供給される中間データを用いて命令供給装置５２に供給する命令発行制約を作成する。命令生成装置５２は、供給される命令発行制約に基づいて命令を生成して命令供給装置６を介してシミュレーション装置７と期待値生成装置８とに供給する。シミュレーション装置７や期待値生成装置８の動作および比較装置９の動作は他の実施形態と同様である。
【０１３５】
以下、検証装置１Ｊを用いた検証方法の要部である実行制御装置４Ｊの処理を説明する。まず参照データ候補決定装置６０が、参照データとしてその命令で使用可能なレジスタ（参照データ候補）を決定する。参照データ候補は、データ制約条件のある命令全てに対応して決定される。以下、参照データ候補の決定方法の詳細を図２８のフローチャートを参照して説明する。
【０１３６】
参照データ候補決定装置６０は、データ制約条件を有する命令の一つを選択する（Ｓ２８０１）。データ情報抽出装置３Ｊから供給される中間データを用いて、参照データとして選択可能なレジスタが格納しているデータ値がデータ制約条件を満足しているか否かを解析する（Ｓ２８０２）。
【０１３７】
Ｓ２８０２で満足していると判断する場合、そのレジスタを参照データ候補とする（Ｓ２８０３）。この解析はその命令において参照データとして選択可能な全てのレジスタに対して行う（Ｓ２８０４）。
【０１３８】
データ制約条件を有する一つの命令においてＳ２８０２〜Ｓ２８０４の処理が終了したら、データ制約条件を有する他の命令があるか否かを判断する（Ｓ２８０５）。Ｓ２８０５で他の命令があると判断する場合は、Ｓ２８０２〜Ｓ２８０４の処理を実施する。これにより、データ制約条件を持つ全ての命令において、その参照データ候補（データ制約条件を満足する参照データ）を決定する。
【０１３９】
次に、全ての命令の参照データ候補が決定したのち、制御装置２３Ｊは次の制御を実施する。制御装置２３Ｊは、命令供給装置６がシミュレーション装置７と期待値生成装置８とに命令を供給する際において、参照データ候補決定装置６０で決定した参照データ候補を参照してその命令を実行するように制御する。このうな制御は、具体的には次のようにして実施される。まず、制御装置２３Ｊが、”その命令の実行に際しては参照データ候補決定装置６０で決定した参照データ候補を参照してその命令を実行する”という命令発行制約の作成を命令発行制約作成装置５１Ｊに指示する。この指示を受けて命令発行制約作成装置５１Ｊで生成される命令発行制約が、命令生成装置５２に供給される。命令発行制約を受けた命令生成装置５２は、その制約に従って命令を作成して命令供給装置６に与える。命令供給装置６は、与えられた命令（前記命令発行制約を含む）をシミュレーション装置７と期待値生成装置８とに供給する。これにより、上述した制御が実現される。
【０１４０】
なお、検証装置１Ｊの実行制御装置４Ｊは、参照データを格納しているレジスタ値を観測することでデータ制約条件を満足する参照データ候補をあらかじめ用意している。そして、データ制約条件のある命令をシミュレーション装置７と期待値生成装置８とに供給する際に、前記候補の中から参照データを選択させることで未定義結果の発生を防いでいる。
【０１４１】
また、検証装置１Ｊでは、データ制約条件のある全ての命令において、参照データとして選択可能な全てのレジスタが参照データ候補となり得るか否かを解析している。したがって、参照データ候補は通常、複数となる。しかしながら、参照データ候補は必ずしも複数必要になるとは限らない。そのため、参照データ候補が１つ決定した時点で次の命令に対する処理に遷移しても良い。そうすることで参照データ候補決定装置６０の実行時間を短縮することが可能である。また、参照データ候補が１つも無い場合には、その命令の発行を禁止するように命令供給装置６に指示すればよい。
【０１４２】
なお、本実施の形態の制御方法は、図２６の検証装置１Ｊの構成の他、図２９の検証装置１Ｊ'でも同様に実施することができる。検証装置１Ｊ'は、基本的に検証装置１Ｊと同じ構成を備えており、同一ないし同様の部分には同一の符号を付している。しかしながら、若干異なる構成を有する部分には（'）を付している。
【０１４３】
制御装置２３Ｊは、参照データ候補決定装置６０の候補決定結果を命令発行制約として命令生成装置５２に与えており、これにより、命令生成装置５２が生成する命令において未定義結果が発生することを防いでいる。これに対して、制御装置１Ｊ'は、参照データ候補決定装置６０の結果を、命令生成制約作成装置５０Ｊ'が生成する既存の命令生成制約に追加している。これにより検証装置１Ｊ’は、命令生成装置５２が生成する命令で未定義結果が発生することを防いでいる。したがって、検証装置１Ｊ'では、命令発行制約作成装置５１Ｊは設けられてない。
【０１４４】
以上、検証装置１Ｊ,１Ｊ'では、データ制約条件を有する命令が参照するレジスタ値から参照データ候補を決定している。そのため、命令生成装置５２が命令を生成する際にその参照データ候補を参照することで未定義結果となる命令の発生を防ぐことが可能となる。したがって、命令の実行結果が未定義結果となる命令の実行が阻止されて、擬似エラーによる検証の中断を防いで検証の高効率化が図れる。
【０１４５】
なお、第１から第９までの実施の形態における検証装置１Ａ〜１Ｊおよびその検証方法では、検証対象はプロセッサに限定されるわけでなく、検証対象で実行される処理の中間データの値に応じて実行結果が未定義となる検証対象全てに適用可能である。テストパターンについても、手で記述したテストパターンであってもランダムに生成したテストパターンでも構わない。また未定義結果についてであるが、各実施の形態では参照データのデータ制約条件を要因とする未定義結果について記述したが、データ情報抽出装置３Ａ,３Ｂ,３Ｊが未定義結果となる要因情報を抽出することができそれをデータ制約情報に登録することができるならば、未定義結果の要因がそれ以外の場合でも対応可能である。例えば、命令実行時に割込み等の外的要因により実行結果が未定義となる場合についても、第７の実施の形態のように未定義結果を更新することで対応可能である。
【産業上の利用可能性】
【０１４６】
本発明にかかる検証装置および検証方法は、テストパターンを検証対象のシミュレータと期待値とを生成するシミュレータに与える際のシミュレーション結果と期待値とを比較して検証する際に、命令の実行時に参照する参照データの値がデータ制約条件を満足していないことに起因して生じる、実行結果が未定義となって比較時に擬似エラーが発生する、という課題を解決している。
【０１４７】
具体的には、未定義結果の発生を事前に妨げたり、未定義結果が発生したことによる影響をそれ以降のシミュレーションを制御することで無くし擬似エラーによる検証の中断を防ぐことで、上記課題を解決し、これによって高効率な検証を実現している。本発明は、計算機上での半導体集積回路の検証等として特に有用である。
【図面の簡単な説明】
【０１４８】
【図１】本発明が実施される検証装置の従来構成を示すブロック図である。
【図２】本発明の検証装置の従来構成による検証方法を示すフローチャートである。
【図３】本発明の第１の実施の形態における検証装置の構成を示すブロック図である。
【図４】データ制約条件の例を示す図である。
【図５】第１の実施の形態の検証装置による検証方法を全体を示すフローチャートである。
【図６】第１の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図７】本発明の第２の実施の形態における検証装置の構成を示すブロック図である。
【図８】第２の実施の形態の検証装置による検証方法の全体を示すフローチャートである。
【図９】第２の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図１０】本発明の第３の実施の形態における検証装置の構成を示すブロック図である。
【図１１】第３の実施の形態の検証装置による検証方法の要部を示すブロック図である。
【図１２】本発明の第４の実施の形態における検証装置の構成を示すブロック図である。
【図１３】第４の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図１４】第４の実施の形態の検証装置による検証方法のさらに要部を示すフローチャートである。
【図１５】本発明の第５の実施の形態における検証装置の構成を示すブロック図である。
【図１６】第５の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図１７】第５の実施の形態の検証装置による検証方法のさらに要部を示すフローチャートである。
【図１８】本発明の第６の実施の形態における検証装置の構成を示すブロック図である。
【図１９】第６の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図２０】本発明の第７の実施の形態における検証装置の構成を示すブロック図である。
【図２１】第７の実施の形態の検証装置による検証方法の全体を示すフローチャートである。
【図２２】第７の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図２３】本発明の第８の実施の形態における検証装置の構成を示すブロック図である。
【図２４】第８の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図２５】第８の実施の変形例の構成を示すブロック図である。
【図２６】本発明の第９の実施の形態における検証装置の構成を示すブロック図である。
【図２７】第９の実施の形態の検証装置による検証方法の全体を示すフローチャートである。
【図２８】第９の実施の形態の検証装置による検証方法の要部を示すフローチャートである。
【図２９】第９の実施の形態の変形例の構成を示すブロック図である。
【符号の説明】
【０１４９】
１Ａ,１Ｂ,１Ｃ,１Ｄ,１Ｅ,１Ｆ,１Ｇ,１Ｈ,１Ｊ  検証装置
２Ａ,２Ｂ,２Ｈ,２Ｈ',２Ｊ,２Ｊ'  検証装置本体
３Ａ,３Ｂ,３Ｊ  データ情報抽出装置
４Ａ,４Ｂ,４Ｃ,４Ｄ,４Ｅ,１Ｆ,１Ｇ,１Ｈ,１Ｊ  実行制御装置
５  回路データ部
６  命令供給装置
７,７Ｂ  シミュレーション装置
８,８Ｂ  期待値生成装置
９  比較装置
１０  シミュレーション実行部
１１  第１記憶装置
１２  期待値生成部
１３  第２記憶装置
２０  データ制約情報格納部
２１  命令解析装置
２２  参照データ解析装置
２３Ａ,２３Ｂ,２３Ｃ,２３Ｄ,２３Ｅ,２３Ｆ,２３Ｇ,２３Ｈ,２３Ｈ',２３Ｊ,
２３Ｊ'  制御装置
３０  前状態戻り装置
３１  実行待機装置
３２  未定義結果判定装置
４０  参照データの候補探索装置
４１  参照データの候補解析装置
４２  参照データ置換装置
４３  命令生成装置
４４  命令配置装置
５０Ｈ,５０Ｈ',５０Ｊ,５０Ｊ'  命令生成制約作成装置
５１  命令発行制約作成装置
５２  命令生成装置
６０  参照データ候補決定装置
【図１】
2005208762.tif 000003
【図２】
2005208762.tif 000004
【図３】
2005208762.tif 000005
【図４】
2005208762.tif 000006
【図５】
2005208762.tif 000007
【図６】
2005208762.tif 000008
【図７】
2005208762.tif 000009
【図８】
2005208762.tif 000010
【図９】
2005208762.tif 000011
【図１０】
2005208762.tif 000012
【図１１】
2005208762.tif 000013
【図１２】
2005208762.tif 000014
【図１３】
2005208762.tif 000015
【図１４】
2005208762.tif 000016
【図１５】
2005208762.tif 000017
【図１６】
2005208762.tif 000018
【図１７】
2005208762.tif 000019
【図１８】
2005208762.tif 000020
【図１９】
2005208762.tif 000021
【図２０】
2005208762.tif 000022
【図２１】
2005208762.tif 000023
【図２２】
2005208762.tif 000024
【図２３】
2005208762.tif 000025
【図２４】
2005208762.tif 000026
【図２５】
2005208762.tif 000027
【図２６】
2005208762.tif 000028
【図２７】
2005208762.tif 000029
【図２８】
2005208762.tif 000030
【図２９】
2005208762.tif 000031