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