(57)【要約】【課題】ファームウェアの検証に要する時間及び資源を低減する。【解決手段】ハードウェアに係る状態遷移情報及びレジスタ情報、及びファームウェアに基づいて、内部状態を更新する内部状態管理部と、内部状態管理部で更新された内部状態と、入力されるハードウェアの制約条件を比較して、ハードウェア制約違反を検出する制約違反検出部とを設けるようにして、ハードウェアを用いずに検証を行ってハードウェア制約違反を検出可能にし、ファームウェアの検証に要する時間及び資源を低減できるようにする。【選択図】図１
2008102627.tif 000002
【特許請求の範囲】
【請求項１】
入力されるハードウェアに係る状態遷移情報及びレジスタ情報、及びファームウェアに基づいて、内部状態を更新する内部状態管理部と、
上記内部状態管理部により更新された内部状態と、入力されるハードウェアの制約条件に基づいて、上記ファームウェアにおけるハードウェア制約違反を検出する制約違反検出部とを備えることを特徴とする検査装置。
【請求項２】
入力される上記ファームウェアをグラフ化した動作データベースを作成するデータベース変換部をさらに備え、
上記内部状態管理部は、上記状態遷移情報、上記レジスタ情報、及び上記データベース変換部により作成された動作データベースに基づいて、内部状態を更新することを特徴とする請求項１記載の検査装置。
【請求項３】
上記制約違反検出部は、上記内部状態管理部により更新された内部状態と、上記ハードウェアの制約条件とを比較し、上記内部状態が上記制約条件に違反しているか否かを判定する判定部を備えることを特徴とする請求項１記載の検査装置。
【請求項４】
上記制約条件には、上記ハードウェア制約違反を検出した場合の修正方法が合わせて記述されており、上記制約違反検出部にて上記ハードウェア制約違反を検出した場合には、上記修正方法に基づいて内部状態を修正して処理を継続することを特徴とする請求項１記載の検査装置。
【請求項５】
ハードウェアに係るレジスタ情報及び制約条件一覧が入力され、上記制約条件一覧に示される制約条件を解析し、レジスタ情報に示されるレジスタ毎に課されている制約を分類し出力することを特徴とする制約条件解析支援装置。
【請求項６】
ハードウェアに依存しない複数の制約タイプで構成される制約タイプ知識を有し、当該制約タイプ知識を参照してレジスタに課されている制約を分類することを特徴とする請求項５記載の制約条件解析支援装置。
【請求項７】
請求項１記載の検査装置と、請求項５記載の制約条件解析支援装置とを備えることを特徴とするデバッグシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ファームウェアにおける不具合を検出するための検証技術に関する。
【背景技術】
【０００２】
ハードウェアとソフトウェアが協調して、画像変換処理などの１つの処理を実行する場合、ハードウェアに不具合がなくてもソフトウェアに不具合があると、異常動作が発生したり、システムが停止したりする。特に、ハードウェアを制御するソフトウェア（ファームウェア）は、ハードウェアの予め決められた制約に違反することなくハードウェアを制御する必要がある。しかし、近年のハードウェアの高機能化や複雑化に伴って、人手による検査ではファームウェアの不具合を検出することが困難になってきている。
【０００３】
図１３は、ファームウェアのハードウェア制約違反の検出及び修正を行うための従来のファームウェア検証の流れを示す図である。
まず、仕様書１０１に基づいて、ファームウェア１０２及びハードウェア１０３が作成される。作成されたファームウェア１０２やハードウェア１０３を用いて、シミュレーション、実機検証１０４が行われる。
【０００４】
そこで、異常動作やシステム停止（フリーズ）などの不具合が発見された場合には（１０５）、原因解析１０６が行われ、解析結果に応じて仕様書１０１やファームウェア１０２が修正される。そして、修正後のファームウェア１０２やハードウェア１０３を用いて、再度、シミュレーション、実機検証１０４が行われる。不具合が発見されなくなるまで、上述した動作が繰り返し行われる。
【０００５】
入力された設計データのメッセージシーケンスデータからレジスタデータを抽出し、ハードウェア設計におけるレジスタ抽出とコード化をグラフィカルな入力と自動化により容易に行うことができるハードウェア設計システムが提案されている（特許文献１参照。）。また、システムＬＳＩの機能テスト方法において、機能記述から機能テストを実施するための制御手順を自動生成し、仕様書からハードウェアの設定パターンを抽出し、制御手順と設定パターンを比較することにより仕様書に対する制御手順の整合性を検証する方法が提案されている（特許文献２参照。）。
【０００６】
【特許文献１】特開２００５−３２７１９２号公報
【特許文献２】特開２００５−９２５９８号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
ファームウェアやハードウェアの作成に使用する仕様書において、ハードウェア制約の記載が漏れていることがあり、また、記載されていない制約が存在するかをチェックすることができなかった。
【０００８】
また、従来、ファームウェア検証のためのシミュレーションや実機検証を行うには、実機又はエミュレータが必要であった。シミュレーションや実機検証で不具合が発見された場合には、原因解析を行うが、１つの不具合を解消するのに時間を要していた。すなわち、従来においては、シミュレーションや原因解析に多大な時間及び資源（シミュレータや実機）を要していた。
【０００９】
本発明は、ハードウェアを用いずに検証を行い、かつ不具合についての原因解析を不要にし、ファームウェアの検証に要する時間及び資源を低減することを目的とする。
【課題を解決するための手段】
【００１０】
本発明の検査装置は、ハードウェアに係る状態遷移情報及びレジスタ情報、及びファームウェアに基づいて、内部状態を更新する内部状態管理部と、更新された内部状態と、入力されるハードウェアの制約条件に基づいて、ファームウェアにおけるハードウェア制約違反を検出する制約違反検出部とを備えることを特徴とする。
また、本発明の制約条件解析支援装置は、入力される制約条件一覧に示される制約条件を解析し、ハードウェアに係るレジスタ情報に示されるレジスタ毎に課されている制約を分類し出力することを特徴とする。
【発明の効果】
【００１１】
本発明によれば、シミュレータや実機等のハードウェアを用いずに、ファームウェアにおけるハードウェア制約条件の違反を検出でき、ファームウェアの検証に要する時間及び資源を低減することができる。
【発明を実施するための最良の形態】
【００１２】
以下、本発明の実施形態を図面に基づいて説明する。
図１は、本発明の一実施形態によるデバッグシステムの構成例を示す図である。
本実施形態におけるデバッグシステム１は、検査装置１０及びマッピング装置２０を有する。
【００１３】
（検査装置１０）
検査装置１０は、ファームウェア２、状態遷移図４、アドレスマップ５、及び制約条件表７が入力され、ファームウェアのハードウェア制約違反を機械的に検査する。検査装置１０は、入力部１１、データベース変換部１２、内部状態管理部１３、制約チェック部１４、及び出力部１６を有する。
【００１４】
入力部１１は、外部から入力されるファームウェア２、状態遷移図（状態遷移情報）４、アドレスマップ（レジスタ情報）５、及び制約条件表７を受ける。制約条件表７、アドレスマップ５、及び状態遷移図４の一例を、図２、図３、図４にそれぞれ示す。
【００１５】
図２は、制約条件表７の一例を示す図である。制約条件表７は、ハードウェアの制約条件を表にまとめたものであり、仕様書３に記載されているハードウェアの制約条件６に基づいて作成される。
【００１６】
制約条件表７において、項目ａ、ｂには、項目ｃ〜ｅにより規定される制約条件をチェックする期間が記述される。項目ａ、ｂの記載には、以下の組み合わせでの記述が可能である。
（１−１）項目ａ−「常に」、項目ｂ−空白
（１−２）項目ａ−「終了時に」、項目ｂ−空白
（１−３）項目ａ−状態値の条件式又はレジスタ値の条件式、項目ｂ−空白
（１−４）項目ａ−レジスタ名及び値、項目ｂ−「書き込んだとき」又は「書き換えたとき」
（１−５）項目ａ−レジスタ名、項目ｂ−「読み出したとき」
【００１７】
また、項目ｃ、ｄには、チェックする制約条件の内容が記述される。項目ｃ、ｄの記述には、以下の組み合わせでの記載が可能である。
（２−１）項目ｃ−状態値の条件式又はレジスタ値の条件式、項目ｄ−空白
（２−２）項目ｃ−レジスタ名及び値、項目ｄ−「書き込み」又は「書き換え」
（２−３）項目ｃ−レジスタ名、項目ｄ−「読み出し」
【００１８】
また、項目ｅには、「は禁止です」又は「は必須です」が記述される。項目ｅに「は禁止です」と記述されている場合には、項目ｃ、ｄに記述された制約条件の内容が満たされたとき制約違反になる。また、項目ｅに「は必須です」と記述されている場合には、項目ｃ、ｄに記述された制約条件の内容が満たされていないとき制約違反になる。
ここで、本実施形態において、書き換え禁止の場合には同じ値を書き込むことは許容され、書き込み禁止の場合には同じ値を書き込むことも禁止される。
【００１９】
図３は、アドレスマップ５の一例を示す図である。アドレスマップ５は、仕様書３に記載されているレジスタに係る記載をそのまま取得し作成される。アドレスマップ５には、図３に示すように、レジスタ名、アドレス、フィールド名、ビット位置、初期値、及びビット幅を含むレジスタ情報が示されている。
【００２０】
図４は、状態遷移図４の一例を示す図である。図４には、停止状態において遷移条件Ａを満足すると待機状態に遷移し、待機状態において遷移条件Ｂ、遷移条件Ｃを満足するとそれぞれ起動状態、停止状態に遷移し、起動状態において遷移条件Ｄを満足すると待機状態に遷移する場合を一例として示している。
【００２１】
図１に戻り、データベース変換部１２は、入力部１１を介して入力されるファームウェア２をグラフ化した動作データベースに変換する。例えば、データベース変換部１２は、Ｃコンパイラの技術を用いて、ファームウェア２をレジスタについての読み書き部分のみを残した動作データベースに変換する。
【００２２】
図５は、データベース変換部１２により変換して得られる動作データベースの一例を示す図である。図５においては、以下のようなファームウェア２を変換して得られる動作データベースを示している。
【００２３】
アドレス値ａｄｒ１にデータｄａｔａ１を書き込み（Ｐ１）、アドレス値ａｄｒ２からデータを読み出し、読み出したデータがデータｄａｔａ２であれば（Ｐ２）、アドレス値ａｄｒ３にデータｄａｔａ３を書き込み（Ｐ１）、終了する。アドレス値ａｄｒ２から読み出したデータがデータｄａｔａ２でない場合には（Ｐ２）、それが５回目のときのみ（Ｐ４）アドレス値ａｄｒ４にデータｄａｔａ４を書き込んで（Ｐ５）、アドレス値ａｄｒ２からデータを読み出し（Ｐ２）を行う。
【００２４】
内部状態管理部１３は、状態遷移図の位置、動作データベースの位置、及びレジスタ値からなる内部状態を管理する。内部状態管理部１３は、逐次的に内部状態を更新するとともに、その内部状態を記憶している。
【００２５】
制約チェック部１４は、判定部１５を有し、内部状態が制約条件表７に記載されているハードウェアの制約条件に違反していないかをチェックし、違反があった場合には、その違反箇所及び内容を出力する。判定部１５は、内部状態管理部１３にて管理されている内部状態を参照し、内部状態がハードウェアの制約条件に違反しているか否かを判定する。
【００２６】
出力部１６は、制約チェック部１４から出力されるハードウェア制約違反の違反箇所及び内容などのファームウェア検証結果を出力する。
【００２７】
次に、検査装置１０の動作について説明する。
図６は、検査装置１０の動作を示すフローチャートである。
【００２８】
まず、ファームウェア２、状態遷移図（状態データベース）４、アドレスマップ５、及び制約条件表７が入力部１１を介して入力され、入力されたファームウェア２がデータベース変換部１２にて動作データベースに変換される。そして、これら状態遷移図４、アドレスマップ５、制約条件表７、及び動作データベースが、内部状態管理部１３及び制約チェック部１４に読み込まれる（Ｓ１１）。
【００２９】
次に、内部状態管理部１３は、状態遷移図の位置、動作データベースの位置、及びレジスタ値からなる内部状態を更新する（Ｓ１２）。具体的には、内部状態の更新は、下記の手順（１）〜（３）からなり、手順（１）、手順（２）、手順（３）の順番で行われる。
（１）動作データベースの現在位置を１つ進める。
（２）動作データベースの現在位置の動作を見てレジスタ値を更新する。
（３）動作データベースの現在位置の動作が状態遷移条件に適合する場合には、状態遷移図の位置を変更する。
【００３０】
次に、制約チェック部１４は、更新された内部状態を参照し、制約条件表７に基づいてハードウェア制約違反の有無をチェックする（Ｓ１３）。このステップＳ１３における制約チェック処理の詳細については後述する。
【００３１】
ステップＳ１３での制約チェック処理の結果、制約違反があった場合には（Ｓ１４のあり）、制約チェック部１４は、違反箇所及び内容を出力部１５を介して出力して（Ｓ１８）、動作を終了する。一方、ステップＳ１３での制約チェック処理の結果、制約違反がない場合には（Ｓ１４のなし）、制約チェック部１４はその旨を内部状態管理部１３に通知する。通知を受けた内部状態管理部１３は、動作データベースの位置が最終位置であるか否かを判断する（Ｓ１５）。
【００３２】
その判断の結果、動作データベースの位置が最終位置でない場合には、ステップＳ１２に戻る。一方、動作データベースの位置が最終位置である場合には、制約チェック部１４は、制約条件表７に基づいて、終了時の内部状態がハードウェア制約条件に違反していないかをチェックする（Ｓ１６）。
【００３３】
ステップＳ１６での制約チェック処理の結果、制約違反があった場合には（Ｓ１７のあり）、制約チェック部１４は、違反箇所及び内容を出力部１５を介して出力して（Ｓ１８）、動作を終了する。一方、制約違反がない場合には（Ｓ１７のなし）、違反なし、つまりファームウェアに不具合がないとして、動作を終了する。
この図６に示した動作を、ハードウェア制約違反が検出されなくなるまで繰り返し実行することで、ファームウェアの不具合をすべて解消することができる。
【００３４】
図７は、図６に示したステップＳ１３、Ｓ１６において行われる制約チェック処理の流れを示すフローチャートである。
【００３５】
まず、ステップＳ２１にて、制約チェック部１４内の判定部１５は、制約条件表の１行目に記載されているハードウェアの制約条件を取り出す。
ステップＳ２２にて、判定部１５は、内部状態が項目ａ、ｂの記述に基づく制約条件のチェック期間を満たすか否かを判定する。その結果、内部状態がチェック期間を満たす場合にはステップＳ２３に進み、そうでない場合にはステップＳ２６に進む。
【００３６】
ステップＳ２３にて、判定部１５は、内部状態が項目ｃ、ｄの記述に基づく制約条件の内容を満たすか否かを判定する。その結果、内部状態が制約条件の内容を満たす場合にはステップＳ２４に進み、そうでない場合にはステップＳ２５に進む。
ステップＳ２４にて、判定部１５は、項目ｅの記述が「は禁止です」であるか否かを判定する。その結果、項目ｅの記述が「は禁止です」である場合には、内部状態が制約条件の内容を満たし、かつ項目ｅが「は禁止です」であるので、ハードウェア制約違反であると判定する。一方、項目ｅの記述が「は禁止です」でない場合には、ハードウェア制約違反でないと判定し、ステップＳ２６に進む。
【００３７】
ステップＳ２５にて、判定部１５は、項目ｅの記述が「は禁止です」であるか否かを判定する。その結果、項目ｅの記述が「は禁止です」でない場合には、内部状態が制約条件の内容を満たさず、かつ項目ｅが「は必須です」であるので、ハードウェア制約違反であると判定する。一方、項目ｅの記述が「は禁止です」である場合には、ハードウェア制約違反でないと判定し、ステップＳ２６に進む。
【００３８】
ステップＳ２６にて、制約条件表７に記載されているすべての制約条件についてチェックを行ったか否かを判定する。その結果、チェックを行っていない制約条件がある場合には、ステップＳ２７にて、判定部１５は、制約条件表７から次の制約条件を取り出し、ステップＳ２２に進む。一方、すべての制約条件についてチェックを行ったと判定した場合には、制約チェック処理を終了し、図６に示す動作に戻る。
【００３９】
図８を参照して、検査装置１０の動作例を具体的に説明する。
図８（ａ）に示す状態遷移図、（ｂ）に示す動作データベース、（ｃ）に示す制約条件表、（ｄ）に示すアドレスマップが取り込まれるものとする。また、以下の説明では、内部状態を（状態遷移図位置，動作データベースの位置，レジスタＷＩＤＴＨ．Ｘの値，レジスタＳＴＡＲＴ．ＥＮの値）により表す。
【００４０】
初期状態の内部状態は（Ｓ００，Ｐ１１，０，０）となる。Ｓ００，Ｐ１１は、状態遷移図の初期値（停止状態）、動作データベースの初期値、レジスタＷＩＤＴＨ．ＸとＳＴＡＲＴ．ＥＮの値は、アドレスマップの初期値「０」を設定する。ここで、制約チェック処理を行う。（Ｓ００，Ｐ１１，０，０）の内部状態は、制約条件表に示される制約条件の項目ａ（Ｓ０１）を満たさないので制約違反なしと判定される。
【００４１】
次に、内部状態を更新する。動作データベース位置がＰ１２に移動し、レジスタＷＩＤＴＨ．Ｘに値「６４０」が書き込まれる。状態遷移図の位置はＳ００からの遷移条件に当てはまらないのでＳ００のままになる。したがって、内部状態は（Ｓ００，Ｐ１２，０→６４０，０）となる。この内部状態で制約チェック処理を行う。（Ｓ００，Ｐ１２，０→６４０，０）の内部状態は、制約条件の項目ａ（Ｓ０１）を満たさないので制約違反なしと判定される。
【００４２】
続いて、内部状態を再び更新する。動作データベースの位置がＰ１３に移動し、レジスタＳＴＡＲＴ．ＥＮに値「１」が書き込まれる。状態遷移図の位置はＳ００→Ｓ０１の遷移条件に当てはまるのでＳ０１に遷移する。したがって、内部状態は（Ｓ００→Ｓ０１，Ｐ１３，６４０，０→１）となる。
【００４３】
ここで制約チェック処理を行う。このとき、制約条件の項目ａ（Ｓ０１）は満たす。しかし、項目ｃ、ｄの制約条件（レジスタＷＩＤＴＨ．Ｘの書き換え）は満たさず、かつ項目ｅが「は禁止です」であるので、制約違反なしと判定される。
【００４４】
次に、内部状態を再び更新する。動作データベースの位置がＰ１４に移動し、レジスタＷＩＤＴＨ．Ｘに値「２００」が書き込まれる。状態遷移図の位置は遷移条件を満たさないのでＳ０１のままである。したがって、内部状態は（Ｓ０１，Ｐ１４，６４０→２００，１）となる。ここで制約チェック処理を行うと、制約条件の項目ａ（Ｓ０１）を満たし、項目ｃ、ｄの制約条件（レジスタＷＩＤＴＨ．Ｘの書き換え）も満たし、かつ項目ｅが「は禁止です」であるので制約違反と判定される。検査装置１０は、Ｐ１４で起動状態中にレジスタＷＩＤＴＨ．Ｘを書き換えてはいけないという制約条件に違反していることを出力し動作を終了する。
【００４５】
以上、説明したように検査装置１０を用いてファームウェア検証を行うことにより、シミュレータや実機等のハードウェアを用いなくとも、ハードウェア制約条件の違反の有無を検査することができる。また、ハードウェア制約違反があっても、その違反箇所及び違反内容が検査装置１０から出力されるので原因解析を行う必要がなくファームウェアの修正を行うことができる。したがって、ファームウェアの検証に要する時間及び資源を低減することができる。
【００４６】
例えば、従来、シミュレーションや実機検証を行うには、専用の装置とそれを動かすための技術が必要であったが、本実施形態では検査装置１０にファームウェア２や状態遷移図４、アドレスマップ５、及び制約条件表７を読み込ませるだけの簡単な作業でファームウェアの不具合を発見でき、しかも汎用の計算機を用いて行うことができる。また、例えば、仕様書３に記載されている内容に基づいてファームウェアの検証が行うので、ハードウェアが未完成であったも仕様書の作成が終わっていれば、ファームウェアの検証を行うことができる。
【００４７】
なお、制約条件表７に示される制約条件に制約違反があった場合の修正方法を合わせて記述することにより、制約違反があった場合にファームウェア２及びそれを基に得られる動作データベースを自動的に更新し、ファームウェア検証を実行し続けるようにすることも可能である。
【００４８】
図９は、制約条件表７の他の例を示す図である。図９において、制約条件表の項目ａ〜ｅは、図２に示した制約条件表の項目ａ〜ｅと同様であるので説明は省略する。
【００４９】
項目ｆ、ｇには、制約違反があった場合の修正方法について記述される。項目ｆ、ｇの記載には、以下の組み合わせでの記述が可能である。
（３−１）項目ｆ−「削除」、項目ｇ−空白…動作データベースの現在の場所の状態を削除する。
（３−２）項目ｆ−「前挿入」、項目ｇ−命令…動作データベースの現在位置の手前に項目ｇで指定された状態を挿入する。
（３−３）項目ｆ−「レジスタ変更」、項目ｇ−「レジスタ名」…動作データベースの現在位置のレジスタ名を変更する。
（３−４）項目ｆ−「データ変更」、項目ｇ−データ…動作データベースの現在位置の状態のデータを変更する。
【００５０】
動作データベースの更新内容は、検査装置１０がパッチデータとして出力し、そのパッチデータをファームウェアに適用することにより、ファームウェアの自動修正を行うことができる。このようにした場合には、ファームウェアの検証に要する時間及び資源をさらに低減することができる。
【００５１】
（マッピング装置２０）
検査装置１０でのファームウェア検証に用いられる制約条件表７は、誤りがなく正確であることが求められる。そこで、本実施形態におけるデバッグシステム１では、マッピング装置２０が制約条件表７を解析して解析結果を出力することにより、正確な制約条件表７の作成を支援する。
【００５２】
マッピング装置２０は、入力部２１、条件解析部２２、出力部２４を有する。
入力部２１は、外部から入力されるアドレスマップ５及び制約条件表７を受ける。
【００５３】
条件解析部２２は、制約タイプ知識２３を有する。
制約タイプ知識２３は、ハードウェアに非依存の下記（１）〜（１３）の制約からなる。
（１）常にレジスタの値、状態をチェックする。
（２）常にレジスタの書き込みをチェックする。
（３）常にレジスタの書き換えをチェックする。
（４）常にレジスタの読み出しをチェックする。
（５）特定の条件のときレジスタの値、状態をチェックする。
（６）特定の条件のときレジスタの書き込みをチェックする。
（７）特定の条件のときレジスタの書き換えをチェックする。
（８）特定の条件のときレジスタの読み出しをチェックする。
（９）あるトリガが発行されたときレジスタの値、状態をチェックする。
（１０）あるトリガが発行されたときレジスタの書き込みをチェックする。
（１１）あるトリガが発行されたときレジスタの書き換えをチェックする。
（１２）あるトリガが発行されたときレジスタの読み出しをチェックする。
（１３）ファームウェアの最後にレジスタの値、状態をチェックする。
【００５４】
条件解析部２２は、入力部２１を介して入力される制約条件表７及びアドレスマップ５に基づいて、レジスタ毎に、（１）〜（１３）のどの制約に相当する制約がハードウェアの制約条件として記載されているかマッピングを行う。条件解析部２２による分類（マッピング）は、図１０に示す流れに従ってステップＳ３１〜Ｓ３５に示すように制約条件表の各項目をチェックすることにより行う。
【００５５】
出力部２４は、条件解析部２２での処理により得られるマッピング結果を出力する。この出力結果を、人間が確認し制約条件表７を補完することにより正確な制約条件表７を作成することができる。
【００５６】
例えば、図１１（ａ）に示すアドレスマップ、図１１（ｂ）に示す制約条件表がマッピング装置２０に入力された場合、制約条件は項目ａが「常に」で項目ｄが空白であるので、制約タイプ知識における（１）の制約に分類される。
【００５７】
そして、マッピング装置１０は、図１１（ｃ）に示すようなマッピング結果を出力する。この出力結果を見て、人間が自己チェックを行い、マッピング装置１０の出力と一致するか、例えば制約条件がついていない項目が本当に制約がないか、確認する。なお、図１１（ｃ）においてマッピング結果の欄がマッピング装置１０の出力に基づくものであり、チェック欄が人間の自己チェックに基づくものである。マッピング装置１０の出力では「×」となっていたのにもかかわらず、自己チェックで「○」となっている項目は、仕様書に記載されてない制約条件漏れに対応し、逆にマッピング装置１０の出力で「○」となっていて自己チェックで「×」となった項目は制約記載ミス、誤った制約であることに対応する。
【００５８】
図１１（ｃ）に示す例では、（１１）の制約に相当するハードウェア制約が実際に存在するが、マッピング装置１０の出力では制約がマッピングされていない。すなわち、制約条件漏れであると認識できる。この場合には、図１２（ａ）に示すように制約条件表に抜けていた制約条件を追加して、再びマッピング装置によるマッピングを実行する。これにより、図１２（ｂ）に示すように、マッピング装置１０の出力と自己チェックが一致する出力が得られる。このようにして、マッピング装置１０の出力及び自己チェックに基づいて、制約条件表を補完することにより制約漏れのない制約条件表を作成することができる。
【００５９】
なお、上記実施形態は、何れも本発明を実施するにあたっての具体化のほんの一例を示したものに過ぎず、これらによって本発明の技術的範囲が限定的に解釈されてはならないものである。すなわち、本発明はその技術思想、またはその主要な特徴から逸脱することなく、様々な形で実施することができる。
【図面の簡単な説明】
【００６０】
【図１】本発明の実施形態によるデバッグシステムの構成例を示す図である。
【図２】本実施形態における制約条件表の一例を示す図である。
【図３】本実施形態におけるアドレスマップの一例を示す図である。
【図４】本実施形態における状態遷移図の一例を示す図である。
【図５】動作データベースの一例を示す図である。
【図６】本実施形態における検査装置の動作を示すフローチャートである。
【図７】本実施形態における制約チェック処理の流れを示すフローチャートである。
【図８】検査装置の動作例を具体的に説明するための図である。
【図９】本実施形態における制約条件表の他の例を示す図である。
【図１０】本実施形態におけるマッピング装置でのマッピング方法を説明するための図である。
【図１１】マッピング結果の一例（修正前）を説明するための図である。
【図１２】マッピング結果の一例（修正後）を説明するための図である。
【図１３】従来のファームウェア検証の流れを示す図である。
【符号の説明】
【００６１】
１  デバッグシステム
２  ファームウェア
３  仕様書
４  状態遷移図
５  アドレスマップ
６  制約条件
７  制約条件表
１０  検査装置
１１  入力部
１２  データベース変換部
１３  内部状態管理部
１４  制約チェック部
１５  判定部
１６  出力部
２０  マッピング装置
２１  入力部
２２  条件解析部
２３  制約タイプ知識
２４  出力部
【図１】
2008102627.tif 000003
【図２】
2008102627.tif 000004
【図３】
2008102627.tif 000005
【図４】
2008102627.tif 000006
【図５】
2008102627.tif 000007
【図６】
2008102627.tif 000008
【図７】
2008102627.tif 000009
【図８】
2008102627.tif 000010
【図９】
2008102627.tif 000011
【図１０】
2008102627.tif 000012
【図１１】
2008102627.tif 000013
【図１２】
2008102627.tif 000014
【図１３】
2008102627.tif 000015