(57)【要約】【課題】検証の容易化により、検証者の労力軽減および検証期間の短縮化を図ること。【解決手段】論理シミュレータ１５０に、ＲＴＬ記述１１０、テストベンチ１４０、および期待値を与える。検証対象１００に入力パターンが与えられたときの出力パターンと期待値とが一致しているか否かを確認して、期待値リスト１３０を更新する。検証者は、論理シミュレータ１５０によるシミュレーションにより得られた結果判定ログ１５１を参照する際に、ＮＧがなければ論理仕様検証は終了する。一方、ＮＧがある場合、従来のように原因解析１７０をする必要はない。すなわち、本実施の形態の論理仕様検証装置３００により曖昧な仕様が自動修正される。また、ＲＴＬバグや検証シナリオバグも期待値リスト１３０や論理仕様検証装置３００からの出力を参照することで、人手により修正することができる。【選択図】図１
2009110417.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、
検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得手段、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出手段、
前記検出手段によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定手段、
前記入力パターン判定手段によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定手段、
前記検出手段によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定手段、
前記出力パターン判定手段によって判定された判定結果に基づいて、前記特定手段によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更手段、
前記変更手段によって変更結果を出力する出力手段、
として機能させることを特徴とする論理仕様検証プログラム。
【請求項２】
前記変更手段は、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が正確であることをあらわす第２の信頼度に変更することを特徴とする請求項１に記載の論理仕様検証プログラム。
【請求項３】
前記コンピュータを、
前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定された回数に基づいて、前記仕様の評価値を算出する算出手段として機能させ、
前記出力手段は、
前記算出手段によって算出された算出結果を出力することを特徴とする請求項１または２に記載の論理仕様検証プログラム。
【請求項４】
前記検証ルールには、前記出力パターン判定手段によって一致すると判定された場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに出力してはいけない出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の成立禁止をあらわす第３の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする請求項１に記載の論理仕様検証プログラム。
【請求項５】
前記変更手段は、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって不一致であると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が無効であることをあらわす第４の信頼度に変更することを特徴とする請求項１に記載の論理仕様検証プログラム。
【請求項６】
前記検証ルールには、前記出力パターン判定手段によって不一致であると判定された場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって不一致であると判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする請求項１に記載の論理仕様検証プログラム。
【請求項７】
検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得手段と、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出手段と、
前記検出手段によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定手段と、
前記入力パターン判定手段によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定手段と、
前記検出手段によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定手段と、
前記出力パターン判定手段によって判定された判定結果に基づいて、前記特定手段によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更手段と、
前記変更手段によって変更結果を出力する出力手段と、
を備えることを特徴とする論理仕様検証装置。
【請求項８】
検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得工程と、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出工程と、
前記検出工程によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定工程と、
前記入力パターン判定工程によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定工程と、
前記検出工程によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定工程と、
前記出力パターン判定工程によって判定された判定結果に基づいて、前記特定工程によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更工程と、
前記変更工程によって変更結果を出力する出力工程と、
を含んだことを特徴とする論理仕様検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、ＬＳＩなどのハードウェアの仕様を検証する論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法に関する。
【背景技術】
【０００２】
ＬＳＩなどのハードウェア設計では、従来から設計期間の短縮による作業効率化が要求されている一方、ＬＳＩが正しく動作するかどうかを検証する検証作業が必要不可欠であり、特に、大規模化、高機能化、高速化および低消費電力化が要求されているＬＳＩについては、高品質を維持するためにもこの検証作業は重要である。
【０００３】
まず、従来のハードウェア設計について説明する。設計者はまずハードウェアの仕様書を作成し、作成された仕様書に基づきＲＴＬ（レジスタ転送レベル、Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌの略）設計をおこなう。つぎに、論理仕様検証をおこなう。論理仕様検証では、検証者はＲＴＬ記述のハードウェアの使い方を仕様書から抽出して検証シナリオと期待値を作成し、論理シミュレーションにてその動作が期待値と一致しているかを確認する。
【０００４】
結果がＮＧの場合は原因がＲＴＬ記述にあるのか検証シナリオにあるのか期待値にあるのかを人手で判断し、修正をおこなう。その後再び論理シミュレーションをおこなう。この一連のフローを結果がＯＫとなるまで繰り返す。すべての検証シナリオにおいて動作が期待値と一致していることが確認された時点で設計完了となる（たとえば、下記特許文献１，２を参照。）。
【０００５】
【特許文献１】特開２００７−１１５００２号公報
【特許文献２】特開昭５５−０６３４４５号公報
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら、仕様書は自然言語で記述されているため、仕様の内容を完全に記述することは難しく、仕様の不備や漏れがあったり、曖昧な記述が含まれていたりする。このような場合、シミュレーションと期待値修正を繰り返しながら真の期待値を人手により探していかなければならない。
【０００７】
特に、論理シミュレーションの結果がＮＧになった場合、その原因がＲＴＬ，テストベンチ，期待値のどこにあるかといった原因解析をおこなう必要がある。しかしながら、この原因解析も人手によりおこなっていたため、論理シミュレータの実行時間よりも時間がかかることが少なくない。また、原因解析は担当回路が分かっている者でないと解析が難しい場合がある。このように、従来技術では、検証者の労力が増大し、検証期間が長期化するという問題があった。
【０００８】
この発明は、上述した従来技術による問題点を解消するため、検証の容易化により、検証者の労力軽減および検証期間の短縮化を図ることができる論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法を提供することを目的とする。
【課題を解決するための手段】
【０００９】
上述した課題を解決し、目的を達成するため、この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法は、検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得し、前記検証対象の論理シミュレーションを開始してから終了するまで、前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出し、検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定し、一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定し、検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定し、その判定結果に基づいて、特定された検証ルールに設定されている前記仕様の信頼度を変更し、その変更結果を出力することを要件とする。
【００１０】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、検証対象の一回の論理シミュレーション中に、検証ルールごとにその仕様の信頼性を自動検証することができる。
【００１１】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記出力パターンに期待値となる出力パターンが設定されており、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターンと一致すると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が正確であることをあらわす第２の信頼度に変更することとしてもよい。
【００１２】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、検証者が曖昧であると判断していた仕様が、正確な仕様であることがわかる。
【００１３】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、一致回数に基づいて、前記仕様の評価値を算出し、その算出結果を出力することとしてもよい。
【００１４】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、その検証ルールがどの程度評価されているかを知ることができる。
【００１５】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記検証ルールには、前記出力パターンと一致すると判定された場合の原因が設定されており、前記出力パターンに出力してはいけない出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の成立禁止をあらわす第３の信頼度に設定されている場合、前記出力パターンと一致すると判定されると、前記原因ありと決定し、その決定結果を出力することとしてもよい。
【００１６】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、出力パターンと一致するパターンが検証対象から出力された場合には、その解析原因が判明する。
【００１７】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターンと不一致であると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様を無効にすべきであることをあらわす第４の信頼度に変更することとしてもよい。
【００１８】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、期待値となる出力パターンが出力されない検証ルールを集合から特定することができる。
【００１９】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記検証ルールには、前記出力パターンと不一致であると判定された場合の解析原因が設定されており、前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターンと不一致であると判定されると、前記解析原因ありと決定し、その決定結果を出力することとしてもよい。
【００２０】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、出力パターンと不一致なパターンが検証対象から出力された場合には、その解析原因が判明する。
【００２１】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記検証ルールには、前記出力パターンと不一致であると判定された場合の解析原因が設定されており、前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記出力パターンと不一致であると判定されると、前記解析原因ありと決定し、その決定結果を出力することとしてもよい。
【００２２】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、論理シミュレーション前は、検証者は仕様が正確であると判断していても、実際に論理シミュレーションを実行すると、解析原因があることがわかる。
【００２３】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が無効であることをあらわす第４の信頼度に変更することとしてもよい。
【００２４】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、期待値となる出力パターンが設定時間内に出力されない検証ルールを集合から特定することができる。
【００２５】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記検証ルールには、前記出力パターンの判定がタイムアウトになった場合の解析原因が設定されており、前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記解析原因ありと決定し、その決定結果を出力することとしてもよい。
【００２６】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、出力パターンが検証対象から設定時間内に出力されなかった場合には、その解析原因が判明する。
【００２７】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記検証ルールには、前記出力パターンの判定がタイムアウトになった場合の解析原因が設定されており、前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記解析原因ありと決定し、その決定結果を出力することとしてもよい。
【００２８】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、論理シミュレーション前は、検証者は仕様が正確であると判断していても、実際に論理シミュレーションを実行すると、タイムアウトに関する解析原因があることがわかる。
【００２９】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、前記解析原因は、前記検証対象のＲＴＬ記述に関するバグまたは前記仕様の検証シナリオに関するバグであることとしてもよい。
【００３０】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、解析原因を具体的に特定することができる。
【００３１】
また、上記論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法において、特定された検証ルールに設定されている仕様が、当該仕様が無効であることをあらわす第４の信頼度に設定されている場合、前記検証対象から出力されるパターンの検出を禁止することとしてもよい。
【００３２】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、無効となった検証ルールの再検証を禁止することができる。
【発明の効果】
【００３３】
この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、検証の容易化により、検証者の労力軽減および検証期間の短縮化を図ることができるという効果を奏する。
【発明を実施するための最良の形態】
【００３４】
以下に添付図面を参照して、この論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法の好適な実施の形態を詳細に説明する。図１は、本実施の形態にかかる論理仕様検証の概要を示す説明図である。図１において、まず、設計者は、ハードウェアなどの検証対象１００の仕様書を作成し、作成された仕様書に基づきＲＴＬ設計１０１をおこなってＲＴＬ記述の設計データ（以下、単に、「ＲＴＬ記述１１０」）を得る。
【００３５】
つぎに、論理仕様検証をおこなう。論理仕様検証では、検証者はＲＴＬ記述１１０のハードウェアの使い方を仕様書から抽出して検証シナリオ作成１０２と期待値作成１０３をおこなう。検証シナリオ１２０はトランザクタ１２１により処理されてテストベンチ１４０に埋め込まれる。
【００３６】
そして、論理シミュレータ１５０に、ＲＴＬ記述１１０、テストベンチ１４０、および期待値を与える。このあと、検証対象１００にインターフェースＸにより入力パターンと同一のパターンが与えられたときに、インターフェースＹまたはＺから出力されるパターンと出力パターン（期待値）とが一致しているか否かを確認して、期待値リスト１３０を更新する。
【００３７】
検証者は、論理シミュレータ１５０によるシミュレーションにより得られた結果判定ログ１５１を参照する際に、ＮＧがなければ論理仕様検証は終了する。一方、ＮＧがある場合、従来のように原因解析１７０をする必要はない。すなわち、本実施の形態の論理仕様検証装置３００により曖昧な仕様が自動修正される。また、ＲＴＬバグや検証シナリオバグも期待値リスト１３０や論理仕様検証装置３００からの出力を参照することで、人手により修正することができる。このように、本実施の形態では、シミュレーション結果の原因解析の容易化を図ることができ、論理仕様検証の効率化を実現することができる。
【００３８】
（期待値リスト１３０）
図２−１は、図１に示した期待値リスト１３０を示す説明図である。期待値リスト１３０は、検証者により作成されるコンピュータ読み取り可能な電子データである。期待値リスト１３０では、検証ルール（以下、単に「ルール」）ごとに各種項目が設定されている。各ルールは、入力パターンと期待値となる出力パターンの組み合わせとこれらに関する情報により定義される。ルールごとに入力パターンと期待値となる出力パターンの組み合わせは異なる。以下、各項目について説明する。
【００３９】
まず、「ルール番号」とは、ルールに固有な番号をあらわす項目である。単独のルールの番号は数字のみであらわすが、ペアルールの場合、１ａ，１ｂのように、同一の数字と互いに異なるアルファベットの組み合わせで表現する。ペアルールは、仕様が複数通りに解釈できる場合や、状況に応じて同じ入力パターンでも複数通りの出力パターンが考えられる場合に用いる。
【００４０】
つぎに、「状態」とは、検証対象１００の状態をあらわす項目であり、論理シミュレータ１５０によるシミュレーション実行中に逐次書き換わる項目である。状態には、“ＩＤＬＥ”と“ＡＣＴＩＶＥ”の２通りの状態が存在する。シミュレーション開始時点では“ＩＤＬＥ”になっている。“ＩＤＬＥ”のときはテストベンチ１４０から検証対象１００へ入力されるパターンを、“ＡＣＴＩＶＥ”のときは検証対象１００からテストベンチ１４０へ出力されるパターンを待ち受けている。
【００４１】
また、「仕様」とは、検証対象１００の仕様書の信頼度をあらわす項目であり、論理シミュレータ１５０によるシミュレーション実行中に逐次書き換わる項目である。ここでは、“○”の場合は信頼性の高い仕様、“△”の場合は信頼性が曖昧な仕様、“×”の場合は成り立ってはいけない仕様、“−”の場合は、無効になっている仕様をあらわす。
【００４２】
ここで、「無効」の場合、状態は常に“ＩＤＬＥ”となり入力パターンにも反応しない。シミュレーション開始時点では検証者の主観により「仕様」が決定されている。信頼性が曖昧な仕様（△）の場合はシミュレーション中に信頼性の高い仕様（○）または無効になっている仕様（−）に書き換わることがある。この項目をシミュレーション終了時に確認することで、シミュレーション開始時に信頼性が低いとしていた仕様が正しいのか誤りなのかが分かる。
【００４３】
また、「評価回数」とは、本ルールが評価された回数を示す。シミュレーション開始時は０に設定されている。この項目はシミュレーション中に入力パターンとそれに対応する出力パターンが現れたときに１ずつ増加する。この項目をシミュレーション終了時に確認することで、一回もチェックされなかったルールが分かり、検証シナリオ１２０が不足していることが分かる。
【００４４】
また、「入力パターン」とは、検証対象１００を動かすための入力パターンを記述する項目である。具体的には、入力パターンが入力されるインターフェース（ｉｆ）、入力パターンのアドレス（ａｄｒ）、データ名（ｄａｔ）、データサイズ（ｓｉｚｅ）により入力パターンを特定する。“ＩＤＬＥ”状態のルールは入力パターンを待っており、入力パターンが確認された時点で当該ルールの状態は“ＡＣＴＩＶＥ”となる。なお、入力パターンが複数のデータで構成されているときは複数行にわたって記述する。
【００４５】
また、「出力パターン」とは、入力パターンが現れたときの検証対象１００の出力パターン（期待値となる出力パターンまたは出力してはいけない出力パターン）を記述する項目である。具体的には、出力パターンが出力されるインターフェース（ｉｆ）、出力パターンのアドレス（ａｄｒ）、データ名（ｄａｔ）、データサイズ（ｓｉｚｅ）により出力パターンを特定する。出力パターンが複数のデータで構成されているときは複数行にわたって記述する。
【００４６】
また、「最大時間」とは、入力パターンが現れてから出力パターンが現れるまでの設定時間を記述する項目である。この最大時間に達しても出力されなかった場合タイムアウトとなる。
【００４７】
また、「一致」とは、出力パターンと一致するパターンが最大時間内に現れたときの処理を記述する項目である。この項目は小項目として、ＲＴＬ項目、シナリオ項目およびルール項目がある。ＲＴＬ項目は、検証対象１００のＲＴＬ記述１１０に解析原因があると考えた場合に“○”を付けるための項目であり、シナリオ項目は検証対象１００の検証シナリオ１２０に解析原因があると考えた場合に“○”を付けるための項目であり、ルール項目は、仕様の信頼度が曖昧（“△”）である場合に、信頼度の変更を許可するための項目である。検証者は、この小項目に“○”を付ける。“○”は複数つけても良いし１つもつけなくても良い。ただし、ＲＴＬ項目およびシナリオ項目の両方には“○”は付けられない。
【００４８】
図２−２は小項目への“○”の付け方のバリエーション例を示す説明図である。“○”の付け方としては、たとえば、仕様が“○”の場合、どの小項目にも“○”を付けない。また、仕様が“△”の場合、出力パターン（期待値となる出力パターン）が一致したときに仕様の確からしさを確定するため、ルール項目に“○”を付ける。また、「出力パターン」に出力してはいけないパターンを記述した場合に、仕様を“×”にする。この場合、出力パターン（出力してはいけない出力パターン）が一致したときに解析原因と考えられるＲＴＬ項目またはシナリオ項目に“○”を付ける。
【００４９】
論理仕様検証装置３００では、ルール項目に“○”が付けられている場合、「仕様」が曖昧（“△”）のときは、「仕様」を高い信頼度（“○”）に書き換える処理を実行する。ＲＴＬ項目に“○”が付けられている場合、ＲＴＬバグに決定する処理を実行する。また、シナリオ項目に“○”が付けられている場合、検証シナリオバグに決定する処理を実行する。
【００５０】
また、図２−１において、「不一致」とは、出力パターンと不一致のパターンが最大時間内に現れたときの処理を記述する項目である。この項目は小項目として、ＲＴＬ項目、シナリオ項目およびルール項目がある。ＲＴＬ項目は、検証対象１００のＲＴＬ記述１１０に解析原因があると考えた場合に“○”を付けるための項目であり、シナリオ項目は検証対象１００の検証シナリオ１２０に解析原因があると考えた場合に“○”を付けるための項目であり、ルール項目は、仕様の信頼度が曖昧（“△”）である場合に、信頼度の変更を許可するための項目である。検証者は、この小項目に“○”を付ける。“○”は複数つけても良いし１つもつけなくても良い。ただし、ＲＴＬ項目およびシナリオ項目の両方には“○”は付けられない。
【００５１】
図２−２に示したように、“○”の付け方としては、たとえば、仕様が“○”の場合、ＲＴＬ項目またはシナリオ項目に“○”を付ける。また、仕様が“△”の場合、ＲＴＬ項目、シナリオ項目またはルール項目に“○”を付ける。出力パターン（期待値となる出力パターン）が不一致のときにそのルールを無効にするため、ルール項目に“○”を付ける。また、出力パターン（期待値となる出力パターン）が不一致であるときに解析原因と考えられるＲＴＬ項目またはシナリオ項目に“○”を付ける。仕様が“×”の場合、どの小項目にも“○”を付けない。
【００５２】
論理仕様検証装置３００では、ルール項目に“○”が付けられている場合、「仕様」が低い信頼度（“△”）のときは、「仕様」を無効（“−”）に書き換える処理を実行する。ＲＴＬ項目に“○”が付けられている場合、ＲＴＬバグに決定する処理を実行する。ただし、“ＡＣＴＩＶＥ”なペアルールが存在する場合はこの限りでない。また、シナリオ項目に“○”が付けられている場合、検証シナリオバグに決定する処理を実行する。ただし、“ＡＣＴＩＶＥ”なペアルールが存在する場合はこの限りでない。
【００５３】
また、「タイムアウト」とは、出力パターンが時間内に現れなかったときの処理を記述する項目である。この項目は小項目として、ＲＴＬ項目、シナリオ項目およびルール項目がある。小項目の“○”の付け方や処理内容は、「不一致」の場合と同様である。また、「バグ種」は、バグの種類を特定する項目であり、論理シミュレータ１５０によるシミュレーション実行中に逐次書き換わる項目である。これにより、シミュレーション開始時は空欄であり、シミュレーション中に「ＲＴＬバグ」、「検証シナリオバグ」などといったバグの種類が書き込まれる場合がある。
【００５４】
（論理仕様検証装置３００のハードウェア構成）
つぎに、実施の形態にかかる論理仕様検証装置３００のハードウェア構成について説明する。図３は、論理仕様検証装置３００のハードウェア構成を示す説明図である。
【００５５】
図３において、論理仕様検証装置３００は、コンピュータ本体３１０と、入力装置３２０と、出力装置３３０と、から構成されており、不図示のルータやモデムを介してＬＡＮ，ＷＡＮやインターネットなどのネットワーク３４０に接続可能である。
【００５６】
コンピュータ本体３１０は、ＣＰＵ，メモリ，インターフェースを有する。ＣＰＵは、論理仕様検証装置３００の全体の制御を司る。メモリは、ＲＯＭ，ＲＡＭ，ＨＤ，光ディスク３１１，フラッシュメモリから構成される。メモリはＣＰＵのワークエリアとして使用される。
【００５７】
また、メモリには各種プログラムが格納されており、ＣＰＵからの命令に応じてロードされる。ＨＤおよび光ディスク３１１はディスクドライブによりデータのリード／ライトが制御される。また、光ディスク３１１およびフラッシュメモリはコンピュータ本体３１０に対し着脱自在である。インターフェースは、入力装置３２０からの入力、出力装置３３０への出力、ネットワーク３４０に対する送受信の制御をおこなう。
【００５８】
また、入力装置３２０としては、キーボード３２１、マウス３２２、スキャナ３２３などがある。キーボード３２１は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式であってもよい。マウス３２２は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。スキャナ３２３は、画像を光学的に読み取る。読み取られた画像は画像データとして取り込まれ、コンピュータ本体３１０内のメモリに格納される。なお、スキャナ３２３にＯＣＲ機能を持たせてもよい。
【００５９】
また、出力装置３３０としては、ディスプレイ３３１、プリンタ３３２、スピーカ３３３などがある。ディスプレイ３３１は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。また、プリンタ３３２は、画像データや文書データを印刷する。またスピーカ３３３は、効果音や読み上げ音などの音声を出力する。
【００６０】
（論理仕様検証装置３００の機能的構成）
つぎに、論理仕様検証装置３００の機能的構成について説明する。図４は、論理仕様検証装置３００の機能的構成を示すブロック図である。図４において、論理仕様検証装置３００は、取得部４０１と、検出部４０２と、入力パターン判定部４０３と、特定部４０４と、出力パターン判定部４０５と、変更部４０６と、出力部４０７と、算出部４０８と、決定部４０９と、を備えている。これら各機能４０１〜４０９は、論理仕様検証装置３００の記憶部に記憶された当該機能４０１〜４０９に関するプログラムをＣＰＵに実行させることにより、または、入出力Ｉ／Ｆにより、当該機能を実現することができる。
【００６１】
また、各機能４０１〜４０９からの出力データは上記記憶部に保持される。また、図４中矢印で示した接続先の機能は、接続元の機能からの出力データを記憶部から読み込んで、当該機能に関するプログラムをＣＰＵに実行させるものとする。
【００６２】
まず、取得部４０１は、検証対象１００に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する機能を有する。検証ルールの集合とは、図２−１に示した期待値リスト１３０である。取得部４０１では、期待値リスト１３０を読み込んでＨＤやメモリなどの記憶部に保存する。
【００６３】
検出部４０２は、検証対象１００に入力されるパターンと、当該パターンが入力された結果、検証対象１００から出力されるパターンとを検出する機能を有する。具体的には、検出部４０２は、検証対象１００の論理シミュレーションの実行開始から実行終了までの間、テストベンチ１４０から検証対象１００に入力されるパターンと、検証対象１００からテストベンチ１４０に出力されるパターンとを監視して、これらが入力／出力されると、そのパターンを取り込む。
【００６４】
入力パターン判定部４０３は、検出部４０２によって検出された検証対象１００に入力されるパターンと一致する入力パターンが集合内にあるか否かを判定する機能を有する。具体的には、テストベンチ１４０から検証対象１００に入力されるパターンと同一の入力パターンを期待値リスト１３０から検索する。
【００６５】
特定部４０４は、入力パターン判定部４０３によって一致すると判定された入力パターンに関する検証ルールを集合の中から特定する機能を有する。具体的には、テストベンチ１４０から検証対象１００に入力されるパターンと同一の入力パターンが記述されているルールを“ＩＤＬＥ”状態から“ＡＣＴＩＶＥ”状態に遷移する。
【００６６】
出力パターン判定部４０５は、検出部４０２によって検出された検証対象１００から出力されるパターンと一致する出力パターンが集合内にあるか否かを判定する機能を有する。具体的には、対象ルールの出力パターンと同一のパターンの出力が検出部４０２によって検出されたか否かを判定する。
【００６７】
判定結果は、設定時間、すなわち、対象ルールの「最大時間」以内に出力パターンと同一のパターンの出力が検出された場合には一致パターンありという判定結果となる。また、対象ルールの「最大時間」以内に出力パターンとは異なるパターンの出力が検出された場合には、不一致パターンありという判定結果となる。さらに、対象ルールの「最大時間」以内に出力パターンと同一または異なるパターンのいずれの出力も検出されなかった場合には、タイムアウトという判定結果となる。
【００６８】
変更部４０６は、出力パターン判定部４０５によって判定された判定結果に基づいて、特定部４０４によって特定された検証ルールに設定されている仕様の信頼度を変更する機能を有する。具体的には、期待値リスト１３０内の対象ルールの仕様が“△”である場合、出力パターン判定部４０５の判定結果が「一致パターンあり」のときは、その仕様を“○”に変更する。また、出力パターン判定部４０５の判定結果が「不一致パターンあり」または「タイムアウト」のときは、その仕様を“―”に変更する。仕様が“○”または“×”の場合には、変更しない。
【００６９】
出力部４０７は、変更部４０６によって変更された変更結果を出力する機能を有する。具体的には、仕様が変更された対象ルールを出力する。より具体的には、検証対象１００の論理シミュレーションが終了した場合には、最終的な期待値リスト１３０を出力する。なお、出力形式は、ディスプレイへの表示、プリンタによる印刷出力、外部のコンピュータへの送信、内部の記憶部への格納などがある。
【００７０】
算出部４０８は、仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度（仕様：“○”）に設定されている場合、出力パターン判定部４０５によって一致すると判定された回数に基づいて、仕様の評価値を算出する機能を有する。具体的には、仕様が“○”の状態で、そのルールが適用された回数、すなわち、そのルールの入力パターンと同一のパターンが入力され、かつ、そのルールの期待値となる出力パターンと同一のパターンが検証対象１００から出力された場合に、評価回数を計数する。この計数結果が評価値となる。そして、検証対象１００の論理シミュレーションが終了した場合には、最終的な期待値リスト１３０には評価値（評価回数）が反映されて出力されることとなる。
【００７１】
したがって、論理シミュレーション中に、同一ルールが何度も適用されると、評価回数もその分上昇する。したがって、評価回数が０であるルールについては、一度も適用されていないことがわかり、検証網羅性を確認することができる。なお、ここで、評価値を評価回数として算出したが、適用の有無（すなわち、評価回数が１または０）であらわしてもよい。
【００７２】
決定部４０９は、出力パターンに出力してはいけない出力パターンが設定され、かつ、仕様の信頼度が当該仕様の成立禁止をあらわす第３の信頼度（仕様：“×”）に設定されている場合、出力パターン判定部４０５によって一致すると判定されると、解析原因ありと決定する機能を有する。
【００７３】
具体的には、図２−１に示したように、各ルールには、出力パターン判定部４０５によって一致すると判定された場合の解析原因（ＲＴＬ項目やシナリオ項目の“○”印）が設定されており、対象ルールにおいて、出力してはいけない出力パターンがあらわれると、対象ルールにおける解析原因を、論理シミュレーション前に設定しておいた解析原因に決定する。
【００７４】
また、図２−１に示したように、各ルールには、出力パターン判定部４０５によって不一致であると判定された場合の解析原因（ＲＴＬ項目やシナリオ項目の“○”印）も設定されている。したがって、出力パターンに期待値となる出力パターンが設定され、かつ、仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度（仕様：“△”）に設定されている場合、出力パターン判定部４０５によって不一致であると判定されると、解析原因ありと決定する。
【００７５】
また、図２−１に示したように、各ルールには、出力パターン判定部４０５によって不一致であると判定された場合の解析原因（ＲＴＬ項目やシナリオ項目の“○”印）が設定されている。したがって、出力パターンに期待値となる出力パターンが設定され、かつ、仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度（仕様：“○”）に設定されている場合、出力パターン判定部４０５によって不一致であると判定されると、解析原因ありと決定する。
【００７６】
また、図２−１に示したように、各ルールには、出力パターン判定部４０５による判定がタイムアウトになった場合の解析原因（ＲＴＬ項目やシナリオ項目の“○”印）が設定されている。したがって、出力パターンに期待値となる出力パターンが設定され、かつ、仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度（仕様：“△”）に設定されている場合、出力パターン判定部４０５によって、検証対象１００から出力されるパターンが、仕様に関する設定時間内に検出されなかったと判定されると、解析原因ありと決定する。
【００７７】
また、図２−１に示したように、各ルールには、出力パターン判定部４０５による判定がタイムアウトになった場合の解析原因が設定されている。したがって、出力パターンに期待値となる出力パターンが設定され、かつ、仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度（仕様：“○”）に設定されている場合、出力パターン判定部４０５によって、検証対象１００から出力されるパターンが、仕様に関する設定時間内に検出されなかったと判定されると、解析原因ありと決定する。なお、検証対象１００の論理シミュレーションが終了した場合には、最終的な期待値リスト１３０に決定結果が反映されて出力されることとなる。
【００７８】
（論理仕様検証処理手順）
つぎに、実施の形態にかかる論理仕様検証処理手順について説明する。図５は、実施の形態にかかる論理仕様検証処理手順を示すフローチャートである。図５において、まず、検証対象１００のシミュレーションが開始されるのを待ち受け（ステップＳ５０１：Ｎｏ）、シミュレーションが開始された場合（ステップＳ５０１：Ｙｅｓ）、ルールの状態が“ＩＤＬＥ”状態か“ＡＣＴＩＶＥ”状態かを判断する（ステップＳ５０２）。
【００７９】
ここで、シミュレーション開始時では、すべてのルールが判断対象となる。シミュレーション開始時ではすべてのルールは“ＡＣＴＩＶＥ”状態である。一方、シミュレーション開始後は、後述するステップＳ５０４で該当するルールが特定されるため、シミュレーション開始後は、該当するルールのみが判断対象となる。
【００８０】
ステップＳ５０２において、“ＩＤＬＥ”状態と判断された場合（ステップＳ５０２：ＩＤＬＥ）、検証対象１００に対して、期待値リスト１３０に記述された入力パターンと同一のパターンが入力されたか否かを検出する（ステップＳ５０３）。検出されない場合（ステップＳ５０３：Ｎｏ）、ステップＳ５０２に戻る。
【００８１】
一方、期待値リスト１３０に記述された入力パターンと同一のパターンが入力されたことが検出された場合（ステップＳ５０３：Ｙｅｓ）、該当するルール、すなわち、その入力されたパターンが入力パターンとして記述されているルールを特定する（ステップＳ５０４）。以降、特定されたルールを「対象ルール」と称す。対象ルールにペアルールが存在する場合には、そのペアルールも対象ルールに特定する。また、この場合、ステップＳ５０２では、対象ルールのうちいずれか一つでも“ＡＣＴＩＶＥ”状態があれば、ステップＳ５０７に移行する。
【００８２】
そして、期待値リスト１３０の仕様項目を参照して、対象ルールの仕様が無効（“−”）であるか否かを判断する（ステップＳ５０５）。無効である場合（ステップＳ５０５：Ｙｅｓ）、ステップＳ５１３に移行する。一方、無効でない場合（ステップＳ５０５：Ｎｏ）、状態を“ＩＤＬＥ”から“ＡＣＴＩＶＥ”に遷移して（ステップＳ５０６）、ステップＳ５０２に戻る。
【００８３】
また、ステップＳ５０２において、ルールの状態が“ＡＣＴＩＶＥ”状態である場合（ステップＳ５０２：ＡＣＴＩＶＥ）、検証対象１００から、期待値リスト１３０に記述された出力パターンと同一のパターンが出力されたか否かを検出する（ステップＳ５０７）。同一のパターンが検出された場合（ステップＳ５０７：Ｙｅｓ）、一致処理を実行する（ステップＳ５０８）。一致処理の詳細については後述する。一致処理の終了後は、ステップＳ５１３に移行する。
【００８４】
一方、同一のパターンが検出されなかった場合（ステップＳ５０７：Ｎｏ）、出力パターンと異なるパターンが検出されたか否かを判断する（ステップＳ５０９）。異なるパターンが検出された場合（ステップＳ５０９：Ｙｅｓ）、不一致処理を実行する（ステップＳ５１０）。不一致処理の詳細については後述する。不一致処理の終了後は、ステップＳ５１３に移行する。
【００８５】
一方、異なるパターンが検出されなかった場合（ステップＳ５０９：Ｎｏ）、タイムアウトか否かを判断する（ステップＳ５１１）。タイムアウトである場合（ステップＳ５１１：Ｙｅｓ）、タイムアウト処理を実行する（ステップＳ５１２）。タイムアウト処理の詳細については後述する。一方、タイムアウトでない場合（ステップＳ５１１：Ｎｏ）、ステップＳ５０７に戻る。タイムアウト処理の終了後は、ステップＳ５１３に移行する。
【００８６】
また、ステップＳ５１３において、シミュレーションが終了したか否かを判断する。終了していない場合（ステップＳ５１３：Ｎｏ）、ステップＳ５０２に戻る。一方、終了した場合（ステップＳ５１３：Ｙｅｓ）、結果出力をおこなう（ステップＳ５１４）。結果出力では、最終的な期待値リスト１３０が出力される。これにより、一連の処理を終了する。
【００８７】
（一致処理）
つぎに、上述した一致処理（ステップＳ５０８）の詳細な処理手順について説明する。図６は、一致処理（ステップＳ５０８）の詳細な処理手順を示すフローチャートである。図６において、まず、対象ルールの仕様が“△”であるか否かを判断する（ステップＳ６０１）。“△”である場合（ステップＳ６０１：Ｙｅｓ）、期待値リスト１３０の一致項目の小項目であるルール項目に“○”があるか否かを判断する（ステップＳ６０２）。“○”がある場合（ステップＳ６０２：Ｙｅｓ）、仕様を“△”から“○”に書き換える（ステップＳ６０３）。そして、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して、ステップＳ５１３に移行する。
【００８８】
一方、ステップＳ６０１において、仕様が“△”でない場合（ステップＳ６０１：Ｎｏ）、または、ステップＳ６０２において、ルール項目に“○”がない場合（ステップＳ６０２：Ｎｏ）、ＲＴＬ項目に“○”があるか否かを判断する（ステップＳ６０５）。
【００８９】
ＲＴＬ項目に“○”がある場合（ステップＳ６０５：Ｙｅｓ）、対象ルールの仕様にはＲＴＬバグありと決定する（ステップＳ６０６）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ６０７）、ステップＳ５１３に移行する。
【００９０】
また、ＲＴＬ項目に“○”がない場合（ステップＳ６０５：Ｎｏ）、シナリオ項目に“○”があるか否かを判断する（ステップＳ６０８）。シナリオ項目に“○”がある場合（ステップＳ６０８：Ｙｅｓ）、対象ルールの仕様には検証シナリオバグありと決定する（ステップＳ６０９）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ６１０）、ステップＳ５１３に移行する。
【００９１】
また、シナリオ項目に“○”がない場合（ステップＳ６０８：Ｎｏ）、対象ルールの評価回数を１加算する（ステップＳ６１１）。そして、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して（ステップＳ６１２）、ステップＳ５１３に移行する。
【００９２】
この一致処理では、ステップＳ６０１において仕様が“△”の場合、ルール項目に“○”があれば、曖昧な仕様（“△”）が正確な仕様であることがわかるため、仕様を“○”に書き換えている（ステップＳ６０３）。また、ルール項目ではなくＲＴＬ項目またはシナリオ項目に“○”がある場合、出力パターンには出力してはいけないパターンが記述されているため、ＲＴＬバグまたはシナリオバグであることが判明する。
【００９３】
また、この一致処理では、ステップＳ６０１において仕様が“○”の場合、ＲＴＬ項目やシナリオ項目にも“○”が付けられていないため、正しく評価されたことがわかる（ステップＳ６１１）。また、仕様が“×”である場合、ＲＴＬ項目またはシナリオ項目に“○”があると、出力パターンには出力してはいけないパターンが記述されているため、ＲＴＬバグまたはシナリオバグであることが判明する。
【００９４】
（不一致処理）
つぎに、上述した不一致処理（ステップＳ５１０）の詳細な処理手順について説明する。図７は、不一致処理（ステップＳ５１０）の詳細な処理手順を示すフローチャートである。図７において、まず、対象ルールにペアルールがあるか否かを判断する（ステップＳ７０１）。ペアルールがある場合（ステップＳ７０１：Ｙｅｓ）、ペアルールが“ＡＣＴＩＶＥ”状態であるか否かを判断する（ステップＳ７０２）。“ＡＣＴＩＶＥ”状態である場合（ステップＳ７０２：Ｙｅｓ）、ステップＳ５１３に移行する。
【００９５】
一方、ステップＳ７０１においてペアルールがない場合（ステップＳ７０１：Ｎｏ）、または、ステップＳ７０２においてペアルールがあってもそのペアルールが“ＩＤＬＥ”状態である場合（ステップＳ７０２：Ｎｏ）、対象ルールの仕様が“△”であるか否かを判断する（ステップＳ７０３）。
【００９６】
そして、対象ルールの仕様が“△”であるか否かを判断する（ステップＳ７０３）。“△”である場合（ステップＳ７０３：Ｙｅｓ）、期待値リスト１３０の不一致項目の小項目であるルール項目に“○”があるか否かを判断する（ステップＳ７０４）。“○”がある場合（ステップＳ７０４：Ｙｅｓ）、仕様を“△”から“−”に書き換える（ステップＳ７０５）。そして、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して（ステップＳ７０６）、ステップＳ５１３に移行する。
【００９７】
一方、ステップＳ７０３において、仕様が“△”でない場合（ステップＳ７０３：Ｎｏ）、または、ステップＳ７０４において、ルール項目に“○”がない場合（ステップＳ７０４：Ｎｏ）、ＲＴＬ項目に“○”があるか否かを判断する（ステップＳ７０７）。
【００９８】
ＲＴＬ項目に“○”がある場合（ステップＳ７０７：Ｙｅｓ）、対象ルールの仕様にはＲＴＬバグありと決定する（ステップＳ７０８）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ７０９）、ステップＳ５１３に移行する。
【００９９】
また、ＲＴＬ項目に“○”がない場合（ステップＳ７０７：Ｎｏ）、シナリオ項目に“○”があるか否かを判断する（ステップＳ７１０）。シナリオ項目に“○”がある場合（ステップＳ７１０：Ｙｅｓ）、対象ルールの仕様には検証シナリオバグありと決定する（ステップＳ７１１）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ７１２）、ステップＳ５１３に移行する。
【０１００】
また、シナリオ項目に“○”がない場合（ステップＳ７１０：Ｎｏ）、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して（ステップＳ７１３）、ステップＳ５１３に移行する。
【０１０１】
この不一致処理では、ステップＳ７０３において仕様が“△”の場合、ルール項目に“○”があれば、曖昧な仕様（“△”）が不要な仕様であることがわかるため、仕様を“−”に書き換えている（ステップＳ７０５）。また、ルール項目ではなくＲＴＬ項目またはシナリオ項目に“○”がある場合、出力パターンとは不一致であるため、ＲＴＬバグまたはシナリオバグであることが判明する。
【０１０２】
また、この不一致処理では、ステップＳ７０３において仕様が“○”の場合、ＲＴＬ項目またはシナリオ項目に“○”があると、出力パターンには出力してはいけないパターンが記述されているため、ＲＴＬバグまたはシナリオバグであることが判明する。
【０１０３】
（タイムアウト処理）
つぎに、上述したタイムアウト処理（ステップＳ５１２）の詳細な処理手順について説明する。図８は、タイムアウト処理（ステップＳ５１２）の詳細な処理手順を示すフローチャートである。図８において、まず、対象ルールにペアルールがあるか否かを判断する（ステップＳ８０１）。ペアルールがある場合（ステップＳ８０１：Ｙｅｓ）、ペアルールが“ＡＣＴＩＶＥ”状態であるか否かを判断する（ステップＳ８０２）。“ＡＣＴＩＶＥ”状態である場合（ステップＳ８０２：Ｙｅｓ）、ステップＳ５１３に移行する。
【０１０４】
一方、ステップＳ８０１においてペアルールがない場合（ステップＳ８０１：Ｎｏ）、または、ステップＳ８０２においてペアルールがあってもそのペアルールが“ＩＤＬＥ”状態である場合（ステップＳ８０２：Ｎｏ）、対象ルールの仕様が“△”であるか否かを判断する（ステップＳ８０３）。
【０１０５】
そして、“△”である場合（ステップＳ８０３：Ｙｅｓ）、期待値リスト１３０のタイムアウト項目の小項目であるルール項目に“○”があるか否かを判断する（ステップＳ８０４）。“○”がある場合（ステップＳ８０４：Ｙｅｓ）、仕様を“△”から“−”に書き換える（ステップＳ８０５）。そして、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して（ステップＳ８０６）、ステップＳ５１３に移行する。
【０１０６】
一方、ステップＳ８０３において、仕様が“△”でない場合（ステップＳ８０３：Ｎｏ）、または、ステップＳ８０４において、ルール項目に“○”がない場合（ステップＳ８０４：Ｎｏ）、ＲＴＬ項目に“○”があるか否かを判断する（ステップＳ８０７）。
【０１０７】
ＲＴＬ項目に“○”がある場合（ステップＳ８０７：Ｙｅｓ）、対象ルールの仕様にはＲＴＬバグありと決定する（ステップＳ８０８）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ８０９）、ステップＳ５１３に移行する。
【０１０８】
また、ＲＴＬ項目に“○”がない場合（ステップＳ８０７：Ｎｏ）、シナリオ項目に“○”があるか否かを判断する（ステップＳ８１０）。シナリオ項目に“○”がある場合（ステップＳ８１０：Ｙｅｓ）、対象ルールの仕様には検証シナリオバグありと決定する（ステップＳ８１１）。そして、その旨を期待値リスト１３０に書き込んで（ステップＳ８１２）、ステップＳ５１３に移行する。
【０１０９】
また、シナリオ項目に“○”がない場合（ステップＳ８１０：Ｎｏ）、対象ルールの状態を“ＡＣＴＩＶＥ”状態から“ＩＤＬＥ”状態に遷移して（ステップＳ８１３）、ステップＳ５１３に移行する。
【０１１０】
このタイムアウト処理では、ステップＳ８０３において仕様が“△”の場合、ルール項目に“○”があれば、曖昧な仕様（“△”）が不要な仕様であることがわかるため、仕様を“−”に書き換えている（ステップＳ８０５）。また、ルール項目ではなくＲＴＬ項目またはシナリオ項目に“○”がある場合、出力パターンとは不一致であるため、ＲＴＬバグまたは検証シナリオバグであることが判明する。
【０１１１】
また、このタイムアウト処理では、ステップＳ８０３において仕様が“○”の場合、ＲＴＬ項目またはシナリオ項目に“○”があると、出力パターンには出力してはいけないパターンが記述されているため、ＲＴＬバグまたはシナリオバグであることが判明する。以下、上述した実施の形態の実施例について説明する。
【実施例１】
【０１１２】
実施例１はある入力パターンに対して期待する出力パターンが２種類（１ａ，１ｂ）考えられ、場合により双方の出力パターンがありえるのかどちらか片方しかありえないのか分からないが、この２種類の出力パターン以外は考えられない例である。図９は、実施例１の期待値リストであり、図１０は、実施例１のタイムチャートである。
【０１１３】
時刻ｔ１にてルール１ａ，１ｂの入力パターンが検出されたためルール１ａ，１ｂが“ＡＣＴＩＶＥ”になる。時刻ｔ２において、ルール１ａは出力パターンとは違うものが現れたので不一致、ルール１ａの不一致処理はＲＴＬ誤りであるがペアルール１ｂが“ＡＣＴＩＶＥ”のため何も行わない。
【０１１４】
時刻ｔ３でルール１ｂの出力パターンが検出されたためルール１ｂの一致処理が行われ仕様を曖昧（“△”）から信頼性が高い（“○”）に書き換える。その後、一致データ（３データ）をデータバッファから取り除く。そしてルール１ｂの評価回数を１増やし、ルール１ｂは“ＩＤＬＥ”になる。
【０１１５】
時刻ｔ４においてルール１ａ，１ｂの入力パターンが検出されたためルール１ａ，１ｂが“ＡＣＴＩＶＥ”になる。時刻ｔ５において、ルール１ａの入力パターンが検出されたためルール１ａの一致処理が行われ仕様を“○”に書き換える。その後一致データ（２データ）をデータバッファから取り除き、ペアルール１ｂの不一致処理を行う。ルール１ｂの不一致処理はＲＴＬ誤りであるがペアルール１ａが“ＡＣＴＩＶＥ”のため行わない。
【０１１６】
そしてルール１ａの評価回数を１増やし、ルール１ａは“ＩＤＬＥ”になる。最終的には仕様はすべて“ＩＤＬＥ”になり仕様は（“△”、“△”、“○”）から（“○”、“○”、“○”）となる。また評価回数は（０，０，０、）から（１，１，０）となる。ルール２は信頼性の高い仕様にもかかわらず１回も通過していないので、検証シナリオ１２０が不足していることが分かる。
【実施例２】
【０１１７】
実施例２は、仕様が曖昧なため、ある入力パターンに対して出力パターンが２種類（１ａ，１ｂ）考えられるが、場合により双方の出力パターンが出力されることはありえず、必ずどちらか一方の出力パターンで出力されることは分かっている場合の期待値リストである。図１１は、実施例２の期待値リストであり、図１２は、実施例２のタイムチャートである。
【０１１８】
時刻ｔ１にてルール１ａ，１ｂの入力パターンが検出されたためルール１ａ，１ｂが“ＡＣＴＩＶＥ”になる。時刻ｔ２において、ルール１ａは出力パターンとは違うものが現れたので不一致、ルール１ａの不一致処理を行い仕様が消去（仕様が曖昧（“△”）→無効（“−”））される。
【０１１９】
時刻ｔ３でルール１ｂの入力パターンが検出されたためルール１ｂの一致処理が行われ仕様を“○”に書き換える。その後一致データ（３データ）をデータバッファから取り除く。そしてルール１ｂの評価回数を１増やし、ルール１ｂは“ＩＤＬＥ”になる。時刻ｔ４においてルール１ｂの入力パターンが検出されたためルール１ｂが“ＡＣＴＩＶＥ”になる。ルール１ａは消去されているので“ＡＣＴＩＶＥ”にならない。
【０１２０】
時刻ｔ５において、ルール１ｂの入力パターンでないものが抽出されたので不一致処理が行われ仕様が曖昧（“△”）でなく、また、“ＡＣＴＩＶＥ”なペアルールもないため、ＲＴＬバグとして異常終了する。
【実施例３】
【０１２１】
実施例３は、タイムアウトの例である。図１３は、実施例３の期待値リストであり、図１４は、実施例３のタイムチャートである。時刻ｔ１にてルール２の入力パターンが検出されたため、ルール２の状態が“ＡＣＴＩＶＥ”になる。時刻ｔ２にて出力パターンが検出される前に最大時間に達したため、タイムアウト処理を行う。これにより、ＲＴＬバグと判断され、シミュレーションは停止する。
【０１２２】
このように、上述した実施の形態（実施例１〜３を含む）では、１回の論理シミュレーションで多くの曖昧な仕様を明確にできるため、論理シミュレーションのやり直しが必要なくなる。また、検証対象１００の内部状態により出力が変わる非決定な仕様でも検証が可能である。さらに、どの仕様を何回検証したかという仕様カバレジ（評価回数）も出力でき、検証シナリオ１２０の網羅性を確認できる。また、結果判定がＯＫ／ＮＧだけでなく、ＮＧの場合にはさらにＲＴＬまたは検証シナリオ１２０のいずれが誤っているかを人手なしに判断することができる。
【０１２３】
以上のことから、この実施の形態にかかる論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法によれば、検証の容易化により、検証者の労力軽減および検証期間の短縮化を図ることができるという効果を奏する。
【０１２４】
なお、本実施の形態で説明した論理仕様検証方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な伝送媒体であってもよい。
【０１２５】
また、本実施の形態で説明した論理仕様検証装置３００は、スタンダードセルやストラクチャードＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）などの特定用途向けＩＣ（以下、単に「ＡＳＩＣ」と称す。）やＦＰＧＡなどのＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）によっても実現することができる。具体的には、たとえば、上述した論理仕様検証装置３００の機能（機能ブロックの各符号を入れる）をＨＤＬ記述によって機能定義し、そのＨＤＬ記述を論理合成してＡＳＩＣやＰＬＤに与えることにより、論理仕様検証装置３００を製造することができる。なお、上述した実施の形態に関し、さらに以下の付記を開示する。
【０１２６】
（付記１）コンピュータを、
検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得手段、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出手段、
前記検出手段によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定手段、
前記入力パターン判定手段によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定手段、
前記検出手段によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定手段、
前記出力パターン判定手段によって判定された判定結果に基づいて、前記特定手段によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更手段、
前記変更手段によって変更結果を出力する出力手段、
として機能させることを特徴とする論理仕様検証プログラム。
【０１２７】
（付記２）前記変更手段は、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が正確であることをあらわす第２の信頼度に変更することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１２８】
（付記３）前記コンピュータを、
前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定された回数に基づいて、前記仕様の評価値を算出する算出手段として機能させ、
前記出力手段は、
前記算出手段によって算出された算出結果を出力することを特徴とする付記１または２に記載の論理仕様検証プログラム。
【０１２９】
（付記４）前記検証ルールには、前記出力パターン判定手段によって一致すると判定された場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに出力してはいけない出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の成立禁止をあらわす第３の信頼度に設定されている場合、前記出力パターン判定手段によって一致すると判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３０】
（付記５）前記変更手段は、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって不一致であると判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が無効であることをあらわす第４の信頼度に変更することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３１】
（付記６）前記検証ルールには、前記出力パターン判定手段によって不一致であると判定された場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって不一致であると判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３２】
（付記７）前記検証ルールには、前記出力パターン判定手段によって不一致であると判定された場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記出力パターン判定手段によって不一致であると判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３３】
（付記８）前記変更手段は、
前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記仕様の信頼度を、前記第１の信頼度から、前記仕様が無効であることをあらわす第４の信頼度に変更することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３４】
（付記９）前記検証ルールには、前記出力パターン判定手段による判定がタイムアウトになった場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が当該仕様の曖昧さをあらわす第１の信頼度に設定されている場合、前記出力パターン判定手段によって、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３５】
（付記１０）前記検証ルールには、前記出力パターン判定手段による判定がタイムアウトになった場合の解析原因が設定されており、
前記コンピュータを、
前記出力パターンに期待値となる出力パターンが設定され、かつ、前記仕様の信頼度が、当該仕様が正確であることをあらわす第２の信頼度に設定されている場合、前記出力パターン判定手段によって、前記検証対象から出力されるパターンが、前記仕様に関する設定時間内に検出されなかったと判定されると、前記解析原因ありと決定する決定手段として機能させ、
前記出力手段は、
前記決定手段によって決定された決定結果を出力することを特徴とする付記１に記載の論理仕様検証プログラム。
【０１３６】
（付記１１）前記解析原因は、前記検証対象のＲＴＬ記述に関するバグまたは前記仕様の検証シナリオバグであることを特徴とする付記４、６、７、または９のいずれか一つに記載の論理仕様検証プログラム。
【０１３７】
（付記１２）前記検出手段は、
前記特定手段によって特定された検証ルールに設定されている仕様が、当該仕様が無効であることをあらわす第４の信頼度に設定されている場合、前記検証対象から出力されるパターンの検出を禁止することを特徴とする付記５または８に記載の論理仕様検証プログラム。
【０１３８】
（付記１３）検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得手段と、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出手段と、
前記検出手段によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定手段と、
前記入力パターン判定手段によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定手段と、
前記検出手段によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定手段と、
前記出力パターン判定手段によって判定された判定結果に基づいて、前記特定手段によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更手段と、
前記変更手段によって変更結果を出力する出力手段と、
を備えることを特徴とする論理仕様検証装置。
【０１３９】
（付記１４）検証対象に対する入力パターンおよび出力パターンとその仕様の信頼度とが設定された検証ルールの集合を取得する取得工程と、
前記検証対象に入力されるパターンと、当該パターンが入力された結果、前記検証対象から出力されるパターンとを検出する検出工程と、
前記検出工程によって検出された前記検証対象に入力されるパターンと一致する入力パターンが前記集合内にあるか否かを判定する入力パターン判定工程と、
前記入力パターン判定工程によって一致すると判定された入力パターンに関する検証ルールを前記集合の中から特定する特定工程と、
前記検出工程によって検出された前記検証対象から出力されるパターンと一致する出力パターンが前記集合内にあるか否かを判定する出力パターン判定工程と、
前記出力パターン判定工程によって判定された判定結果に基づいて、前記特定工程によって特定された検証ルールに設定されている前記仕様の信頼度を変更する変更工程と、
前記変更工程によって変更結果を出力する出力工程と、
を含んだことを特徴とする論理仕様検証方法。
【産業上の利用可能性】
【０１４０】
以上のように、論理仕様検証プログラム、論理仕様検証装置、および論理仕様検証方法は、ＬＳＩなどのハードウェアの論理仕様の検証に有用である。
【図面の簡単な説明】
【０１４１】
【図１】本実施の形態にかかる論理仕様検証の概要を示す説明図である。
【図２−１】図１に示した期待値リストを示す説明図である。
【図２−２】小項目への“○”の付け方のバリエーション例を示す説明図である。
【図３】論理仕様検証装置のハードウェア構成を示す説明図である。
【図４】論理仕様検証装置の機能的構成を示すブロック図である。
【図５】実施の形態にかかる論理仕様検証処理手順を示すフローチャートである。
【図６】一致処理（ステップＳ５０８）の詳細な処理手順を示すフローチャートである。
【図７】不一致処理（ステップＳ５１０）の詳細な処理手順を示すフローチャートである。
【図８】タイムアウト処理（ステップＳ５１２）の詳細な処理手順を示すフローチャートである。
【図９】実施例１の期待値リストである。
【図１０】実施例１のタイムチャートである。
【図１１】実施例２の期待値リストである。
【図１２】実施例２のタイムチャートである
【図１３】実施例３の期待値リストである。
【図１４】実施例３のタイムチャートである。
【符号の説明】
【０１４２】
１００  検証対象
１３０  期待値リスト
１４０  テストベンチ
１５０  論理シミュレータ
１５１  結果判定ログ
３００  論理仕様検証装置
４０１  取得部
４０２  検出部
４０３  入力パターン判定部
４０４  特定部
４０５  出力パターン判定部
４０６  変更部
４０７  出力部
４０８  算出部
４０９  決定部
【図１】
2009110417.tif 000003
【図２−１】
2009110417.tif 000004
【図２−２】
2009110417.tif 000005
【図３】
2009110417.tif 000006
【図４】
2009110417.tif 000007
【図５】
2009110417.tif 000008
【図６】
2009110417.tif 000009
【図７】
2009110417.tif 000010
【図８】
2009110417.tif 000011
【図９】
2009110417.tif 000012
【図１０】
2009110417.tif 000013
【図１１】
2009110417.tif 000014
【図１２】
2009110417.tif 000015
【図１３】
2009110417.tif 000016
【図１４】
2009110417.tif 000017