(57)【要約】【課題】浮動小数点数演算器の特殊演算ケースの検証の進捗度合を、内部のとりうる値やおこりうる例外に着目して、定量的に計測可能して、信頼性の高い検証を行えるようにする。【解決手段】ＲＴＬ記述によるハードウェア記述言語を解釈実行して、入力値に対して出力値として出力する論理シミュレータと、入力値に対して規定の演算を行い、期待値として出力する高信頼演算器とを有し、論理シミュレータの出力する出力値と、高信頼演算器の出力する期待値とを比較することにより、ハードウェア記述言語により機能を記述された演算器を検証する演算器を検証するダイナミック検証装置を有し、ダイナミック検証装置は、ハードウェア記述言語により記述されたモジュールの内部に用いられる中間ポートを参照し、ある中間ポートの取りうる値に対しての検証の網羅性を算出して、中間値カバレッジとして出力する。【選択図】  図１
2019185301.tif 000002
【特許請求の範囲】
【請求項１】
ＲＴＬ（Register Transfer Level）記述によるハードウェア記述言語により機能を記述された演算器を検証する演算器の検証装置であって、
前記ハードウェア記述言語を解釈実行して、入力値に対して出力値として出力する論理シミュレータと、
入力値に対して規定の演算を行い、期待値として出力する高信頼演算器とを有し、前記論理シミュレータの出力する出力値と、前記高信頼演算器の出力する期待値とを比較することにより、前記ハードウェア記述言語により機能を記述された演算器を検証する演算器を検証するダイナミック検証装置を有し、
前記ダイナミック検証装置は、前記ハードウェア記述言語により記述されたモジュールの内部に用いられる中間ポートを参照し、
ある中間ポートの取りうる値に対しての検証の網羅性を算出して、中間値カバレッジとして出力することを特徴とする演算器の検証装置。
【請求項２】
前記ハードウェア記述言語により機能を記述された演算器は、浮動小数点数演算器であることを特徴とする請求項１記載の演算器の検証装置。
【請求項３】
前記ダイナミック検証装置に、前記ハードウェア記述言語により機能を記述された演算器のモジュールと対応して、前記モジュールの入力ポートの値と同一の入力値に対して同一の出力値を出力する関数が入力され、
前記ダイナミック検証装置は、ある中間ポートの取りうる値に対して、検証していない不足中間値を求め、前記モジュールに対応する関数により、前記不足中間値に対応する入力ポートの値を求めることを特徴とする請求項１記載の演算器の検証装置。
【請求項４】
前記不足中間値に対応する入力ポートの値を、前記論理シミュレータと前記高信頼演算器とに入力し、それぞれの出力する期待値と出力値とを比較することを特徴とする請求項３記載の演算器の検証装置。
【請求項５】
ＲＴＬ（Register Transfer Level）記述によるハードウェア記述言語により機能を記述された演算器を検証する演算器の検証装置であって、
前記ハードウェア記述言語を解釈実行して、入力値に対して出力値として出力する論理シミュレータと、
入力値に対して規定の演算を行い、期待値として出力する高信頼演算器とを有し、前記論理シミュレータの出力する出力値と、前記高信頼演算器の出力する期待値とを比較することにより、前記ハードウェア記述言語により機能を記述された演算器を検証する演算器を検証するダイナミック検証装置を有し、
前記ダイナミック検証装置は、前記ハードウェア記述言語により記述されたモジュールの入力値における例外が発生する境界値に対しての検証の網羅性を算出して、例外発生境界カバレッジとして出力することを特徴とする演算器の検証装置。
【請求項６】
前記ハードウェア記述言語により機能を記述された演算器は、浮動小数点数演算器であることを特徴とする請求項５記載の演算器の検証装置。
【請求項７】
前記例外は、Ｚｅｒｏ除算例外、または、オーバーフロー例外であることを特徴とする請求項５記載の演算器の検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、演算器の検証装置に係り、特に、浮動小数点数を扱う演算器で、内部のとりうる値やおこりうる例外に着目した検証の網羅性を担保して、信頼性の高い検証を行うのに好適な演算器の検証装置に関する。
【背景技術】
【０００２】
産業機器向けの計装制御装置の一部には、高い安全性が要求される。例えば、原子力発電所が故障した場合には人間社会や周囲の環境に及ぼす影響が大きいため、故障のリスクを許容範囲まで低減することが必須である。このため、これら産業機器向けの計装制御装置上で実行される演算アプリケーションには誤り、すなわちバグがないことが求められる。演算アプリケーションで用いられる多種多様な数値計算関数の演算の中核を担うユニットモジュールは、浮動小数点数演算器であるため、浮動小数点数演算器にバグが発生しないように正しい開発プロセスを踏む必要がある。バグを未然に防ぐ目的においては、浮動小数点数演算器の開発プロセスの中でも特に重要なのは検証である。浮動小数点数演算器は、固定小数点数演算器と比較して非常に複雑であり、また、演算の入力パターンには見落としがちな特殊演算ケースが多数存在する。可能であれば、検証時に浮動小数点数演算器に全入力パターンを入力し出力値の正しさを調べることで設計の正しさを証明すべきである。しかしながら、入力数が二つの加算器や乗算器は、精度が単精度（３２ビット）の場合に、入力パターン数が２の６４乗通りとなり、全入力パターンに対して特殊演算ケースを調査することは実質的に不可能である。
【０００３】
したがって、現実的な工数で検証を完了する必要があるため、カバレッジという概念を導入して、全入力パターンを検証する検証全体の母数に対して現状の検証進捗度合が、どの程度十分であるか定量的に測定する必要がある。
【０００４】
カバレッジによる検証に関しては、例えば、特許文献１には、ＲＴＬ（Register Transfer Level）記述を前提とした回路検証において、ＲＴＬ記述の全記述のうち、シミュレーションで何行実行されたかを計測するラインカバレッジが説明されている（段落番号０００２）。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００８−５９０３２号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
特許文献１に記載のＲＴＬ記述の回路記述言語により記述された回路のラインカバレッジで計測可能な検証進捗度合の適用範囲は、一般的な固定小数点数演算器や制御回路であり、複雑な浮動小数点数演算器の特殊演算ケースには適用不可能な問題がある。これは、浮動小数点数演算器は、動作が複雑であり、上述のように検証すべき入力値の入力パターンの組合せと、その出力値の出力パターンが膨大になることが要因である。
【０００７】
このように、従来のカバレッジの計測においては、入力値の入力パターンの組合せと、その出力値の出力パターンにのみ、着目して、浮動小数点数演算器の内部で取りうる値と、カバレッジの関係については考慮されていない。入力値の入力パターンの組合せと、その出力値の出力パターンの組合せが膨大であっても、浮動小数点数演算器の内部で取りうるある値のパターンが少ないときには、その値に着目して、検証することにより、カバレッジの値を上げることができ、検証の信頼性を向上させることができる。然し、特許文献１の回路検証のカバレッジの計測は、それをどのようにおこなうのか示唆されていない。
【０００８】
また、浮動小数点数演算器には、浮動小数点数演算に際しての様々な例外（例えば、Ｚｅｒｏ除算（Division by Zero）、オーバーフロー（Overflow））が定義されている。このような例外発生が起こりうる入力値の境界で検証することは、浮動小数点数演算器の信頼性を向上させるのに、重要な意義を有する。しかしながら、特許文献１の回路検証のカバレッジの計測においては、例外発生が起こりうる入力値の境界でのカバレッジをどのように計測すればよいかについては示唆されていない。
【０００９】
本発明の目的は、浮動小数点数演算器の特殊演算ケースの検証の進捗度合を定量的に計測可能して、信頼性の高い検証をおこなうことのできる演算器の検証装置を提供することにある。
【課題を解決するための手段】
【００１０】
本発明の演算器の検証装置の構成は、好ましくは、ＲＴＬ（Register Transfer Level）記述によるハードウェア記述言語により機能を記述された演算器を検証する演算器の検証装置であって、ハードウェア記述言語を解釈実行して、入力値に対して出力値として出力する論理シミュレータと、入力値に対して規定の演算をおこない、期待値として出力する高信頼演算器とを有し、論理シミュレータの出力する出力値と、高信頼演算器の出力する期待値とを比較することにより、ハードウェア記述言語により機能を記述された演算器を検証する演算器を検証するダイナミック検証装置を有し、ダイナミック検証装置は、ハードウェア記述言語により記述されたモジュールの内部に用いられる中間ポートを参照し、ある中間ポートの取りうる値に対しての検証の網羅性を算出して、中間値カバレッジとして出力するようにしたものである。
【００１１】
また、本発明の演算器の検証装置の構成は、好ましくは、ＲＴＬ記述によるハードウェア記述言語により機能を記述された演算器を検証する演算器の検証装置であって、ハードウェア記述言語を解釈実行して、入力値に対して出力値として出力する論理シミュレータと、入力値に対して規定の演算をおこない、期待値として出力する高信頼演算器とを有し、論理シミュレータの出力する出力値と、高信頼演算器の出力する期待値とを比較することにより、ハードウェア記述言語により機能を記述された演算器を検証する演算器を検証するダイナミック検証装置を有し、ダイナミック検証装置は、ハードウェア記述言語により記述されたモジュールの入力値における例外が発生する境界値に対しての検証の網羅性を算出して、例外発生境界カバレッジとして出力するようにしたものである。
【発明の効果】
【００１２】
本発明によれば、浮動小数点数演算器の特殊演算ケースの検証の進捗度合を定量的に計測可能して、信頼性の高い検証をおこなうことのできる演算器の検証装置を提供することができる。
【図面の簡単な説明】
【００１３】
【図１】浮動小数点数演算器の検証装置の機能構成図である。
【図２】検証対象とする浮動小数点数演算器の回路構成と、その回路構成に対応するＳＶＡ、ＲＴＬ、ＬＩＢの内容を示す図である。
【図３】浮動小数点数演算器の検証装置のハードウェア・ソフトウェア構成図である。
【図４】ダイナミック検証装置の機能構成図である。
【図５】ダイナミック検証装置の計側部の機能構成図である。
【図６】入力生成部の機能構成図である。
【図７】浮動小数点数演算器の検証装置の全体処理を示すフローチャートである。
【図８】形式検証の処理を示すフローチャートである。
【図９】ダイナミック検証装置によるダイナミック検証の処理を示すフローチャートである。
【図１０】論理シミュレータにおける中間値指向のダイナミック検証の実行イメージを示す図である。
【図１１】中間値指向のダイナミック検証の処理を示すフローチャートである。
【図１２】検査対象ポートについての処理を示すフローチャートである。
【図１３】検査対象不足中間値の処理を示すフローチャートである。
【図１４】加算器における例外発生境界指向のダイナミック検証の検証内容の例を示す図である。
【図１５】加算器における例外発生境界指向のダイナミック検証の処理を示すフローチャートである。
【図１６】（Ｘ１，Ｘ２）周辺の境界探索と照合の処理を示すフローチャートである。
【図１７】乗算器における例外発生境界指向のダイナミック検証の検証内容の例を示す図である。
【図１８】乗算器における例外発生境界指向のダイナミック検証の処理を示すフローチャートである。
【図１９】除算器における例外発生境界指向のダイナミック検証の検証内容の例を示す図である。
【図２０】除算器における例外発生境界指向のダイナミック検証の処理を示すフローチャートである。
【図２１】完全乱数によるダイナミック検証の処理を示すフローチャートである。
【発明を実施するための形態】
【００１４】
以下、本発明に係る一実施形態を、図１ないし図２１を用いて説明する。
【００１５】
先ず、図１ないし図６を用いて本発明の一実施形態に係る浮動小数点数演算器の検証装置の構成について説明する。
本実施形態で説明する浮動小数点数演算器の検証装置は、検証される浮動小数点数演算器の機能がＲＴＬの記述レベルを有するハードウェア記述言語（例えば、Verilog HDL）で記述されていることを前提とする。
【００１６】
先ず、図１と図２を用いて浮動小数点数演算器の検証装置に入力されるデータと本実施形態に関連するハードウェア記述言語の基礎概念について説明する。
浮動小数点数演算器の検証装置１００には、図１に示されるように、ＲＴＬ４００、ＬＩＢ４１０、ＳＶＡ４２０、検査対象ポートリスト８００が入力される。
【００１７】
ハードウェア記述言語では、ハードウェア記述言語の記述の抽象度（水準）が定義されている。ＲＴＬとは、レジスタと演算器とその間の配線（接続）を記述する抽象度のレベルである。ＲＴＬ４００とは、ＲＴＬで記述されたハードウェア記述言語のソースコードを意味するものとする。
【００１８】
ハードウェア記述言語におけるアサーションは、設計した回路で期待されている動作や禁止されている動作を記述した文であり、このアサーションをベースとした検証により、ＲＴＬで記述されたハードウェア記述言語の論理シミュレータの動作を検証することができる。アサーションを記述する言語としては、代表的なものに、ＳＶＡ（System Verilog Assertion）があり、ＳＶＡ４２０は、ＳＶＡで記述されたソースコードを意味するものとする。
【００１９】
Verilog HDLなどのハードウェア記述言語においては、機能単位を「モジュール」としてとらえ、その入出端子を仮想化したものを「ポート」としている。本実施形態でも、これらの用語を用いることにする。
【００２０】
浮動小数点数演算器をソフトウェアで記述した機能構成が図２に示される。図２において、入力ポートとしてＩＮＰＵＴ＿１、ＩＮＰＵＴ＿２の二つを有し、出力ポートとしてＯＵＴＰＵＴを持ち、例外出力ポートとして、ＥＸＣＥＰＴＩＯＮを有するものとする。
【００２１】
ここで、浮動小数点数演算器の機能を記述するモジュールを「トップモジュール」ということにする。トップモジュールは、その内部構成として、下位モジュールのモジュールＡ、モジュールＢ、モジュールＣ、…、モジュールＺと機能ブロックレベルで分割されており、ＲＴＬ４００は、この回路構成のモジュールレベルで記述されている。また、トップモジュールの内部のポート（下位レベルの入力ポート、出力ポートでもある）を「中間ポート」または「内部ポート」ということにする。さらに、中間ポートの取りうる値を「中間値」ということにする。
【００２２】
形式検証用の検証プログラムのＳＶＡ４２０は、このＲＴＬ４００のモジュールレベルでの検証をおこなうために、各モジュールに一対一で対応するようにアサーション記述される。すなわち、浮動小数点数演算器はそのサブモジュールそれぞれについて要求仕様が定義されており、モジュールＡ、モジュールＢ、モジュールＣ、…、モジュールＺそれぞれに対してその要求仕様を満足するか否かを証明するアサーションＡ、アサーションＢ、アサーションＣ、…、アサーションＺが用意してある。また、浮動小数点数演算器のトップモジュールの要求仕様ついては、トップアサーションで動作記述の正しさの証明をおこなう。なお、浮動小数点数演算器の演算内容は、形式検証のアサーション記述では表現不可能のため、トップアサーションではインターフェースプロトコルなど上位階層との接続に必要な機能についての証明をおこなう。
【００２３】
ＬＩＢ（演算ライブラリ）４１０は、不足中間値を求める際に、モジュールの出力ポートの値から入力ポートの値を求めるときに使用される（詳細は後述）関数のソースコードであり、ＲＴＬの各モジュールと一対一となるように関数が構成されている。各関数は、各モジュールと同一の演算内容となるように設計されている。すなわち、トップモジュールとトップ関数が対応しており、モジュールＡ、モジュールＢ、モジュールＣ、…、モジュールＺと関数Ａ、関数Ｂ、関数Ｃ、…、関数Ｚの演算内容は、ＲＴＬのタイミング情報をのぞき、それぞれ等価である。ここで、等価とは、モジュールと同一の入力値に対して、同じ出力値を返すことを意味する。
【００２４】
検査対象ポートリスト８００は、中間値カバレッジを取得する対象とするポートのリストである（詳細は後述）。
【００２５】
次に、本実施形態の浮動小数点数演算器の検証装置の構成と、これらのデータを入力しておこなう検証について説明する。
浮動小数点数演算器の検証装置１００は、図１に示されるように、制御部１１０、形式検証装置２００、ダイナミック検証装置３００、検証結果集約部１２０からなる。制御部１１０は、検証装置の全体的な動作を監視し制御する部分である。
【００２６】
これまでに述べたとおり、浮動小数点数演算器の検証装置１００は、浮動小数点数演算器の信頼性を担保することを目的としている。この目的を達成するために、検証装置は二つの異なる検証方式で浮動小数点数演算器の検証をおこなう。一つは、形式検証であり、今一つは、ダイナミック検証である。浮動小数点数演算器の検証装置１００においては、形式検証装置２００が、浮動小数点数演算器のＲＴＬ４００を形式検証し、ダイナミック検証装置３００が、浮動小数点数演算器のＲＴＬ４００をダイナミック検証する。
【００２７】
形式検証は、ＲＴＬ４００の動作記述が要求仕様を満たしていることを論理的に証明する検証方式であり、形式検証プログラムであるＳＶＡ４２０に証明が記述されている。形式検証ツールがＲＴＬ４００とそのＲＴＬ４００に対する証明が記載されているＳＶＡ４２０のセットを読み込むことで証明が実行され、証明が完了すると実行結果のデータとして証明結果６３０とラインカバレッジ５２０を得ることができる。証明結果６３０には、証明が完了したか証明が完了できなかったが記載されており、証明が完了しなかった場合には反例が記載される。ラインカバレッジ５２０は、形式検証の証明においてＳＶＡが参照したＲＴＬの行数の割合を反映する指標である。浮動小数点数演算器全体としての潜在的なバグの低減を目的とした場合に、浮動小数点数演算器を構成するすべてのＲＴＬのすべての行が要求仕様通りに正しく動作している証明が完了している必要がある。形式検証装置がラインカバレッジを計測しそれが１００％を達成していることを確認することにより、浮動小数点数演算器が要求仕様通りに正しく設計されていることが確認可能である。
【００２８】
しかしながら、形式検証においては、浮動小数点数演算器の入力パターンデータに対する出力パターンデータを網羅的に検証することは非常に困難である。これは浮動小数点数演算器の入力パターンには、非常に多くの特殊演算ケースが存在するため、それらすべての特殊演算ケースを要求仕様として定義し、ＳＶＡに記載する数式で網羅的に表現することは非現実的であるからである。そこで、形式検証では網羅しきれない入出力データが正しいか否かを検証するために、浮動小数点数演算器の検証装置１００では、ダイナミック検証装置３００を導入する。ダイナミック検証装置３００は、検証装置に入力される浮動小数点数演算器と同じ種類の使用実績のある演算器を内部に備えている。
【００２９】
本明細書では、この使用実績のある演算器を以下、「高信頼モデル」、「高信頼演算器」ということにする。ダイナミック検証装置３００は、ＲＴＬ４００と高信頼モデルに同じ入力データを印加し、その結果が一致しているか否かを確認する。これを、検証の規格で定める十分な回数をおこない、各試行の入力データや高信頼モデルとＲＴＬ４００のそれぞれの出力データやそれらの一致ないし不一致の結果は、照合結果６２０に保存される。検証対象とする浮動小数点数演算器に設計ミスやバグなどがなければ、全ての入力パターンに対して、ＲＴＬ４００の演算結果が高信頼モデルの演算結果と一致することが期待される。
【００３０】
例外発生境界カバレッジ５１０と中間値カバレッジ５００は、ともに、ダイナミック検証装置３００が、特に重点的に調査すべき特殊なデータ入力パターンの検証の網羅性を示す指標である。
【００３１】
浮動小数点数演算器は、演算結果がそのビットフィールドで表現可能な値を逸脱する場合、０で除算するなどの不正な演算が実行された場合に、オーバーフロー例外やＺｅｒｏ除算例外などの例外を出力する。高い安全性が要求されるシステムには、例外が発生するデータパターンでは演算器から正しく例外が出力されることが要求される。したがって、例外が発生しない入力データに対しては例外が発生せず、例外が発生する入力データに対しては例外が正しく発生することを検証する必要がある。この目的を達成するために、例外が発生する入力データと例外が発生しない入力データの境界をすべてでダイナミック検証を実行し照合結果も正しい必要がある。例外が発生する境界値の検証の網羅性を確認するために、検証すべき例外の境界すべてを母数とした場合の、母数に対する照合結果の一致数を例外発生境界カバレッジ５１０として出力する。
【００３２】
また、中間値カバレッジ５００は、後に詳しく述べるが、浮動小数点数演算器の内部のポートごとに、その取りうる値に対しての検証の網羅性を示す指標である。中間値カバレッジ５００を参照することにより、浮動小数点数演算器の様々な特殊演算ケースについての検証の網羅性が知ることができる。ここで、検査対象ポートリスト８００は、中間値カバレッジ５００を取得すべき内部ポートの情報のリストである。
【００３３】
検査対象ポートリスト８００は、中間値カバレッジ５００を取得する検証プロセスで順番にポートを検査していく。ＬＩＢ４１０は、中間値カバレッジ５００算出の際に、モジュールに対する出力ポートの値から入力ポートの値を算出するための関数からなるデータである（詳細は後述）。証明結果６３０、照合結果６２０、ラインカバレッジ５２０、例外発生境界カバレッジ５１０、中間値カバレッジ５００の各種検証結果が揃うと、検証結果集約部１２０がそれらの情報をまとめて人にとってわかりやすい形式で検証結果を出力する。検証結果６００内の総合カバレッジ６１０は、各種カバレッジの状況を数値で示すためのものである。検証結果６００内の詳細情報６１１は、形式検証の証明結果や反例、照合結果それぞれの内容と発生する具体的な条件を示したものである。
【００３４】
次に、図３を用いて、浮動小数点数演算器の検証装置のハードウェア・ソフトウェア構成について説明する。
浮動小数点数演算器の検証装置１００のハードウェア構成としては、例えば、図３に示されるような一般的な情報処理装置、例えば、パーソナルコンピュータで実現される。
浮動小数点数演算器の検証装置１００は、ＣＰＵ（Central Processing Unit）９０２、主記憶装置９０４、ネットワークＩ／Ｆ９０６、表示Ｉ／Ｆ９０８、入出力Ｉ／Ｆ９１０、補助記憶Ｉ／Ｆ９１２が、バスにより結合された形態になっている。
【００３５】
ＣＰＵ９００は、浮動小数点数演算器の検証装置１００の各部を制御し、主記憶装置９０４に必要なプログラムをロードして実行する。また、ＣＰＵ９００には、コプロセッサとして、ＦＰＵ９０２（Floating Point Unit：浮動小数演算ユニット）が内蔵されており、浮動小数点演算の命令語をフッチしたときには、ＦＰＵ９０２に処理を依頼して実行させる。ＦＰＵ９０２が、ハードウェアで実現した高信頼モデルに該当する。本実施形態では、ＦＰＵ９０２をＣＰＵ９００のコプロセッサとして実現する形式を示したが、Ｉ／Ｏポートを接続して、通常の周辺機器と同様にＩ／Ｏポートを介してデータのやり取りをおこなう、いわゆる、Ｉ／Ｏプロセッサ形式でもよい。主記憶装置９０４は、通常、ＲＡＭなどの揮発メモリで構成され、ＣＰＵ９００が実行するプログラム、参照するデータが記憶される。
【００３６】
ネットワークＩ／Ｆ９０６は、ネットワークと接続するためのインタフェースである。表示Ｉ／Ｆ９０８は、ＬＣＤ（Liquid Crystal Display）などの表示装置９２０を接続するためのインタフェースである。入出力Ｉ／Ｆ９１０は、入出力装置を接続するためのインタフェースである。図３の例では、キーボード９３０とポインティングデバイスのマウス９３２が接続されている。
【００３７】
補助記憶Ｉ／Ｆ９１２は、ＨＤＤ（Hard Disk Drive）９５０やＤＶＤドライブ（Digital Versatile Disk）などの補助記憶装置を接続するためのインタフェースである。
【００３８】
ＨＤＤ９５０は、大容量の記憶容量を有しており、本実施形態を実行するためのプログラムが格納されている。浮動小数点数演算器の検証装置１００には、論理シミュレータプログラム１０００、形式検証プログラム１０１０、期待値・比較値比較プログラム１０２０、不足中間値生成プログラム１０３０、境界値探索プログラム１０４０、乱数生成プログラム１０５０がインストールされている。
【００３９】
論理シミュレータプログラム１０００は、ダイナミック検証装置３００における論理シミュレータ（後述）を実行するプログラムである。形式検証プログラム１０１０は、形式検証装置２００における形式検証をおこなうプログラムである。期待値・出力値比較プログラム１０２０は、高信頼モデルの出力する期待値とを照合し比較するプログラムである。不足中間値生成プログラム１０３０は、中間値指向のダイナミック検証において、不足中間値（詳細は後述）を生成するプログラムである。境界値探索プログラム１０４０は、例外発生指向のダイナミック検証において、検証するべき境界値を探索するプログラムである。乱数生成プログラム１０５０は、検証の対象を求めるための元データとなる乱数を生成するプログラムである。
【００４０】
次に、図４を用いてダイナミック検証装置の機能構成について説明する。
ダイナミック検証装置３００は、浮動小数点数演算器のＲＴＬ４００と、それと同種類の演算をおこなう高信頼モデル２２０の比較をおこなう。比較に際しては、同じ入力データをそれぞれに入力し、ＲＴＬ４００の出力値と高信頼モデル２２０の期待値が一致するか否かを確かめる。論理シミュレータ２３０は、ＲＴＬ４００を受け取り、ＲＴＬ４００の動作記述に従って実際の論理回路と同等の動作を提供する機能部である。ＲＴＬ４００は、論理シミュレータ２３０上で動作し、演算結果としての出力値７２０や中間ポートの中間値７３０を出力する。
【００４１】
入力生成部２１０は、主に乱数に基づき入力値を生成する機能部である。本実施形態のダイナミック検証装置３００の検証方法は、三種類のダイナミック検証から構成される。三種類のダイナミック検証とは、中間値指向のダイナミック検証と、例外境界値指向のダイナミック検証と、完全乱数のダイナミック検証である（詳細は後述）。
【００４２】
中間値指向のダイナミック検証において、入力生成部２１０は、入力値７００を出力し、それを論理シミュレータ２３０に入力する。中間値指向のダイナミック検証においては、ＬＩＢ４１０と不足中間値リスト７４０を用いて入力値を生成する場合がある（詳細は後述）。
【００４３】
計測部２４０は、高信頼モデル２２０から期待値７１０、論理シミュレータ２３０から出力値７２０と中間値７３０、入力生成部２１０から入力値７００と、検査対象ポートリスト８００のポート情報８１０を受け取り、ダイナミック検証装置３００の出力データである照合結果６２０や例外発生境界カバレッジ５１０や中間値カバレッジ５００を出力する。ここで、ポート情報８１０とは、検査対象ポートリスト８００に挙げられる中間値カバレッジの計測対象とする中間ポートに関する情報である。
なお、これらダイナミック検証装置３００の内部に存在する各種下位装置の機能や働きは、後の図９ないし図２０に示すフローチャートで詳細に説明する。
【００４４】
次に、図５を用いてダイナミック検証装置における計測部の機能構成について説明する。
計測部２４０は、図５に示されるように、比較部２４１、検証結果集計部２４２、中間値集計部２４３からなる。
【００４５】
比較部２４１は、高信頼モデル２２０の演算結果である期待値７１０とＲＴＬ４００の論理シミュレータ２３０上での演算結果である出力値７２０を比較する。そして、１回分の比較に用いた入力値７００と出力値７２０と期待値７１０と、それらの比較結果と、ポート情報８１０と中間値７３０を、関連付けて検証サンプル７７０として保存する。検証サンプル７７０は、検証ログ７８０に保存され、中間値７３０は、中間値ログ７６０に保存される。
【００４６】
検証結果集計部２４２は、中間値指向ダイナミック検証では、検証ログ７８０から照合結果６２０と中間値カバレッジ５００を出力し、例外発生境界指向ダイナミック検証では、検証ログ７８０から照合結果６２０と例外発生境界カバレッジ５１０を出力し、完全乱数ダイナミック検証では照合結果６２０のみを出力する。中間値指向ダイナミック検証では、中間値集計部２４３が中間値ログ７６０と検査対象ポートのビット幅から不足中間値（詳細は後述）を割り出し、不足中間値リスト７４０を出力する。
【００４７】
次に、図６を用いてダイナミック検証装置における入力生成部の機能構成について説明する。
入力生成部２１０は、ライブラリ選択部２１１、乱数生成部２１２、不足中間値生成部２１３、入力値算出部２１４からなる。
【００４８】
完全乱数ダイナミック検証では、入力値算出部２１４は、乱数生成部２１２の出力した乱数から入力値７００を出力する。中間値指向ダイナミック検証は、先ず乱数生成部２１２の生成する乱数から入力値７００を生成し、中間値指向ダイナミック検証途中で、不足中間値リスト７４０が生成された場合には、不足中間値選択部２１３により、不足中間値７５０を一つ選択し、ライブラリ選択部２１１がＬＩＢ４１０からいずれかの関数を呼び出して、入力値算出部２１４が入力値を算出する（詳細は後述）。
【００４９】
次に、図７ないし図２１を用いて浮動小数点数演算器の検証装置の処理について説明する。
先ず、図７を用いて浮動小数点数演算器の検証装置の全体処理を説明する。
浮動小数点数演算器の検証装置の全体処理では、先ず、形式検証装置２００による形式検証処理をおこなう（Ｓ２００）。
【００５０】
次に、ダイナミック検証装置３００によるダイナミック検証をおこなう（Ｓ３００）。
そして、検証結果６００を出力する（Ｓ１１０）。
検証結果６００の出力としては、形式検証における全体証明数に対する証明完了数やラインカバレッジ５２０、ダイナミック検証における全体照合数に対する一致数や例外発生境界カバレッジ５１０、中間値カバレッジ５００を総合カバレッジ６１０として出力する。詳細情報６１１には、形式検証で証明の対象にならなかった行や反例が出てしまったモジュールとアサーション情報、ダイナミック検証の照合で不一致となった入出力パターンや不足中間値が出てしまった中間値カバレッジ５００の情報を出力する。
【００５１】
次に、図８を用いて形式検証装置による形式検証の処理について説明する。
これは、図７におけるＳ２００の処理である。
先ず、トップモジュールをトップアサーションで形式検証し証明する（Ｓ２０１）。その証明の結果と、証明の対象となったトップモジュールの行数と、トップモジュール全体の行数を記録する。
【００５２】
次に、初期処理として、モジュールＡを検証対象モジュールＭＯＤとし、アサーションＡを形式検証プログラムＡＳＥとする（Ｓ２０２）。
次に、検証対象モジュールＭＯＤを形式検証プログラムＡＳＥで形式検証し証明する。そして、その証明の結果と、証明の対象となったトップモジュールの行数と、トップモジュール全体の行数を記録する（Ｓ２０３）。
次に、ＲＴＬ４００のすべてのモジュールを形式検証で検証したか否かを判定し（Ｓ２０４）、すべてのモジュールを形式検証で検証した場合には（Ｓ２０４：ＹＥＳ）、Ｓ２０６に進み、そうでない場合には（Ｓ２０４：ＮＯ）、Ｓ２０５に進む。
【００５３】
形式検証で検証してないないモジュールがあるときには、ＲＴＬ４００の中で形式検証において未検証のモジュールを探し、そのモジュールを検証対象モジュールとし、また、そのモジュールに対応するアサーションを形式検証プログラムＡＳＥにする（Ｓ２０５）。なお、図７のＮＥＸＴ＿ＭＯＤ（）は、引数のモジュールの次のモジュールを返す関数、ＮＥＸＴ＿ＡＳＥ（）は、引数のアサーションの次のアサーションを返す関数とする。
【００５４】
すべてのモジュールを形式検証で検証した場合には、各ＲＴＬ４００に対する形式検証の証明の結果を証明結果６３０として出力する。また、各ＲＴＬ４００の全体の行数に対して証明された行数をラインカバレッジ５２０として出力する。証明結果６３０の付随情報として、未証明の行の情報等も含めて出力する。
【００５５】
次に、図９を用いてダイナミック検証装置によるダイナミック検証の処理について説明する。
これは、図７におけるＳ３００の処理である。
浮動小数点数演算器のＲＴＬ４００を動作させるために、ＲＴＬ４００を論理シミュレータ２３０にセットする（Ｓ３０１）。必要に応じて論理合成をおこなう。
【００５６】
次に、中間値指向のダイナミック検証をおこなう（Ｓ４００）。中間値指向のダイナミック検証においては、照合結果６２０と中間値カバレッジ５００を出力する。なお、詳細は後述する。
【００５７】
次に、例外発生境界指向のダイナミック検証をおこなう（Ｓ５００）。例外発生境界指向のダイナミック検証においては、照合結果６２０と例外発生境界カバレッジを出力する。なお、浮動小数点数演算器の実行する演算の内容が加算か乗算か除算かによって、検査すべき境界の種類が異なる。なお、詳細は後述する。
次に、完全乱数によるダイナミック検証をおこなう（Ｓ９００）。完全乱数によるダイナミック検証においては、照合結果６２０のみを出力する。なお、詳細は後述する。
【００５８】
次に、図１０を用いて中間値指向のダイナミック検証の実行イメージを示す図である。
中間値指向のダイナミック検証とは、検証の対象となる浮動小数点数演算器のＲＴＬ４００により、論理シミュレータ２３０を実行させたときのモジュールにおける中間ポートの中間値の着目したダイナミック検証である
以下では、図１０に示されるような浮動小数点数加算器を例にとって説明する。この場合は、浮動小数点数加算器において、桁落ちが発生する演算特殊ケースを重点的に検証する目的で、ＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯの中間ポートを指定してダイナミック検証をおこなうものとする。
【００５９】
桁落ちとは、二つの入力の値が非常に近い場合で、かつ実質減算の場合に発生する浮動小数点数加算器の特殊ケースである。例えば、入力値の値が下記のような値の場合である。
ＩＮＰＵＴ＿１＝（−１）＾０＊２＾９＊１．０１１１００１０１０１１１０１１０１１１０００２
ＩＮＰＵＴ＿２＝（−１）＾１＊２＾９＊１．０１１１０００１１１１０１１００１０１１０１０２
【００６０】
ここで、ａ＾ｂは、ａのｂ乗を表し、インデックスの２は、２進数であることを示している。この場合に、ほぼ同じ大きさの値の引き算のため互い打ち消し合い、非常に小さい値が出力されることとなる。このとき、浮動小数点の位置が大きく変化するため特殊な処理が必要となる。特殊な処理をおこなうモジュールが図中のモジュールＸであり、この桁落ちが発生する場合に活性化する中間ポートがＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯポートである。例えば、ＩＮＰＵＴ＿１、ＩＮＰＵＴ＿２が上記の値のときに、仮数部の「１．０１１１００１０１０１１１０１１０１１１０００２」と「１．０１１１０００１１１１０１１００１０１１０１０２」が直接引き算されることでモジュールＸの入力値は下記のようになる。
ＳＵＭＭＡＴＩＯＮ＝０００００００００１１００１１１０１０１１１１０２
【００６１】
この上位ビットに並ぶ０の数を数えて、その数をＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯポートから出力する。
ＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯ＝０１００１２
これはすなわち、１０進数では９である。ＦＲＡＣはＳＵＭＭＡＴＩＯＮをＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯだけ左シフトした値となる。この例では、
ＦＲＡＣ＝１１００１１１０１０１１１１００００００００００２
となり、最終的なＯＵＴＰＵＴの値は、
ＯＵＴＰＵＴ＝（−１）＾０＊２＾０＊１．１００１１１０１０１１１１００００００００００２
である。
【００６２】
この桁落ちが発生する場合に、浮動小数点数加算器で特徴的に発火するポートは、ＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯである。このため、桁落ちの演算特殊ケースを重点的に検証したい場合には、ＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯが網羅的になるように入力値をうまく生成し、実際にＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯの値を、中間値として取得し網羅できているかを確認しながら検証を進めることにより、浮動小数点数加算器の演算の信頼性を高めようというのが、中間値指向のダイナミック検証の基本的なアイデアである。
【００６３】
また、本実施形態でいう不足中間値とは、検査対象ポート（ここでは、ＮＵＭ＿ＬＥＡＤＩＮＧ＿ＺＥＲＯであり、そのとりうる値は、２＾６ある）において、検証していない中間値を意味する。
【００６４】
次に、図１１を用いて中間値指向のダイナミック検証処理について説明する。
これは、図９におけるＳ４００の処理である。
先ず、検査対象ポートリスト８００から未検査のポートを一つ選択し、検査対象ポートとする（Ｓ４０１）。
【００６５】
次に、検査対象ポートの中間値について網羅的な検証をおこなう処理を実行する（Ｓ６００）。
検査対象ポートすべてについて、網羅率の検査が完了しているか否かを判定し（Ｓ４０２）、完了している場合には（Ｓ４０２：ＹＥＳ）、Ｓ４０３に進み、そうでない場合には（Ｓ４０２：ＮＯ）、Ｓ４０１に進む。
【００６６】
検査対象ポートすべてについて、網羅率の検査が完了して場合には、照合結果６２０を出力し、また、検査が完了した検査対象ポートの網羅率を中間値カバレッジ５００として出力する（Ｓ４０３）。
【００６７】
次に、図１２を用いて検査対象ポートの中間値について網羅的な検証をおこなう処理について説明する。
これは、図１１のＳ６００の処理である。
先ず、変数ｉを０で初期化する（Ｓ６０１）。
次に、入力値Ｘ１とＸ２を乱数で生成し、高信頼モデル２２０と論理シミュレータ２３０のそれぞれに入力し、それぞれ期待値７１０と出力値７２０を得る。高信頼モデル２２０から得た期待値ＹＥと論理シミュレータ２３０から得た出力値ＹＯと検査対象ポートの中間値ＩＶを計測部２４０に入力し、内部の検証ログ７８０と中間値ログ７６０に保存する（Ｓ６０２）。
【００６８】
次に、予め定まった検証サンプル数のＮ回と変数ｉを比較し（Ｓ６０３）、ｉが小さいならＳ６０４に進み、そうでないならＳ６０５に進む。
【００６９】
ｉがＮより小さいときには、変数ｉに１を加算して変数ｉに保存し（Ｓ６０４）、Ｓ６０２に進む。
ｉがＮと等しくなったときに、検査対象ポートの値の取りうる値の範囲を算出する。その中で中間値ログ７６０に存在しない未記録の中間値を割り出し、それらすべてを不足中間値として、不足中間値リスト７４０に登録する（Ｓ６０５）。
【００７０】
次に、不足中間値リスト７４０から未調査の不足中間値を一つ選択し、検査対象の不足中間値として登録しておく（Ｓ６０６）。
次に、検査対象の不足中間値についての検証の処理を実行する（Ｓ７００）。
次に、不足中間値リストに登録されているすべての不足中間値について検証が完了したか否かを判定し（Ｓ６０７）、検証が完了している場合には（Ｓ６０７：ＹＥＳ）、処理を終了し、検証が完了していない場合には（Ｓ６０７：ＮＯ）、Ｓ６０６に進む。
【００７１】
次に、図１３を用いて検査対象の不足中間値についての検証の処理について説明する。
先ず、ポート情報とポートの値のリストの組を持つデータ（ポート情報、値リスト）のリストのデータ構造を定義し、そのデータ構造を持つ変数ＬＩＳＴに、｛（検査対象ポート，｛不足中間値｝）｝を代入する（Ｓ７０１）。
【００７２】
次に、Ｓ７０２とＳ７０３では、Ｓ７０１のＬＩＳＴの検査対象ポートの不足中間値に到達しうる値を探索する。
先ず、ＬＩＳＴから要素を一つ取り出し、それをＣＵＲとする。ＬＩＳＴからＣＵＲを取り除いた状態にする。ＰＯにＣＵＲのポートをセットし、ＶＯＬＩＳＴにＣＵＲの値リストをセットする。ＰＯを出力ポートとするモジュールに対応する関数を、ＬＩＢ４１０からロードし、その関数の入力ポートを参照する。入力ポートがＮ本あった場合にはそれぞれに対応するＮ個のポート情報ＰＩｘ（０≦ｘ＜Ｎ）とＮ個の空のデータ入力値リストＶＩＬＩＳＴｘ＝｛｝を用意する（Ｓ７０２）。
【００７３】
次に、これら関数の入力ポートの取りうる値すべてを関数に入力する。関数の出力ポートＰＯの値が、ＶＬＩＳＴに存在する値と一致した場合に、そのときのＰＩｘの値ＶＩｘをＶＩＬＩＳＴｘに記録する（Ｓ７０３）。図１３のａｐｐｅｎｄに関する式は、第一引数のＶＩＬＩＳＴｘのリストの最後に、第二引数のＶＩｘの値を付け加え、それを新たなＶＩＬＩＳＴｘとすることを意味している。
【００７４】
次に、全入力ポートＰＩｘに対して、ＶＬＩＳＴｘが空であるか否かを判定し（Ｓ７０４）、Ｓ７０３でＶＬＩＳＴｘに値が記録されず、ＶＬＩＳＴｘが空のままであった場合には（Ｓ７０４：ＹＥＳ）、Ｓ７０５に進み、そうでない場合には（Ｓ７０４：ＮＯ）、Ｓ７０６に進む。
【００７５】
ＶＬＩＳＴｘに値が記録されず、ＶＬＩＳＴｘが空のままのときには、検査対象の不足中間値は取りうる値の範囲になかったと判定する（Ｓ７０５）。
ＶＬＩＳＴｘに値が記録されているときには、すべての入力ポートＰＩｘについて、｛ＰＩｘ，ＶＩＬＩＳＴｘ｝をＬＩＳＴに追加する（Ｓ７０６）。
【００７６】
次に、ＬＩＳＴ中に演算器の入力ポートＩＮＰＵＴ＿１、ＩＮＰＵＴ＿２の両方が存在するか否かを判定し（Ｓ７０７）、ＬＩＳＴ中に演算器の入力ポートＩＮＰＵＴ＿１、ＩＮＰＵＴ＿２の両方が存在する場合には（Ｓ７０７：ＹＥＳ）、Ｓ７０８に進み、そうでない場合には（Ｓ７０７：ＮＯ）、Ｓ７０２に進む。
【００７７】
そして、ＬＩＳＴに保存されているＩＮＰＵＴ＿１の取りうる値とＩＮＰＵＴ＿２の取りうる値の組を１個以上選択し、高信頼モデル２２０と論理シミュレータ２３０それぞれに入力し、照合結果６２０を取得する（Ｓ７０８）。
【００７８】
次に、図１４ないし図２０を用いて例外発生境界指向のダイナミック検証の処理について説明する。
例外発生境界指向のダイナミック検証とは、入力値に対して、例外が発生するか否かの境界に着目して、検証をおこなう手法である。以下では、検証の対象とする浮動小数点数演算器が加算器の場合、乗算器の場合、除算器の場合の例に分けて説明する。これは、図９のＳ５００の処理である。
【００７９】
先ず、図１４ないし図１６を用いて検証の対象とする浮動小数点数演算器が加算器の場合の例外発生境界指向のダイナミック検証の処理について説明する。
図１４には、加算器がオーバーフローする境界が示されている。図中のＭＡＸは、検証の対象とする浮動小数点数演算器が取り扱える浮動小数点数で表現可能な絶対値最大値の値を示している。ＥＰＳは、（１＋ＥＰＳ）が１を超える最小の数を示している。そして、浮動小数点数演算器が取り扱う浮動小数点数で表現可能な値は、格子上の離散値として表現される。この格子の間隔は一定ではなく、比にして表現すると、１，（１＋ＥＰＳ），（１＋ＥＰＳ）＾２と値が大きくなるにつれて徐々に大きくなる。加算器がオーバーフローしないＸ１とＸ２の領域は、−ＭＡＸ≦Ｘ１＋Ｘ２≦ＭＡＸであり、この領域内の格子上の点（Ｘ１，Ｘ２）を○で示している。これとは、逆に加算器がオーバーフローする領域はＸ１＋Ｘ２＜−ＭＡＸとＸ１＋Ｘ２＞ＭＡＸであり、この領域に存在する格子上の点（Ｘ１，Ｘ２）を×で示している。本実施形態の例外発生境界指向のダイナミック検証は、こうした境界に隣接する格子上の点を検証対象とするものである。
【００８０】
先ず、検証対象の浮動小数点数演算器の種類が加算器である場合の例外発生境界指向のダイナミック検証の処理では、調査する境界値の初期値のＸ１座標を設定する（Ｓ５０１）。加算器の場合は、ＭＡＸ＊ＥＰＳを初期値として、設定する。
【００８１】
次に、高信頼モデル２２０を用いた演算で、Ｘ１の値から、第一象限の境界線：Ｘ１＋Ｘ２＝ＭＡＸのＸ２の値Ｘ２＿Ｐ＝ＭＡＸ−Ｘ１と第三象限の境界線：Ｘ１＋Ｘ２＝−ＭＡＸのＸ２の値Ｘ２＿Ｍ＝（−１）＊ＭＡＸ＋Ｘ１の値を求める（Ｓ５０２）。
【００８２】
次に、座標（Ｘ１，Ｘ２＿Ｐ）周辺の境界探索と照合処理をおこなう（Ｓ８００ａ）。
次に、座標（Ｘ１，Ｘ２＿Ｍ）周辺の境界探索と照合処理フローをおこなう（Ｓ８００ｂ）。
【００８３】
そして、Ｘ１がＭＡＸより小さいか判定し（Ｓ５０３）、Ｘ１がＭＡＸより小さい場合には（Ｓ５０３：ＹＥＳ）、Ｓ５０４に進み、そうでない場合には（Ｓ５０３：ＹＥＳ）、処理を終了する。
Ｘ１がＭＡＸより小さい場合には、Ｘ１に、Ｘ１＊（１＋ＥＰＳ）を代入する（Ｓ５０４）。すなわち、Ｘ１の値を、Ｘ１の隣の点の値に更新する。そして、Ｓ５０２に進む。
【００８４】
次に、図１６を用いて（Ｘ１，Ｘ２）周辺の境界探索と照合の処理を説明する。
これは、図１５のＳ８００ａ、Ｓ８００ｂに該当する処理である。また、後の乗算器の場合の処理の図１８のＳ８００ｃ〜Ｓ８００ｆ、除算器の場合の処理の図２０のＳ８００ｇ〜Ｓ８００ｋにもサブルーチンとして用いられる。
【００８５】
本実施形態の処理では、予め境界の式によって境界上に存在する格子点（Ｘ１，Ｘ２）を求めるが、丸め誤差などにより真の境界値から若干のずれが生じることを考慮し、高信頼モデルを用いて調査すべき格子点が境界の周辺であることを確かめてから照合をおこなう。
【００８６】
先ず、境界値か否かを調査すべき点を５点に絞り、照合をおこなう（Ｓ８０１）。事前に数式で境界のおおよその位置が判明しているので、５点程度を調べればよい。Ｘ２を中心とする隣接５点をＸ２＿０〜Ｘ２＿４に設定する。すなわち、順に、Ｘ２＿０＊（１＋ＥＰＳ）＾２＝Ｘ２，Ｘ２＿１＊（１＋ＥＰＳ）＝Ｘ２，Ｘ２＿２＝Ｘ２，Ｘ２＿３＝Ｘ２＊（１＋ＥＰＳ），Ｘ２＿４＝Ｘ２＊（１＋ＥＰＳ）＾２になるように、それぞれＸ２＿０〜Ｘ２＿４を定める。
【００８７】
次に、ループ変数ｉを０で初期化する（Ｓ８０２）。
次に、高信頼モデル２２０を用いて、期待値ＹＥ＿Ａ＝Ｘ  ｏｐ  Ｘ２＿ｉと、ＹＥ＿Ｂ＝Ｘ  ｏｐ  Ｘ２＿｛ｉ＋１｝を計算する（Ｓ８０３）。ここで、Ｘ２＿ｉ、Ｘ２＿｛ｉ＋１｝は、ｉに応じて、可変な変数名になっていることに留意する。また、ｏｐは、二項演算子であり、検証対象の浮動小数点数の演算の種類が加算なら、ｏｐ＝＋、乗算なら、ｏｐ＝＊、除算なら、ｏｐ＝／である。
【００８８】
次に、ＹＥ＿Ａを求める演算で例外が発生およびＹＥ＿Ｂを求める演算どちらかで例外が発生しない、または、ＹＥ＿Ａを求める演算で例外が発生しないおよびＹＥ＿Ｂを求める演算どちらかで例外が発生したかを判定し（Ｓ８０４）、いずれかの演算で例外が発生している場合には（Ｓ８０４：ＹＥＳ）、Ｓ８０５に進み、そうでない場合には（Ｓ８０４：ＮＯ）、Ｓ８０６に進む。
【００８９】
ＹＥ＿Ａを求める演算、ＹＥ＿Ｂを求める演算のいずれかで例外が発生している場合には、論理シミュレータ２３０を用いて、出力値ＹＯ＿Ａ＝Ｘ  ｏｐ  Ｘ２＿ｉと、ＹＯ＿Ｂ＝Ｘ  ｏｐ  Ｘ２＿｛ｉ＋１｝を計算する（Ｓ８０５）。
ＹＥ＿Ａを求める演算、ＹＥ＿Ｂを求める演算のいずれかで例外が発生していない場合には、ループ変数ｉをｉ＋１で更新する（Ｓ８０６）。そして、Ｓ８０３に進む。
最後に、ＹＥ＿ＡとＹＯ＿Ａ、ＹＥ＿ＢとＹＯ＿Ｂをそれぞれ比較する（Ｓ８０６）。
【００９０】
次に、図１７および図１８を用いて検証の対象とする浮動小数点数演算器が乗算器の場合の例外発生境界指向のダイナミック検証の処理について説明する。
図１７には、乗算器がオーバーフローする境界が示されている。乗算器がオーバーフローしないＸ１とＸ２の領域は、−ＭＡＸ≦Ｘ１＊Ｘ２≦ＭＡＸであり、この領域内の格子上の点（Ｘ１，Ｘ２）を○で示している。これとは、逆に乗算器がオーバーフローする領域はＸ１＊Ｘ２＜ＭＡＸ，Ｘ１＊Ｘ２＞−ＭＡＸであり、この領域に存在する格子上の点（Ｘ１，Ｘ２）を×で示している。
【００９１】
先ず、検証対象の浮動小数点数演算器の種類が乗算器である場合の例外発生境界指向のダイナミック検証の処理では、調査する境界値の初期値のＸ１座標を設定する（Ｓ５１０）。乗算器の場合は、１を初期値として設定する。
【００９２】
次に、Ｘ１の値から、第一象限と第二象限の境界線のＸ２の値Ｘ２＿Ｐ＝ＭＡＸ／Ｘ１と第三象限と第四象限の境界線のＸ２の値Ｘ２＿Ｍ＝（−１）＊ＭＡＸ／Ｘ１の値を求める（Ｓ５１１）。
【００９３】
次に、座標（Ｘ１，Ｘ２＿Ｐ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｃ）。
次に、座標（Ｘ１，Ｘ２＿Ｍ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｄ）。
次に、座標（（−１）＊Ｘ１，Ｘ２＿Ｐ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｅ）。
次に、座標（（−１）＊Ｘ１，Ｘ２＿Ｍ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｆ）。
【００９４】
次に、Ｘ１がＭＡＸより小さいか否かを判定し（Ｓ５１２）、Ｘ１がＭＡＸより小さい場合には（Ｓ５１２：ＹＥＳ）、Ｓ５１３に進み、そうでない場合には（Ｓ５１２：ＮＯ）、処理を終了する。
【００９５】
Ｘ１がＭＡＸより小さい場合には、  Ｘ１に、Ｘ１＊（１＋ＥＰＳ）を代入する（Ｓ５１３）。すなわち、Ｘ１の値を、隣の点の値に更新する。そして、Ｓ５１１に進む。
【００９６】
次に、図１９および図２０を用いて検証の対象とする浮動小数点数演算器が除算器の場合の例外発生境界指向のダイナミック検証の処理について説明する。
図１９には、除算器がオーバーフローする境界が示されている。除算器がオーバーフローしないＸ１とＸ２の領域は、−ＭＡＸ≦Ｘ１／Ｘ２≦ＭＡＸであり、この領域内の格子上の点（Ｘ１，Ｘ２）を、○で示している。これとは逆に除算器がオーバーフローする領域は、Ｘ１／Ｘ２＜ＭＡＸ，Ｘ１／Ｘ２＞−ＭＡＸであり、この領域に存在する格子上の点（Ｘ１，Ｘ２）を×で示している。
【００９７】
先ず、検証対象の浮動小数点数演算器の種類が除算器である場合の例外発生境界指向のダイナミック検証の処理では、座標（０，０）周辺の境界探索と照合処理をおこなう（Ｓ８００ｇ）。
【００９８】
次に、調査する境界値の初期値のＸ１座標を設定する（Ｓ５２０）。除算器の場合は、ＭＩＮを初期値とする。ＭＩＮとは、検証する浮動小数点数演算器における浮動小数点数で表現される最小の正の整数である。
【００９９】
次に、Ｘ１の値から、第一象限と第二象限の境界線のＸ２の値Ｘ２＿Ｐ＝Ｘ１／ＭＡＸと、第三象限と第四象限の境界線のＸ２の値Ｘ２＿Ｍ＝（−１）＊Ｘ１／ＭＡＸの値を求める（Ｓ５２１）。
【０１００】
次に、座標（Ｘ１，Ｘ２＿Ｐ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｈ）。
次に、座標（Ｘ１，Ｘ２＿Ｍ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｉ）。
次に、座標（（−１）＊Ｘ１，Ｘ２＿Ｐ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｊ）。
次に、座標（（−１）＊Ｘ１，Ｘ２＿Ｍ）周辺の境界探索と照合処理をおこなう（Ｓ８００ｋ）。
【０１０１】
次に、Ｘ１がＭＡＸより小さいか否かを判定し（Ｓ５２２）、Ｘ１がＭＡＸより小さい場合には（Ｓ５２２：ＹＥＳ）、Ｓ５２３に進み、そうでない場合には（Ｓ５２２：ＮＯ）、処理を終了する。
Ｘ１がＭＡＸより小さい場合には、Ｘ１に、Ｘ１＊（１＋ＥＰＳ）を代入する（Ｓ５２３）。すなわちＸ１の値を、隣の点の値で更新する。そして、Ｓ５２１に進む。
【０１０２】
次に、図２１を用いて完全乱数によるダイナミック検証の処理を説明する。
これは、図９のＳ９００の処理である。
完全乱数によるダイナミック検証の処理は、上述の中間値指向のダイナミック検証や例外発生境界指向のダイナミック検証とは異なり、特定の値に着目することなく、完全に乱数により発生した値を、高信頼モデル２２０と論理シミュレータ２３０への入力として、それぞれが出力する期待値７１０、出力値７２０を比較して、検証する処理である。
完全乱数によるダイナミック検証では、先ず、ループ変数ｉを０で初期化する（Ｓ９０１）。
【０１０３】
次に、乱数を用いて入力値Ｘ１，Ｘ２を生成する。高信頼モデル２２０と論理シミュレータ２３０に、それぞれＸ１とＸ２を入力し、それぞれから出力される期待値ＹＥと出力値ＹＯを照合する（Ｓ９０２）。
次に、ループ変数ｉと規定の検証回数Ｎを比較し（Ｓ９０３）、ｉ＜Ｎの場合には（Ｓ９０３：ＹＥＳ）、Ｓ９０４に進み，そうでない場合には（Ｓ９０２：ＮＯ）、処理を終了する。
次に、ｉ＜Ｎの場合には、ループ変数ｉをｉ＋１で更新し（Ｓ９０４）、Ｓ９０２に進む。
【符号の説明】
【０１０４】
１００…浮動小数点数演算器の検証装置、１１０…制御部、２００…形式検証装置、３００…ダイナミック検証装置、１２０…検証結果集約部、
４００…ＲＴＬ、４１０…ＬＩＢ、４２０…ＳＶＡ、
５００…中間値カバレッジ、５１０…例外発生境界カバレッジ、５２０…ラインカバレッジ、
６００…検証結果、６１０…総合カバレッジ、６１１…詳細情報、６２０…照合結果、６３０…証明結果、
７００…入力値、７１０…期待値、７２０…出力値、７３０…中間値、７４０…不足中間値リスト、７５０…不足中間値、７６０…中間値ログ、７７０…検証サンプル、７８０…検証ログ、
８００…検査対象ポートリスト、８１０ポート情報
【図１】
2019185301.tif 000003
【図２】
2019185301.tif 000004
【図３】
2019185301.tif 000005
【図４】
2019185301.tif 000006
【図５】
2019185301.tif 000007
【図６】
2019185301.tif 000008
【図７】
2019185301.tif 000009
【図８】
2019185301.tif 000010
【図９】
2019185301.tif 000011
【図１０】
2019185301.tif 000012
【図１１】
2019185301.tif 000013
【図１２】
2019185301.tif 000014
【図１３】
2019185301.tif 000015
【図１４】
2019185301.tif 000016
【図１５】
2019185301.tif 000017
【図１６】
2019185301.tif 000018
【図１７】
2019185301.tif 000019
【図１８】
2019185301.tif 000020
【図１９】
2019185301.tif 000021
【図２０】
2019185301.tif 000022
【図２１】
2019185301.tif 000023