(57)【要約】【課題】  検証未実施のアサーションを実施させるべくテストを生成し、アサーションを実施可能とする。【解決手段】  ハードウェア記述言語で記述された論理システムの検証に用いるアサーションの中から検証未実施のアサーションを抽出する。ハードウェア記述言語で記述された論理システムを有限状態機械に変換し、抽出された検証未実施のアサーションを内部の表現に変換する。有限状態機械の状態遷移を辿り、内部表現の前提条件が含む有限状態機械の状態を求め、有限状態機械の状態と状態遷移とに基づき、検証未実施のアサーションを実施させるためのテストを生成する。【選択図】      図３
2008033691.tif 000002
【特許請求の範囲】
【請求項１】
ハードウェア記述言語により記述された論理システムの論理検証を行う論理検証装置であって、
前記論理システムの検証に用いるアサーションの中から、検証未実施のアサーションを抽出する抽出手段と、
前記論理システムの設計データを有限状態機械に変換する変換手段と、
前記抽出手段で抽出された検証未実施のアサーションを内部の表現に変換する内部表現変換手段と、
前記有限状態機械の状態遷移を辿り、前記内部表現の前提条件が含む前記有限状態機械の状態を求める手段と、
前記有限状態機械の状態と前記有限状態機械の状態遷移とに基づき、前記検証未実施のアサーションを実施させるためのテストを生成するテスト生成手段とを有することを特徴とする論理検証装置。
【請求項２】
前記抽出手段は、
前記論理システムの設計データを有限状態機械に変換する手段と、
前記論理システムの検証に用いるアサーション記述毎に内部表現に変換する手段と、
前記有限状態機械の状態遷移を辿り、前記内部表現が成立する条件が含む前記有限状態機械の状態を前記内部表現毎に求める第１の手段と、
テストに従って前記有限状態機械を用いて前記論理システムの論理シミュレーションを実施し、論理シミュレーションした前記有限状態機械の状態を前記テスト毎に求める第２の手段と、
前記第１及び第２の手段により求めた状態の包含関係を判定する判定手段と、
前記判定手段での判定結果に応じて、十分な検証が実施できないアサーションとテストの組み合わせを出力する出力手段とを有することを特徴とする請求項１に記載の論理検証装置。
【請求項３】
ハードウェア記述言語により記述された論理システムの論理検証を行う論理検証装置の検証方法であって、
前記論理システムの検証に用いるアサーションの中から、検証未実施のアサーションを抽出する抽出工程と、
前記論理システムの設計データを有限状態機械に変換する変換工程と、
前記抽出工程で抽出された検証未実施のアサーションを内部の表現に変換する内部表現変換工程と、
前記有限状態機械の状態遷移を辿り、前記内部表現の前提条件が含む前記有限状態機械の状態を求める工程と、
前記有限状態機械の状態と前記有限状態機械の状態遷移とに基づき、前記検証未実施のアサーションを実施させるためのテストを生成するテスト生成工程とを有することを特徴とする論理検証装置の検証方法。
【請求項４】
請求項３に記載の論理検証装置の検証方法をコンピュータに実行させるためのプログラム。
【請求項５】
請求項４に記載のプログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウェア記述言語により記述された論理システムを論理検証する技術に関する。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年々増加している。これに伴い、論理システムの検証にかかる工数も増加している。一方、市場には消費者が欲するときに製品を投入しなければならず、ＬＳＩを始めとする論理システムの開発期間は短くなっている。そのため、論理システム検証の効率向上を図る必要が生じている。
【０００３】
現在、ＬＳＩを含む論理システムの検証は、論理シミュレータを用いて論理システムを動作させて検証を実施する「論理シミュレーション」が主流である。論理シミュレータ上で、検証対象（以下、ＤＵＴ：Design Under Test）を擬似的に動かし、論理シミュレーションを実施してＤＵＴの内部状態や出力の値を求める。そして、求めたＤＵＴの出力と期待値を論理シミュレータで、或いは別の方法で比較し、ＤＵＴの動作を確認する。
【０００４】
しかし、ＤＵＴの出力と期待値を比較するだけでは検証は十分ではない。ＤＵＴの入出力が仕様通りに動作しているかは、ＤＵＴの出力と期待値を比較するだけでははっきりしないからである。そのため、信号値の観測、或いは比較だけではなく、仕様通りに動作しているかを何らかの方法で確認する必要がある。
【０００５】
この問題を解決すべく、論理シミュレーション実行時、仕様が意図する動作とＤＵＴの動作を比較する機構を用いる手法が使用されている。この機構は、ＤＵＴの動作を監視し、仕様が意図する動作と異なる動きをＤＵＴがしたならば、警告を発する。ここで、仕様が意図する動作の記述を、一般に「アサーション」、或いは「プロパティ」と呼ぶ。この２つの用語は検証手法により使い分けられることが多い。即ち、「アサーション」は論理シミュレータを用いた論理シミュレーションで、「プロパティ」は数学的に仕様とＤＵＴの一致性を判定する静的検証で用いることが多い。
【０００６】
本発明でも、「アサーション」といった場合、論理シミュレーションに限定する。このアサーションを用いて、論理シミュレーションでＤＵＴの検証を実施する手法を「アサーションベース検証」と呼ぶ。このアサーションベース検証は公知の技術である。例えば、非特許文献１、非特許文献２、非特許文献３に、アサーションベース検証に関して詳細な説明がある。
【０００７】
アサーションの記述には、ＨＤＬ（Hardware Description Language）やアサーション記述専用言語を用いる。本発明で解決すべき課題は、アサーションベース検証そのものに起因し、アサーション記述言語に依存するものではない。そこで、時相論理を基にした、仮のアサーション記述言語を用いて本発明を説明する。以下に、本アサーション記述言語が持つ演算子の抜粋を示す。
【０００８】
｜｜  ：  論理和（ＯＲ）
＆＆  ：  論理積（ＡＮＤ）
＝＝  ：  論理等価（equivalence）
‘ｂ  ：  二進数（binary number）
‘Ｘ  ：  次サイクル
＝＞  ：  含意（Implication）
ここで、命題論理や時相論理と同じく、含意演算子“＝＞”の左辺を前提、右辺を帰結と呼ぶ。前提は、アサーションを成立させる条件である。前提が成り立ち、帰結の評価を始めることを「アサーションが発火する」と表現する。このアサーション記述言語では、「信号ａと信号ｂの何れかが‘ｂ１ならば、次のサイクルで信号ｃは’ｂ１である。」という仕様は、以下のように記述する。
【０００９】
（ａ＝＝‘ｂ１）｜｜（ｂ＝＝’ｂ１）  ＝＞  ‘Ｘ（ｃ＝＝’ｂ１）
アサーションをＤＵＴやテストと共に論理シミュレータが読み込み、論理シミュレーションを実施する。論理シミュレーションを実行中に、アサーションが発火すると、論理シミュレータは帰結を評価する。帰結の評価が偽ならば、ＤＵＴの動作と仕様が意図する動作が異なっている。この場合、論理シミュレータは、アサーションの識別子及び発生時刻と共に「アサーション違反あり」を出力する。
【００１０】
反対に、帰結の評価結果が真ならば、ＤＵＴの動作と仕様が意図する動作が一致している。この場合、論理シミュレータは、アサーションの識別子及び発生時刻と共に「アサーション違反なし」を出力する。「アサーション違反がある場合、アサーション識別子と発生時刻を基にＤＵＴの誤りを解析する。アサーション識別子よりＤＵＴの期待する動作が明らかであり、その上違反発生時刻が明らかであるので、アサーションベース検証を用いない場合と比較して、容易にＤＵＴの誤りを発見することが可能となる。
【００１１】
上記アサーションを例にとると、信号ａ或いは信号ｂが‘ｂ１であるのにも係わらず、次のサイクルで信号ｃが’ｂ０ならば、帰結の評価は偽である。よって、「アサーション違反あり」が報告される。反対に次のサイクルで信号ｃが‘ｂ１ならば、帰結の評価は真である。よって、「アサーション違反なし」が報告される。
【００１２】
しかし、アサーションベース検証を用いたからといって、必ずしも検証精度が向上するわけではない。仕様を正しく解釈し、かつ仕様に忠実に記述したアサーションを用いても、使い方によっては却って検証精度を低下させることもある。なぜならば、アサーションが正しく発火しなければ、帰結の評価結果が正しいとは言い切れないからである。従って、アサーション違反が無いことを理由にＤＵＴに誤りが無いと判断することは、ＤＵＴの誤りを見逃す原因になり得る。
【００１３】
アサーションが正しく発火しないため、ＤＵＴの誤りを見逃す事例を次に示す。アサーションとしては、以下を例に挙げる。
【００１４】
（ａ＝＝‘ｂ１）｜｜（ｂ＝＝’ｂ１）  ＝＞  ‘Ｘ（ｃ＝＝’ｂ１）
これに対して、例えば以下のようなテストが用意されていたとする。
【００１５】
テスト[１]：信号a、信号ｂ共に‘ｂ0
即ち、テスト[１]実行中は信号a、信号ｂ共‘ｂ１にならない
テスト[１]は、アサーションの前提｛（ａ＝＝‘ｂ１）｜｜（ｂ＝＝’ｂ１）｝が成立しないので、期間の評価を実施せず、その結果、論理シミュレータは「アサーション違反あり」を報告しない。アサーションの前提条件を満たしていないテストしか実施していない状態は、結局はテストを実施していないのと同等である。つまり、これは「アサーション違反なし」ではなく、検証未実施である。そのため、このアサーションに対して検証を実施するべくテストを流す必要がある。
【００１６】
また、論理シミュレーションの主な手法として、ランダム手法とダイレクト手法がある。ランダム手法は、ＤＵＴに対して乱数を使用して無作為にテストを生成し、そのテストを実行する手法である。この手法を用いることにより、人間が考え付くことのできないテストを生成することが可能となり、コーナーケースバグの発見につながる。
【００１７】
一方、ダイレクト手法はＤＵＴに対して実施したいテストを人間が考えて記述し、そのテストを実行する手法である。この手法を用いることにより、テストしたい項目を確実に検証することが可能となる。
【００１８】
論理シミュレーションのランダム手法においてアサーションベース検証を実行した場合に、未発火のアサーションがあったとする。例えば、上述のアサーションに対して、上記テスト[１]が実施されたときである。このアサーションを引き続きランダムシミュレーションで検証する場合、当該アサーションを実施するようなテストがいつ実施されるのか不明である。また、ダイレクト手法を用いて未発火のアサーションを実施するべくテスト作成しようとしても、どのようなテストを作成すればよいのか分からない。
【００１９】
それゆえ、未発火のアサーションが存在する場合は、ランダム手法を用いて当該アサーションが発火するまで待つしか方法がなかった。また、仮に長時間シミュレーションを実行し続けたとしても、アサーションが発火するという保証はない。アサーションが発火しないことは、その部分において検証を実施していないのと同様であり、バグが潜んでいる可能性が高い。
【００２０】
また、当該アサーションが本当に実行可能な前提条件となっているかは不明である。論理シミュレーションの実行時間に与える影響は大きい。非特許文献１によれば、アサーションを用いた場合の影響は、論理シミュレーション時間の２０％にも達する。評価のショートカットをせず、アサーション発火条件の全ての項を評価するとなると、論理シミュレーション時間に与える影響は増加し、論理シミュレーションの実施時間が延びる。その上、アサーション発火の条件が含む項全てを評価するまで、論理シミュレーションを繰り返すため、検証時間が増加する。
【非特許文献１】浜口清治著、“アサーションベース検証の基礎とそのねらい”、情報処理学会研究報告、2005-SLDM-118(6):29-34、2005
【非特許文献２】温兆祺、吉永和弘著、“アサーションベース検証”、情報処理、Vol45,No.5:477-483,2004
【非特許文献３】H.D.Foster,A.C.Krolnik,D.J.Lacey,"Assertion-Based Design,2nd Edition",Kluwer Academic Publishers,2004.
【発明の開示】
【発明が解決しようとする課題】
【００２１】
即ち、正しくアサーションを記述して長時間論理シミュレーションを実施したとしても、十分な精度が得られるとは限らない。また、長時間論理シミュレーションを実施したとしても、そのアサーションが本当に必要なアサーションであるとは限らない。
【００２２】
本発明は、検証未実施のアサーションを実施させるべくテストを生成し、アサーションを実施可能とすることを目的とする。
【課題を解決するための手段】
【００２３】
本発明は、ハードウェア記述言語により記述された論理システムの論理検証を行う論理検証装置であって、前記論理システムの検証に用いるアサーションの中から、検証未実施のアサーションを抽出する抽出手段と、前記論理システムの設計データを有限状態機械に変換する変換手段と、前記抽出手段で抽出された検証未実施のアサーションを内部の表現に変換する内部表現変換手段と、前記有限状態機械の状態遷移を辿り、前記内部表現の前提条件が含む前記有限状態機械の状態を求める手段と、前記有限状態機械の状態と前記有限状態機械の状態遷移とに基づき、前記検証未実施のアサーションを実施させるためのテストを生成するテスト生成手段とを有することを特徴とする。
【００２４】
また、本発明は、ハードウェア記述言語により記述された論理システムの論理検証を行う論理検証装置の検証方法であって、前記論理システムの検証に用いるアサーションの中から、検証未実施のアサーションを抽出する抽出工程と、前記論理システムの設計データを有限状態機械に変換する変換工程と、前記抽出工程で抽出された検証未実施のアサーションを内部の表現に変換する内部表現変換工程と、前記有限状態機械の状態遷移を辿り、前記内部表現の前提条件が含む前記有限状態機械の状態を求める工程と、前記有限状態機械の状態と前記有限状態機械の状態遷移とに基づき、前記検証未実施のアサーションを実施させるためのテストを生成するテスト生成工程とを有することを特徴とする。
【発明の効果】
【００２５】
本発明によれば、いつ実施できるか分からなかったアサーションを確実に実施することが可能となる。これにより、シミュレーション時間を短縮でき、検証工数の削減が可能となる。
【００２６】
また、本発明によれば、実施できなかった可能性のあるアサーションを確実に実施することが可能となる。従って、検証精度が向上し、市場が欲するときに十分な精度を持った製品を投入することが可能となる。
【発明を実施するための最良の形態】
【００２７】
以下、図面を参照しながら発明を実施するための最良の形態について詳細に説明する。
【００２８】
図１は、本実施形態におけるテストを生成する方法を説明するための図である。図１において、１０１は仕様であり、論理システムの仕様が記載されたデータである。尚、後述する設計データやテスト、及びアサーションは、全て仕様１０１のデータに基づいて作成される。また、仕様１０１は書式に依存したものではなく、自然言語、その他、如何なる言語や書式で記述されていてもかまわない。
【００２９】
１０２はＤＵＴであり、論理システムの設計データである。このＤＵＴ１０２は、論理検証装置によって論理検証が行われる検証対象である。ＤＵＴ１０２の記述は、後述する有限状態機械変換器が理解できる形式であれば、何を用いても良いが、ここでは、ＨＤＬで記述しているものとする。
【００３０】
１０３は有限状態機械変換器であり、ＤＵＴ１０２を後述する有限状態機械（ＦＳＭ：Finite State Machine）に変換する機能を有する。原則的に、同期式順序回路は有限状態機械で表わすことが可能である。そのため、論理システムの設計及び検証において、有限状態機械を用いる方法は広く用いられている。
【００３１】
尚、本発明は、ＤＵＴ１０２を有限状態機械に変換するアルゴリズムに依存するものではないので、どの変換アルゴリズムを用いても良い。また、有限状態機械変換器１０３により変換された有限状態機械はムーア型、ミーリ型の何れでも良い。
【００３２】
１０４は有限状態機械であり、その表現形式にはＢＤＤ（Binary Decision Diagram）、状態遷移図、状態遷移表などがある。勿論、有限状態機械１０４は表現形式に依存するものではなく、同一の論理関数が同一の表現になるならばどのような表現を用いて良い。ところが、ＤＵＴ１０２の内部状態が多くなると、有限状態機械１０４の状態数はＤＵＴ１０２が含むフリップ・フロップの値が取り得る組み合わせ数になるため、２０ｂｉｔのレジスタであれば２の２０乗の状態、つまり約百万状態になる。そのため、状態遷移図や状態遷移表ではなく、ＢＤＤを用いて有限状態機械を非明示的に表現する手法が広く使われている。しかし、本実施形態では、説明が容易であることからＢＤＤを用いずに、状態遷移図を用いて説明する。
【００３３】
図２は、有限状態機械１０４の一例を状態遷移図として示す図である。図２において、Ｓｎ、Ｓｎ＋１、…、Ｓｎ＋１１は有限状態機械１０４の状態を表し、矢印は状態遷移の方向を表している。
【００３４】
ここで、図１に戻り、１０５はテスト・レポート生成器であり、ＤＵＴ１０２に対して実施したアサーションベース検証に基づき、アサーションの発火状況をリストアップする機能を有する。
【００３５】
尚、発火、或いは未発火のアサーションが抽出できるものであれば、どのようなテスト・レポートを生成しても良い。また、本発明は、検証未実施アサーションを探索する方法に関するものではないので、どのような手法を用いても良い。
【００３６】
１０６は検証未実施アサーションであり、テスト・レポート生成器１０５によって抽出された検証未実施のアサーションの集合である。１０７は内部表現変換器であり、検証未実施アサーション１０６を後述する内部表現に変換する機能を有する。アサーション記述言語は高級言語に近いため、人間にとっては取り扱いが容易であるが、後述する到達可能状態抽出器が取り扱うには不便である。
【００３７】
そこで、内部表現変換器１０７によって検証未実施アサーション１０６を後述する到達可能状態抽出器が取り扱い易い形式に変換する。１０８は内部表現変換器１０７によって変換された検証未実施アサーションの内部表現である。本発明は、内部表現の形式に依存したものではないので、到達可能状態抽出器が取り扱える形式であれば内部表現１０８は何を用いても良い。例えば、内部表現１０８としてＣＴＬ（Computation Tree Logic）を用いることができる。
【００３８】
ＣＴＬは、時相論理の一つである。ＣＴＬは、通常の論理演算子に加え、全称演算子Ａ、存在演算子Ｅ、時相演算子（Ｆ、Ｇ、Ｘ、Ｕ）が存在する。時相演算子Ｆは「いつか」を、時相演算子Ｇは「つねに」を、時相演算子Ｘは「つぎの時刻に」を、時相演算子Ｕは「まで」を表す。
【００３９】
１０９は到達可能状態抽出器であり、有限状態機械１０４と内部表現１０８とを用いて有限状態機械１０４内の節に内部表現１０８が含まれるものが存在するか否かを探索する。１１０は到達可能状態であり、到達可能状態抽出器１０９によって抽出された有限状態機械１０４内の節が記録される。
【００４０】
１１１はテスト生成器であり、到達可能状態１１０をスタート地点とし、有限状態機械１０４の分岐開始地点まで遡り、検証が実施できなかったアサーションを実施するためのテストを生成する。１１２はテストであり、テスト生成器１１１によって生成された、未実施アサーションを実施するためのテストである。
【００４１】
ここで、テスト・レポート生成器１０５によって抽出された検証未実施アサーションと有限状態機械１０４の節に含まれる内部表現に基づいて、未実施アサーションを実施するためのテストを生成する処理を、図３を用いて説明する。
【００４２】
図３は、検証未実施アサーションに基づきテストを生成する処理を示すフローチャートである。まず、ステップＳ３０１では、内部表現変換器１０７がテスト・レポート生成器１０５によって生成された検証未実施アサーション１０６を一つずつ取り出す。そして、ステップＳ３０２で、内部表現変換器１０７が検証未実施アサーション１０６を到達可能状態抽出器１０９で取り扱える形式の内部表現１０８に変換する。これは、アサーションを記述するアサーション記述言語及びＤＵＴを記述するハードウェア記述言語は高級言語に近いため、それぞれを比較可能な形に変換する必要があるためである。上述したように、ここでは検証未実施アサーション１０６の内部表現１０８としてＣＴＬを用いる。
【００４３】
次に、ステップＳ３０３では、到達可能状態抽出器１０９が有限状態機械１０４の節に含まれる内部表現１０８を探索する。即ち、ＤＵＴ１０２を有限状態機械１０４に変換したものの中から、ステップＳ３０２でＣＴＬに変換したアサーションの内部表現１０８を含むものを、有限状態機械１０４を辿って探索する。
【００４４】
次に、ステップＳ３０４では、有限状態機械１０４内に内部表現１０８が含まれる節が有るか否かを判定する。アサーションの内部表現１０８が成り立っても成り立たなくとも、通過する状態があれば、即ち前提条件が成り立っていればステップＳ３０５へ分岐し、通過する状態がなければステップＳ３０６へ分岐する。この「通過する状態」については更に後述する。
【００４５】
ステップＳ３０５では、有限状態機械１０４の節のうちアサーションの内部表現１０８を含む節に印を付ける。そして、ステップＳ３０７で、有限状態機械１０４の節のうち、印を付けた節をスタート地点として分岐開始地点まで遡り、印を付けた節を通過するようなテスト１１２を生成する。尚、このテスト１１２を生成する方法については、更に後述する。
【００４６】
一方、ステップＳ３０６では、内部表現１０８が含まれる節がないアサーションは実施不可能アサーションとして記録する。尚、この実施不可能アサーションについては、更に後述する。
【００４７】
次に、ステップＳ３０８では、テスト・レポート生成器１０５で生成された検証未実施アサーションに残りが有るか否かを判定する。ここで、有ればステップＳ３０１へ分岐し、無ければ、この処理を終了する。
【００４８】
尚、ステップＳ３０１で抽出される検証未実施アサーション１０６には、ＤＵＴ１０２に対してアサーションベース検証を実施した結果、アサーションを通過したか、一部通過していない部分があるか、全く通過していないかなどが記述されている。
【００４９】
ここで、テスト・レポート生成器１０５の構成、及び検証未実施アサーション１０６の一例を、図４を用いて説明する。
【００５０】
尚、本発明は検証未実施アサーション１０６を抽出する方法に関するものではないため、検証未実施アサーション１０６の抽出方法は如何なるものでもかまわない。
【００５１】
図４は、図１に示すテスト・レポート生成器１０５の構成の一例を示す図である。尚、図１と同じものには同一の符号を付し、その説明は省略する。
【００５２】
テスト・レポート生成器１０５において、アサーション４０１は、ＤＵＴ１０２の仕様を定義したアサーションの集合である。尚、本発明は、唯一のアサーションに限ったものではないため、複数のアサーションが含まれる。また、アサーションの記述にはＨＤＬ、時相論理による論理式、時相論理にマクロや関数の仕様を追加したアサーション記述言語を用いることが可能である。本発明は、アサーション記述言語や記述形式に依存するものではないので、仕様１０１を必要かつ十分に定義可能ならば、アサーション記述にはどのような記述言語、記述形式を用いても良い。ここで、本実施形態では、先に定義した仮のアサーション記述言語を用いて説明する。
【００５３】
アサーション４０１の書式には、ＤＵＴ１０２のＨＤＬ記述内に注釈行でアサーション４０１を埋め込む形式と、アサーション４０１のみＤＵＴ１０２とは別に定義する形式がある。尚、本発明は、アサーションの書式に依存するものではないので、どちらの形式を用いても良い。
【００５４】
ここで、ＤＵＴ１０２のＨＤＬ記述内に注釈行で埋め込む形式を用いた場合は、ＤＵＴ１０２からアサーションの部分を抽出し、アサーション４０１とする処理が必要となる。このアサーション抽出を行うアサーション抽出部は図４では不図示である。
【００５５】
一方、アサーション４０１のみ別に定義する形式を用いた場合は、別に定義したアサーションをアサーション４０１とする。勿論、ＤＵＴ１０２のＨＤＬ記述内に注釈行で埋め込む形式と、アサーション４０１のみＤＵＴ１０２とは別に定義する形式とを併用しても良い。その場合、ＤＵＴ１０２に埋め込んだアサーションをアサーション抽出部で抽出し、別に定義したアサーションと結合してアサーション４０１とする。
【００５６】
アサーション抽出部は、ＤＵＴ１０２からアサーション記述を抽出する。ＤＵＴ１０２はＨＤＬで記述されているので、正規表現を用いたテキスト処理で抽出可能である。この処理は、ＰｅｒｌやＡＷＫといったスクリプト言語で記述することが可能である。勿論、スクリプト言語による処理に限ったものではなく、Ｃ言語等で処理プログラムを記述しても良い。図５は、Ｐｅｒｌによるアサーション抽出部の一例を示す図である。
【００５７】
テスト４０２は、ＤＵＴ１０２の論理シミュレーションに用いるテストである。本発明は、テストの構成に依存するものではないので、どのような手法を用いても良い。また、ランダム・テストであっても、シナリオ・テストであっても良い。そして、テストを記述する言語も問わない。
【００５８】
内部表現変換器４０３は、アサーション４０１内のアサーションを、アサーション毎、アサーション内部表現４１１に変換する。ここでは、内部表現変換器４０３は図１に示す内部表現変換器１０７と同様のものとする。
【００５９】
次に、アサーション発火条件収集器４０４は、アサーションが発火する条件が含む有限状態機械１０４の状態をアサーション内部表現４１１と有限状態機械１０４から求める。ここでは、有限状態機械１０４を初期状態から全ての状態を巡り、各状態でアサーション発火条件が当該状態を含んでいるかを調べる。アサーションが発火するか否かは問わず、アサーション発火条件が当該状態を含んでいるならば、当該状態に印を付ける。そして、全ての状態を巡った後、印が付いている有限状態機械１０４の状態を収集し、集合とする。このとき、印が付いている有限状態機械１０４の状態が存在しなければ、アサーション番号のみからなる集合にする。
【００６０】
このようにして収集した集合を、アサーション発火条件が含む状態４１２の新たな元として追加する。これを全てのアサーションについて繰り返す。
【００６１】
図６は、あるアサーションについて全ての状態を巡った後の有限状態機械１０４の一例を示す図である。図６に示す６０１、６０２の状態、即ち、Ｓｎ＋３，Ｓｎ＋４，Ｓｎ＋８はアサーション発火条件が含む状態である。状態の集合、｛Ｓｎ＋３，Ｓｎ＋４，Ｓｎ＋８｝が新たな元として、アサーション発火条件が含む状態４１２に追加される。
【００６２】
図４に戻り、到達状態収集器４０５は、テスト４０２で到達可能な有限状態機械１０４の状態を求める。テスト４０２に従って、有限状態機械１０４を初期状態から遷移させ、通過した状態に印を付ける。このとき、アサーションが発火するか否かは問わない。このテスト４０２を終了後、印が付いている有限状態機械１０４の状態を収集し、集合とする。このようにして収集した集合を、到達状態４１３に新しい元として追加する。そして、これを全てのテスト実行時に実施する。
【００６３】
図７は、あるテストを動的シミュレータで実行後の有限状態機械１０４の一例を示す図である。図７に示す７０１の状態、即ち、Ｓｎ，Ｓｎ＋２，Ｓｎ＋５，Ｓｎ＋７，Ｓｎ＋１１がテストで巡った状態である。この状態の集合、｛Ｓｎ，Ｓｎ＋２，Ｓｎ＋５，Ｓｎ＋７，Ｓｎ＋１１｝が新たな元として、到達状態４１３に追加される。
【００６４】
尚、本実施形態では、到達状態収集器４０５で有限状態機械１０４の状態を遷移させて到達状態４１３を収集しているが、本発明はこの収集方法に限ったものではない。
【００６５】
図４に戻り、次に、アサーション・テスト解析器４０６でアサーション４０１とテスト４０２の組み合わせを分類・解析する。まず、アサーション・テスト解析器４０６では、アサーション４０１とテスト４０２の組を、以下に示す基準で分類結果集合Ａ，Ｂ，Ｃ，Ｚの４種類に分類する。
【００６６】
Ａ：当該アサーションが発火する全ての状態を当該テストが満たす
Ｂ：当該アサーションが発火する一部の状態を当該テストが満たさない
Ｃ：当該アサーションが発火するどの状態も当該テストが満たさない
Ｚ：ＤＵＴ１０２内にアサーションが発火する条件が存在しない。
【００６７】
分類Ａに分類されるアサーション４０１とテスト４０２の組み合わせは、アサーション発火条件に含まれる状態をテスト４０２が全て通過しているので、アサーション発火漏れが生じない。
【００６８】
一方、分類Ｂ及びＣに分類されるアサーション４０１とテスト４０２の組み合わせは、アサーション発火条件に含まれる状態をテスト４０２が全て通過していないので、アサーション発火漏れが生じる。よって、「アサーション違反なし」であっても、ＤＵＴ１０２に誤りが無いとは限らない。
【００６９】
また、分類Ｚに分類されるアサーション４０１はＤＵＴ１０２にアサーション発火条件が存在しないため、アサーション４０１の記述誤り、ＤＵＴ１０２の誤り、或いは冗長なアサーションである。
【００７０】
ここで、アサーション・テスト解析器４０６で、アサーション４０１とテスト４０２の組み合わせを分類・解析する方法の一例を、図８を用いて説明する。
【００７１】
図８は、アサーション・テスト解析器４０６の分類・解析処理を示すフローチャートである。本実施形態では、分類・解析はステップＳ８０１からＳ８１４までの１４の処理で行われる。
【００７２】
尚、アサーション発火条件が含む状態４１２を集合Ｑとし、Ｑの元をＱ［ｉ］とする。ｉはアサーション番号である。また、到達状態４１３を集合Ｒとし、Ｒの元をＲ［ｊ］とする。ｊはテスト番号である。そして、ある集合Ｐがｎ個の元を持つならば、Ｐ［ｉ］をＰの元とし、次の関係が成り立つものとする。ここで、｛｝は空集合である。
【００７３】
０≦ｉ≦ｎ−１ならばＰ［ｉ］∈Ｐ、かつ、ｎ≦ｉならばＰ［ｉ］＝｛｝
まず、ステップＳ８０１で、初期化を行う。アサーション番号を示すカウンタ変数ｉに０を代入（ｉ←０）し、分類結果集合Ａ，Ｂ，Ｃ，Ｚを空にする（Ａ←｛｝、Ｂ←｛｝、Ｃ←｛｝、Ｚ←｛｝）。
【００７４】
次に、ステップＳ８０２で、発火しないアサーションを分類する。Ｑ［ｉ］＝＝ｉ即ち、Ｑの元がアサーション番号に一致するならば、ステップＳ８０３へ分岐し、不一致ならばステップＳ８０４へ分岐する。
【００７５】
ステップＳ８０３では、アサーションを発火させる状態がＤＵＴ１０２中に存在しないので、分類結果集合Ｚにアサーション番号ｉを追加（Ｚ←Ｚ∪ｉ）し、ステップＳ８１２へ進む。
【００７６】
ステップＳ８０４では、テスト番号を示すカウンタ変数ｊに０を代入（ｊ←０）する。そして、ステップＳ８０５では、アサーション発火条件が含む状態Ｑ［ｉ］が、到達状態Ｒ［ｊ］に包含されているか否かを判定する。ここでは、Ｑ［ｉ］⊆Ｒ［ｊ］即ち、アサーション発火条件が含む状態Ｑ［ｉ］が到達状態Ｒ［ｊ］の部分集合ならば、ステップＳ８０６へ分岐し、それ以外はステップＳ８０７へ分岐する。
【００７７】
ステップＳ８０６では、アサーション発火条件が含む状態Ｑ［ｉ］が到達状態Ｒ［ｊ］に包含され、テスト番号ｉのテストはアサーション番号ｊのアサーションが発火条件する状態を全て通過する。よって、アサーション番号ｉとテスト番号ｊの組｛ｉ，ｊ｝をＡに追加（Ａ←Ａ∪｛ｉ，ｊ｝）する。
【００７８】
ステップＳ８０７では、アサーション発火条件が含む状態Ｑ［ｉ］と到達状態Ｒ［ｊ］の積集合を求める。その結果、積集合が空集合ならば、ステップＳ８０８へ分岐し、それ以外はステップＳ８０９へ分岐する。
【００７９】
ステップＳ８０８では、アサーション発火条件が含む状態Ｑ［ｉ］と到達状態Ｒ［ｊ］の積集合が空集合で、テスト番号ｊのテストはアサーション番号ｉのアサーションが発火条件する状態を一つとして通過しない。よって、アサーション番号ｉとテスト番号ｊの組｛ｉ，ｊ｝をＣに追加（Ｃ←Ｃ∪｛ｉ，ｊ｝）する。
【００８０】
ステップＳ８０９では、アサーション発火条件が含む状態Ｑ［ｉ］が到達状態Ｒ［ｊ］に包含されず、アサーション発火条件が含む状態Ｑ［ｉ］と到達状態Ｒ［ｊ］の積集合が空集合でない。即ち、テスト番号ｊのテストはアサーション番号ｉのアサーションが発火条件する状態の一部を通過する。よって、アサーション番号ｉとテスト番号ｊの組｛ｉ，ｊ｝をＢに追加（Ｂ←Ｂ∪｛ｉ，ｊ｝）する。
【００８１】
次に、ステップＳ８１０でテスト番号ｊを更新（ｊ←ｊ＋１）する。そして、ステップＳ８１１で、Ｒ［ｊ］が空集合でなければ、即ちテストがまだ存在するならば、ステップＳ８０５に戻り、上述の判定処理を繰り返す。
【００８２】
また、テストが存在しなければ、ステップＳ８１２へ進み、アサーション番号ｉを更新（ｉ←ｉ＋１）する。そして、ステップＳ８１３で、Ｑ［ｉ］が空集合でなければ、即ちアサーションがまだ存在するならば、ステップＳ８０２に戻り、上述の処理を繰り返す。また、アサーションが存在しなければ、ステップＳ８１４へ進み、アサーションとテストの組の分類・解析結果４０７を出力する。
【００８３】
図９は、アサーション・テスト解析器４０６の分類・解析結果４０７の一例を示す図である。図９では、表形式で分類結果集合Ａ，Ｂ，Ｃ，Ｚの内容を示している。勿論、出力形式は表形式に限ったものではなく、どのような書式を用いても良い。
【００８４】
本実施形態では、図９に示すようなテスト・レポートがある場合は、分類Ｂ及び分類Ｃのテストを抽出し、検証未実施アサーション１０６とする。しかし、テスト・レポートの分類方法に関するものではなく、例えば図９に示す分類Ｂ、分類Ｃ及び分類Ｚが混在しているテスト・レポートであっても、その分類を判定する機能を有する。
【００８５】
上述したステップＳ３０４の判別における「通過する状態がない」というのは、図９に示す分類Ｚのことである。また、「通過する状態がある」というのは、図９に示す分類Ｂ及び分類Ｃのことである。ここで、分類Ｂ及び分類Ｃの取り扱いについて説明する。
【００８６】
分類Ｃは、テストがアサーションを実施していない、つまり、論理シミュレーションにおいてアサーションの前提条件が成立していないことが証明されている。ゆえに、分類Ｃについてはテストを生成する過程に進んで構わない。
【００８７】
分類Ｂは、テストがアサーションの前提条件の一部だけを実行したと分かっているものである。しかし、これは組み合わせによっては、アサーションの前提条件全てを実行したと考えられるものもある。
【００８８】
以下、例を用いて説明する。アサーションの本数は２本、テストの本数は３本とする。また、アサーション発火条件が含む状態４１２の集合Ｑと到達状態４１３の集合Ｒを以下のように仮定する。
【００８９】
Ｑ［０］＝｛Ｓｎ＋１、Ｓｎ＋９｝
Ｑ［１］＝｛Ｓｎ、Ｓｎ＋５、Ｓｎ＋７｝
Ｒ［０］＝｛Ｓｎ、Ｓｎ＋１｝
Ｒ［１］＝｛Ｓｎ、Ｓｎ＋３、Ｓｎ＋４、Ｓｎ＋９｝
Ｒ［２］＝｛Ｓｎ、Ｓｎ＋２、Ｓｎ＋５｝
アサーション［０］は、テスト［０］とテスト［１］にそれぞれアサーション発火条件が含む状態の一部が含まれている。テスト［０］では｛Ｓｎ＋１｝、テスト［１］では｛Ｓｎ＋９｝が含まれているため、テスト［０］とテスト［１］を組み合わせることによりアサーション［０］のアサーション発火条件は全て発火したことになる。従って、テストを追加する必要はない。
【００９０】
一方、アサーション［１］は、テスト［０］、テスト［１］、テスト［２］にそれぞれアサーション発火条件が含む状態の一部が含まれているが、全てのテストにアサーション発火条件が含む状態の一部である｛Ｓｎ＋７｝は含まれない。従って、この部分のテストは不備であり、追加する必要がある。
【００９１】
このように、本実施形態では、上述の判断も実施し、アサーション発火条件が含む状態の中からテストが実施されていない節を洗い出し、それに対して全てのテストを生成するものとする。
【００９２】
ここで、上述したステップＳ３０６で記録される実施不可能アサーションについて説明する。アサーションの本数は２本、テストの本数は２本とする。また、アサーション発火条件が含む状態４１２の集合Ｑと、到達状態４１３の集合Ｒを以下のように仮定する。
【００９３】
Ｑ［０］＝｛０｝
Ｑ［１］＝｛Ｓｎ＋２、Ｓｎ＋４｝
Ｒ［０］＝｛Ｓｎ、Ｓｎ＋１｝
Ｒ［１］＝｛Ｓｎ、Ｓｎ＋１、Ｓｎ＋３｝
アサーション［０］は、ＤＵＴ１０２内にアサーションが発火する条件が存在しない。これは、図９に示す分類Ｚに相当するものである。この場合、アサーション［０］を実施するテストを作ることは不可能である。また、このようなアサーションはＤＵＴ１０２内で起こりえないことが判明している場合は不必要となる。不要なアサーションを含めてシミュレーションを実施することは、検証速度低下の原因ともなる。そのため、実施不可能アサーションと判定された場合、その旨を記録した後にシミュレーションを実施する際に省く。
【００９４】
アサーション［１］は、有限状態機械１０４の節の中にアサーションの内部表現１０８はあるが、テスト［０］及びテスト［１］を用いてもアサーション発火条件が発火しない。これは、図９に示す分類Ｃに相当するものである。これは、単にテストが不十分であることに起因するため、アサーション［１］が発火するようなテストを生成するものとする。
【００９５】
ここで、本実施形態におけるテスト１１２の生成方法を、図１０、図１１を用いて説明する。今、検証未実施アサーション１０６から取り出したアサーションの発火条件が含む状態の集合Ｑが以下の通りとする。
【００９６】
Ｑ［０］＝｛Ｓｎ＋２、Ｓｎ＋８｝
以下の手順で、Ｑ［０］の状態を通過するようなテスト１１２を生成する。
１．Ｑの中で、有限機械状態１０４の分岐開始地点、即ち図１０に示すＳｎから最も遠い節１００１を求める。Ｑ［０］の場合は｛Ｓｎ＋８｝である。
２．上記１．で求めた節からＳｎに向かい状態を辿り、遷移条件とＱに属する節を通過したか否かを記録する。Ｑ[０]の場合、｛Ｓｎ＋２｝を含む通路もあるため、図１１に示すように｛Ｓｎ＋２｝の節に印を付ける。
３．Ｓｎに至る経路が複数あるならば、Ｑに属する節を最も多く通過する経路を選択する。Ｑ［０］において、｛Ｓｎ＋８｝を選択した場合、次のａ）〜ｆ）の経路が検出される。
ａ）｛Ｓｎ＋８、Ｓｎ＋３、Ｓｎ＋１、Ｓｎ｝
ｂ）｛Ｓｎ＋８、Ｓｎ＋４、Ｓｎ＋３、Ｓｎ＋１、Ｓｎ｝
ｃ）｛Ｓｎ＋８、Ｓｎ＋４、Ｓｎ｝
ｄ）｛Ｓｎ＋８、Ｓｎ＋３、Ｓｎ＋１、Ｓｎ＋２、Ｓｎ｝
ｅ）｛Ｓｎ＋８、Ｓｎ＋４、Ｓｎ＋３、Ｓｎ＋１、Ｓｎ＋２、Ｓｎ｝
ｆ）｛Ｓｎ＋８、Ｓｎ＋４、Ｓｎ＋２、Ｓｎ｝
この中で、Ｑ［０］に属する節を最も多く通過する経路は、｛Ｓｎ＋２、Ｓｎ＋８｝の両方を含むものである。この場合、両方の節を含むｄ）〜ｆ）のどれを選択しても良い。例えば、ここではｄ）を選択する。
４．上記３．で選択した経路の遷移条件を逆順にし、テスト１１２の入力とする。この例においては、上記３．でｄ）を選択したので、テスト１１２は以下のようになる。
【００９７】
Ｓｎ  ＆＆  `Ｘ（Ｓｎ＋２）  ＆＆  Ｘ２（Ｓｎ＋１）  ＆＆
Ｘ３（Ｓｎ＋３）  ＆＆  Ｘ４（Ｓｎ＋８）
上記テストの意味は以下のようになる。
【００９８】
即ち、ある時刻Ｔ０において状態Ｓｎが成立し、時刻Ｔ１において状態Ｓｎ＋１が成立し、時刻Ｔ２において状態Ｓｎ＋２が成立し、  時刻Ｔ３において状態Ｓｎ＋３が成立し、時刻Ｔ４において状態Ｓｎ＋８が成立する。
【００９９】
本実施形態では、上述したように、テストを表現したが、論理シミュレーションを実施できるようなテストであれば、どのような形式でもかまわない。図１１に示す１１０１は、上記テストの通路を示す図である。
５．Ｑに属する節で、通過していない節が存在しないならば、上記４．で生成したテスト１１２を出力し、アサーション番号を更新し、上記１．からこの動作を繰り返す。また、Ｑ[０]の場合、属する節は全てテスト１１２により通過するため、テスト１１２をＱ[０]のテストとして出力し、Ｑ[１]のテストを生成するべく動作を繰り返す。
６．Ｑに属する節で、通過していない節が存在するならば、その中でＳｎから最も遠い節を求め、上記２．の動作から繰り返す。Ｑ[０]の場合は、通過していない節が存在しないため、この動作は必要ない。
【０１００】
上述したフローの中の上記１．で、Ｓｎから最も遠い節を求める理由は、分岐開始地点まで辿る遷移状態が多い方が、Ｑに属する節をより多く通る可能性があるためである。
【０１０１】
本実施形態では、説明を簡単にするため、ＤＵＴ１０２の有限状態機械１０４を図２に示すように小規模なものとしたが、実際のＤＵＴ１０２はより複雑で、大規模であることが想定される。そのため、未実施アサーションに対して全てのテストとなるが、実際はテストの数が膨大になる可能性もある。そのようなことを防ぐため、上述したフローを用いることによりテストの数をできるだけ少なくすることができる。
【０１０２】
このように生成したテスト１１２を用いて、論理シミュレーションを実施すれば検証未実施アサーション１０６は確実にテストを通過することになる。
【０１０３】
但し、生成したテスト１１２はＤＵＴ１０２に基づいて生成しているため、検証未実施アサーション１０６を発火させるに至るまでのシーケンスは必ずしも正しいとは言えない。生成したテスト１１２のシーケンスが仕様１０１に基づいたものになっているか否かは、仕様１０１と比較して確かめる必要がある。
【０１０４】
しかし、本実施形態ではアサーションは正しいものとしている。ＤＵＴを検証する方法としては、アサーションが発火しさえすれば良い。即ち、アサーションが発火するようなテストであれば、そのシーケンスは如何なるものでも構わない。
【０１０５】
従って、仮にテスト１１２のもつシーケンスがＤＵＴ１０２のバグを含むものであっても、アサーションが発火するならば、テスト１１２の不備が原因でＤＵＴのエラーを隠蔽してしまう恐れはない。
【０１０６】
以上説明した本実施形態によれば、従来いつ実施できるか分からなかったアサーションを確実に実施することが可能となる。これにより、検証効率の向上及び検証工数の削減が可能となる。
【０１０７】
従って、市場が欲するときに十分な精度で製品を投入することが可能となる。
【０１０８】
尚、本発明は複数の機器（例えば、ホストコンピュータ，インターフェース機器，リーダ，プリンタなど）から構成されるシステムに適用しても、１つの機器からなる装置（例えば、複写機，ファクシミリ装置など）に適用しても良い。
【０１０９】
また、前述した実施形態の機能を実現するソフトウェアのプログラムコードを記録した記録媒体を、システム或いは装置に供給し、そのシステム或いは装置のコンピュータ（ＣＰＵ若しくはＭＰＵ）が記録媒体に格納されたプログラムコードを読出し実行する。これによっても、本発明の目的が達成されることは言うまでもない。
【０１１０】
この場合、記録媒体から読出されたプログラムコード自体が前述した実施形態の機能を実現することになり、そのプログラムコードを記憶した記録媒体は本発明を構成することになる。
【０１１１】
このプログラムコードを供給するための記録媒体として、例えばフレキシブルディスク，ハードディスク，光ディスク，光磁気ディスク，ＣＤ−ＲＯＭ，ＣＤ−Ｒ，磁気テープ，不揮発性のメモリカード，ＲＯＭなどを用いることができる。
【０１１２】
また、コンピュータが読出したプログラムコードを実行することにより、前述した実施形態の機能が実現されるだけでなく、次の場合も含まれることは言うまでもない。即ち、プログラムコードの指示に基づき、コンピュータ上で稼働しているＯＳ（オペレーティングシステム）などが実際の処理の一部又は全部を行い、その処理により前述した実施形態の機能が実現される場合である。
【０１１３】
更に、記録媒体から読出されたプログラムコードがコンピュータに挿入された機能拡張ボードやコンピュータに接続された機能拡張ユニットに備わるメモリに書込む。その後、そのプログラムコードの指示に基づき、その機能拡張ボードや機能拡張ユニットに備わるＣＰＵなどが実際の処理の一部又は全部を行い、その処理により前述した実施形態の機能が実現される場合も含まれることは言うまでもない。
【図面の簡単な説明】
【０１１４】
【図１】本実施形態におけるテストを生成する方法を説明するための図である。
【図２】有限状態機械１０４の一例を状態遷移図として示す図である。
【図３】検証未実施アサーションに基づきテストを生成する処理を示すフローチャートである。
【図４】図１に示すテスト・レポート生成器１０５の構成の一例を示す図である。
【図５】Ｐｅｒｌによるアサーション抽出部の一例を示す図である。
【図６】あるアサーションについて全ての状態を巡った後の有限状態機械１０４の一例を示す図である。
【図７】あるテストを動的シミュレータで実行後の有限状態機械１０４の一例を示す図である。
【図８】アサーション・テスト解析器４０６の分類・解析処理を示すフローチャートである。
【図９】アサーション・テスト解析器４０６の分類・解析結果４０７の一例を示す図である。
【図１０】本実施形態におけるテスト１１２の生成方法を説明するための図である。
【図１１】本実施形態におけるテスト１１２の生成方法を説明するための図である。
【符号の説明】
【０１１５】
１０１  仕様
１０２  ＤＵＴ
１０３  有限状態機械変換器
１０４  有限状態機械
１０５  テスト・レポート生成器
１０６  検証未実施アサーション
１０７  内部表現変換器
１０８  内部表現
１０９  到達可能状態抽出器
１１０  到達可能状態
１１１  テスト生成器
１１２  テスト
４０１  アサーション
４０２  テスト
４０３  内部表現変換器
４０４  アサーション発火情報収集器
４０５  到達状態収集器
４０６  アサーション・テスト解析器
４０７  分類・解析結果
【図１】
2008033691.tif 000003
【図２】
2008033691.tif 000004
【図３】
2008033691.tif 000005
【図４】
2008033691.tif 000006
【図５】
2008033691.tif 000007
【図６】
2008033691.tif 000008
【図７】
2008033691.tif 000009
【図８】
2008033691.tif 000010
【図９】
2008033691.tif 000011
【図１０】
2008033691.tif 000012
【図１１】
2008033691.tif 000013