(57)【要約】【課題】ディジタル回路設計に用いられるハードウェア記述言語の多くは、ソフトウェアの記述言語と異なり、フリップフロップを中心として、回路の接続関係を記述する言語であるから、それによってプログラミングされるディジタル回路の検証においても、フリップフロップを中心としたカバレッジ基準、すなわち、フリップフロップの動作網羅率を測るカバレッジ基準が必要である。【解決手段】フリップフロップの動作として、状態を０に更新する動作と、状態を１に更新する動作と、現在の状態を保持する動作と、現在の状態を反転した値に更新する動作と、について各々の動作が起きるための条件を論理回路プログラムから抽出し、それらが論理シミュレーションによって活性化されたか否かを測定する検証支援装置によって達成できる。【選択図】図２
2014132403.tif 000002
【特許請求の範囲】
【請求項１】
論理回路中のフリップフロップの動作条件を算出するフリップフロップ動作条件算出部と、
フリップフロップの各動作条件を表示させるフリップフロップ動作仕様表示指示部と、
論理回路プログラムを論理シミュレーションし、フリップフロップの各動作条件の実行成否を監視するシミュレーション部と、
条件監視によって得られたモニタ情報により、各フリップフロップ動作が活性化されたか否かを集計するカバレッジ集計部と、
カバレッジ集計結果を表示させるカバレッジ表示指示部と、
前記フリップフロップ動作仕様表示部と前記カバレッジ表示指示部とからの指示により情報出力を行う表示部と、
を含むことを特徴とする検証支援装置。
【請求項２】
ハードウェア記述言語により記述された論理回路プログラムを受け付けるステップと、
前記論理回路プログラムから、フリップフロップを中心としたロジックコーンを表す論理式の算出を行うステップと、
前記論理式から前記フリップフロップの遷移表を作成するステップと、
前記遷移表に基づき、前記フリップフロップの動作の入力条件の算出を行うステップと、
を含む検証支援方法。
【請求項３】
請求項２に記載の検証支援方法であって、
前記動作は、状態を１に更新する動作、状態を０に更新する動作、現在の状態を保持する動作、現在の状態を反転した値に更新する動作、であること特徴とする検証支援方法。
【請求項４】
請求項２に記載の検証支援方法であって、
さらに、前記入力条件を、前記フリップフロップの動作仕様として表示するステップを、含む検証支援方法。
【請求項５】
請求項２に記載の検証支援方法であって、
さらに、前記入力条件に対し論理シミュレーションによって条件実行の成否を監視するステップと、
監視によって得られたモニタ情報を集計するステップと、
集計により得られたカバレッジ情報を表示するステップと、
を含む検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検証支援装置および検証支援方法に係り、特にディジタル回路設計における検証支援装置および検証支援方法に関する。
【背景技術】
【０００２】
ディジタル回路の検証において、実行すべきテストパターンを十分に実行したか否かを評価する指標として、カバレッジという考え方がある。カバレッジは、元来ソフトウェアプログラムを対象として考案された指標であるが、論理合成技術の実用化に伴って、ディジタル回路をハードウェア記述言語によるプログラミングでソフトウェアライクに設計するに至り、現在では、ディジタル回路設計における検証の分野においてもカバレッジが一般的となってきている。
【０００３】
ディジタル回路のプログラミングに用いられるハードウェア記述言語は、ソフトウェア設計に用いられる逐次実行型の記述言語とは大きく性格が異なる。ディジタル回路の記述には、一般的にＲＴＬ（Register Transfer Level）と呼ばれる記述言語が用いられる。ソフトウェアのプログラミング言語が逐次実行型の動作記述であるのに対し、ＲＴＬはフリップフロップ（以降、ＦＦと表記する）を中心として、回路の接続関係を表現したものであり、並列に動作する。したがって、これらの性格の相違故に、ディジタル回路の検証においては、ソフトウェアの検証では考慮する必要の無かった注意が必要である。
【０００４】
本技術分野の背景技術として、特許文献１がある。特許文献１は、前述したハードウェア・ソフトウェアの性格の相違に対して、ハードウェア特有の並列動作性に着目し、これによって発生し得る競合状態を想定した回路構成が論理シミュレーションによってどれだけ活性化されたかを、カバレッジとして測定する技術を開示する。
【０００５】
非特許文献１にはカバレッジの簡単な解説が記載されている。また、非特許文献２は、良く知られるカバレッジ基準である、ステートメント・カバレッジ、ブランチ・カバレッジ等の他、様々な既存のカバレッジ基準を紹介している。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１１−１３８４２８号公報
【非特許文献】
【０００７】
【非特許文献１】Lee Copeland、「はじめて学ぶソフトウェアのテスト技法」、日経ＢＰ社、２０１１年
【非特許文献２】Steve Cornett、”Code Coverage Analysis”、［ｏｎｌｉｎｅ］、Bullseye Testing Technology、［平成２４年１２月５日検索］、インターネット＜http://www.bullseye.com/coverage.html＞
【発明の概要】
【発明が解決しようとする課題】
【０００８】
本発明は、上述した記述言語の性格の相違に対して、特許文献１とは異なった観点で、カバレッジを測定する。ハードウェア記述言語は、ＦＦを中心として記述するものである。それゆえ、ハードウェア記述言語によってプログラミングされるディジタル回路の検証においても、本来は、ＦＦを中心としたカバレッジ基準、すなわち、ＦＦの動作の網羅率を測るカバレッジ基準が必要である。ところが、従来のディジタル回路検証には、そのようなカバレッジ基準が存在しなかった。このため、ＦＦの動作に対する網羅的な検証を行うことは難しく、この点において、ＦＦを中心とした配線記述のプログラムを対象とする観点を持たないソフトウェアのカバレッジ基準のみでは、たとえ１００％のカバレッジを達成したとしても、依然として検証漏れを発生させる危険があった。
【０００９】
上述した検証漏れを発生させないためには、システムを構成する大規模・複雑な論理において、回路中に多用されるＦＦ一つ一つにつき、各々を中心とした全ての動作条件を漏れなく把握する必要がある。しかし、その数の多さと条件の複雑さから、人間がこれを把握することは、現実的に不可能である。また、これらの条件を人手で抽出することは、極めて困難な状況にある。
【００１０】
本発明は、上述した状況を鑑みて、為されたものである。すなわち、本発明の目的は、ＦＦの動作に注目した網羅的検証を行うための検証支援装置および検証支援方法の提供である。
【課題を解決するための手段】
【００１１】
上述した課題は、  論理回路中のフリップフロップの動作条件を算出するフリップフロップ動作条件算出部と、フリップフロップの各動作条件を表示させるフリップフロップ動作仕様表示指示部と、論理回路プログラムを論理シミュレーションし、フリップフロップの各動作条件の実行成否を監視するシミュレーション部と、条件監視によって得られたモニタ情報により、各フリップフロップ動作が活性化されたか否かを集計するカバレッジ集計部と、カバレッジ集計結果を表示させるカバレッジ表示指示部と、フリップフロップ動作仕様表示部とカバレッジ表示指示部とからの指示により情報出力を行う表示部と、を含む検証支援装置により、達成できる。
【００１２】
また、ハードウェア記述言語により記述された論理回路プログラムを受け付けるステップと、論理回路プログラムから、フリップフロップを中心としたロジックコーンを表す論理式の算出を行うステップと、論理式からフリップフロップの遷移表を作成するステップと、遷移表に基づき、フリップフロップの動作の入力条件の算出を行うステップと、を含む検証支援方法により、達成できる。
【発明の効果】
【００１３】
本発明に依れば、ハードウェア記述言語によって記述されるディジタル回路において、本来留意すべき、ＦＦの動作に注目した客観的な検証品質指標を得ることができる。
【図面の簡単な説明】
【００１４】
【図１】検証支援装置のハードウェアブロック図である。
【図２】検証支援装置の機能ブロック図である。
【図３】ＦＦ動作条件算出の処理を説明するフローチャートである。
【図４】ロジックコーンの概念を説明する図である。
【図５】単一のロジックコーンを説明する図である。
【図６】単一のロジックコーンの回路図である。
【図７】ＦＦからの自己回帰を持つロジックコーンを説明する図である。
【図８】論理式化した回路記述から各ＦＦ動作に対する入力条件が算出できる理由を説明する図である。
【図９】ハードウェア記述言語で記述した論理回路プログラムである。
【図１０】ＦＦ遷移表への変換結果を示す図である。
【図１１】ＦＦ遷移表への変換方法を説明するフローチャートである。
【図１２】ＦＦの各動作に対する入力条件式の算出結果を示す図である。
【図１３】多数の入力信号が有る場合の、ＦＦ遷移表への変換結果を示す図である。
【図１４】多数の入力信号が有る場合の、ＦＦの各動作に対する入力条件式の算出結果を示す図である。
【図１５】検証支援装置が出力する第１の表示を説明する図である。
【図１６】検証支援装置が出力する第２の表示を説明する図である。
【図１７】検証支援装置が出力する第３の表示を説明する図である。
【図１８】検証支援装置が出力する第４の表示を説明する図である。
【図１９】検証支援装置が出力する第５の表示を説明する図である。
【図２０】検証支援装置が出力する第６の表示を説明する図である。
【発明を実施するための形態】
【００１５】
以下、本発明の実施の形態について、実施例を用い図面を参照しながら詳細に説明する。なお、実質同一部位には同じ参照番号を振り、説明は繰り返さない。
【００１６】
図１を参照して、検証支援装置のハードウェア構成を説明する。図１において、検証支援装置１００は、メモリ１１０と、ＣＰＵ１２０と、記憶装置１３０と、入力装置１４０と、出力装置１５０と、バス１６０とから構成される。
【００１７】
メモリ１１０は、ＣＰＵ１２０が実行するプログラムを記憶する。ＣＰＵ１２０は、メモリ１１０が記憶するプログラムを実行することにより、論理シミュレーションと、ＦＦ動作仕様算出およびカバレッジ情報算出を行う。記憶装置１３０は、ＨＤ（ハードディスク）等の補助記憶装置であり、論理回路プログラム、テストパターン、ＦＦ動作仕様算出結果、カバレッジ情報算出結果等を記憶する。入力装置１４０は、論理回路プログラムおよびテストパターンを読み込む。出力装置１５０は、カバレッジの出力結果を表示する。バス１６０はメモリ１１０と、ＣＰＵ１２０と、記憶装置１３０と、入力装置１４０と、出力装置１５０とを相互接続する。
【００１８】
図２を参照して、検証支援装置の機能的構成を説明する。図２において、検証支援装置１００は、ＦＦ動作条件算出部２０１と、ＦＦ動作仕様表示指示部２０２と、シミュレーション部２０３と、カバレッジ集計部２０４と、カバレッジ表示指示部２０５と、表示部２０６とから構成される。
【００１９】
ＦＦ動作条件算出部２０１は、論理回路プログラム２０７を取得し、論理回路中の全ＦＦに対し、各ＦＦ動作の入力条件情報２０９の算出を行う。ここで、論理回路プログラム２０７とは、検証対象となる論理回路をハードウェア記述言語で記述したプログラムである。ＦＦ動作仕様表示指示部２０２は、ＦＦ動作条件算出部２０１が算出した、各ＦＦ動作の入力条件情報２０９を表示部２０６に出力させる処理を行う。
【００２０】
シミュレーション部２０３は、ＦＦ動作条件算出部２０１が算出した、各ＦＦ動作の入力条件情報２０９を取得し、論理シミュレーションによって、各々の条件が実行されたか否かの監視を行う。カバレッジ集計部２０４は、シミュレーション部２０３の条件監視によって得られるモニタ情報を取得し、各条件が実行されたか否か、すなわち、各ＦＦ動作が活性化されたか否かを、カバレッジ集計結果２１０として集計する。カバレッジ表示指示部２０５は、カバレッジ集計部２０４が集計した、カバレッジ集計結果２１０を表示部２０６に出力させる処理を行う。表示部２０６は、各ＦＦ動作の入力条件情報２０９およびカバレッジ集計結果２１０を表示する。
【００２１】
図３を参照して、ＦＦ動作条件算出部の処理を説明する。図３において、ＦＦ動作条件算出部２０１は、論理回路プログラムを読込む（Ｓ３１）。ＦＦ動作条件算出部２０１は、全てのＦＦの動作条件の算出が完了したか否かを判定する（Ｓ３２）。検証対象の論理回路にＦＦが含まれなかった場合（ＹＥＳ）、ＦＦ動作条件算出部２０１は、処理は終了とする。
【００２２】
ステップ３２において、全てのＦＦの動作条件の算出が完了していなければ（ＮＯ）、ＦＦ動作条件算出部２０１は、未処理のＦＦの中から、今回、対象とするＦＦを１つ決定する（Ｓ３３）。ＦＦ動作条件算出部２０１は、入力された論理回路プログラム２０７から、対象のＦＦのＦＦ論理式を算出する（Ｓ３４）。ＦＦ動作条件算出部２０１は、算出したＦＦ論理式を、ＦＦ遷移表に変換する（Ｓ３５）。ＦＦ動作条件算出部２０１は、得られたＦＦ遷移表に基づき、各ＦＦ動作の入力条件の算出を行う（Ｓ３６）。ＦＦ動作条件算出部２０１は、得られた各ＦＦ動作の入力条件情報を、記憶装置１３０に記憶し（Ｓ３７）、ステップ３２に戻る。
【００２３】
ステップ３４のＦＦ論理式算出について、以下、さらに詳細に説明する。論理回路は、ＦＦ一つ一つを中心としたロジックコーンと呼ばれる論理構造グループに分割して考えることができる。ロジックコーンは、ＦＦ論理式生成に用いるものであり、この抽出方法について説明する。
【００２４】
図４を参照して、ロジックコーンの概念を説明する。図４において、ロジックコーン４５０は、ＦＦ４４０の出力を頂点とし、入力ポート４１０またはＦＦ４４０の出力の組を底面とした円錐型の論理構造グループである。ロジックコーン４５０は、ＦＦ４４０の入力側に存在する組合せ論理回路４３０の接続関係を、他のＦＦの出力、または自分自身のＦＦの出力からの回帰、または入力ポートに辿り着くまで遡ることで抽出できる。論理回路は、各ロジックコーン４５０とその接続を指定することにより、一意に表すことが可能である。
【００２５】
図５を参照して、単一のロジックコーンの簡単な抽象図を説明する。図５において、ロジックコーン４５０は、ＦＦ４４０を頂点とする組合せ論理回路４３０から構成される。組合せ論理回路４３０は、単純に入力ａ、ｂ、ｃのみによって出力Ｑｎが決定されるので、これを論理関数ｆで（式１）のように表現することができる。
Ｑｎ＝ｆ(ａ,ｂ,ｃ)  …（式１）
図６を参照して、図５のロジックコーンの具体的な回路を説明する。図６において、ロジックコーン４５０は、ＮＯＴゲート６１０と、ＡＮＤゲート６２０と、ＯＲゲート６３０と、ＦＦ６４０とで構成されている。この回路おいて、（式１）の論理関数ｆは、（式２）で表される。
Ｑｎ＝！ａ＆(ｂ｜ｃ)  …（式２）
ここで、「！」は、論理否定を表す論理記号でありＮＯＴゲート６１０を指す。「＆」は、論理積を表す論理記号であり、ＡＮＤゲート６２０を指す。「｜」は、論理和を表す論理記号でありＯＲゲート６３０を指す。また、「ｂ」、「！ａ」の変数と変数の否定のことをリテラルと呼ぶ。
【００２６】
図７を参照して、現在の状態を保持する動作または現在の状態を反転した値に更新する動作を持つロジックコーンを説明する。図７において、ロジックコーン４５０Ａは、ＦＦ４４０からの自己回帰を持つ。ＦＦ４４０が現在の状態を保持する動作または現在の状態を反転した値に更新する動作を持つ場合、必ずＦＦ４４０の出力Ｑｎ−１が入力側の組合せ論理回路４３０の入力に回帰する論理構成となる。ここで、組合せ論理回路４３０の出力Ｑｎを論理関数ｆで表現すると、（式３）となる。
Ｑｎ＝ｆ(ａ,ｂ,ｃ,Ｑｎ−１)  …（式３）
図８と（式４）を参照して、論理式化した回路記述から、各ＦＦ動作とそれぞれの動作が成立するための条件式を算出できる理由を説明する。
Ｑｎ
＝ｆ１(ａ,ｂ,ｃ)｜ｆ２(ａ,ｂ,ｃ)＆Ｑｎ-１｜ｆ３(ａ,ｂ,ｃ)＆(！Ｑｎ-１)…(式４)
（式４）は、（式３）からＱｎ−１および！Ｑｎ−１のリテラルを括り出した論理式である。ｆ２は、Ｑｎ−１に対する係数となる論理式である。ｆ３は、！Ｑｎ−１に対する係数となる論理式である。ｆ１は、Ｑｎ−１および！Ｑｎ−１のリテラルを括り出した結果、余りとなる論理式である。ｆ１、ｆ２、ｆ３は、いずれも、現在の入力信号ａ、ｂ、ｃのみによって０か１かの論理値が一意に決定される論理式である。また、図５で表されるような、ＦＦの自己回帰を持たないロジックコーンも、（式４）において、ｆ２およびｆ３の論理値が常に０である論理であるとすることにより、表現できる。すなわち、（式４）は、どのようなロジックコーンであっても、必ず表現することが可能である。したがって、（式４）によれば、どのようなロジックコーンであっても、各ＦＦの動作は、現在の入力条件のみから、計算によって求めることができる。
【００２７】
図８を参照して、その理由を具体的に説明する。図８において、条件と結果のテーブル８２０は、条件８２１と、Ｑｎ計算結果８２２と、意味８２３とで構成されている。図８において、ｆ１の論理値が１である場合、または、ｆ１の論理値が０であり、かつｆ２およびｆ３の論理値が共に１である場合、Ｑｎの論理値は常に１となる。これは、ＦＦの現在の状態に関わらず、次の状態は必ず１に更新されることを表す。
【００２８】
ｆ１およびｆ３の論理値が０であり、かつｆ２の論理値が１である場合、Ｑｎの論理値は、常にＱｎ−１と等しくなる。これは、ＦＦの現在の状態を保持することを表す。
ｆ１およびｆ２の論理値が０であり、かつｆ３の論理値が１である場合、Ｑｎの値は、常に！Ｑｎ−１と等しくなる。これは、ＦＦの次の状態が、現在の状態を反転した値に更新されることを表す。
それ以外の場合、Ｑｎの論理値は、常に０となる。これは、ＦＦの現在の状態に関わらず、次の状態は必ず０に更新されることを表す。
【００２９】
図９を参照して、論理回路プログラムからのＦＦ論理式算出について説明する。図９は、検証対象となる論理回路をハードウェア記述言語で記述した論理回路プログラムである。図９において、論理回路プログラムは、００１：〜００８：の行番号と制御文および命令文から構成される。ここで、”ａ”、”ｂ”、”ｃ”は、入力信号の信号名を表す。”ｆｆ１”は、ＦＦの識別名称を表す。”１’ｂ０”および”１’ｂ１”は、それぞれ、１ビットの論理値の０と１を表す。”＜＝”の記号は、左辺の示すＦＦの状態を、右辺の示す値に更新する命令を表している。
【００３０】
図９の論理回路プログラムにおける、”ｆｆ１”に対し、ＦＦ論理式化した回路記述が、（式５）である。図９の論理回路プログラムと（式５）の論理式は表現方法の違いこそあれ、全く同じ回路構造を表すものである。論理回路プログラムから論理式を抽出することは、市販の論理設計支援ツールなどを用いて容易に実現することができる。
ｆｆ１＝(ｆｆ１｜(ｂ｜ｃ))＆(！ａ)  …（式５）
ここで、（式５）の右辺の”ｆｆ１”は、”ｆｆ１”の現在の状態、すなわち、（式３）の右辺のＱｎ−１を表す。一方、左辺の”ｆｆ１”は、”ｆｆ１”の次の状態、すなわち、（式３）の左辺のＱｎを表す。
【００３１】
図１０および図１１を参照して、図３のステップ３５のＦＦ遷移表変換を説明する。図１０は、（式５）のＦＦ論理式における、”ｆｆ１”に対し、ＦＦ遷移表への変換を行った表である。ＦＦ遷移表１０００において、ａ列１０１０、ｂ列１０２０、ｃ列１０３０は、それぞれ入力信号ａ、ｂ、ｃの論理値を表している。Ｑｎ列１０４０は、ＦＦの次の状態を表す。
【００３２】
具体的には、行１０５０において、入力信号ａ、ｂ、ｃの組合せが、（式６）のときに、ＦＦの次の状態ＱｎがＦＦの現在の状態Ｑｎ−１となること、すなわち、現在の状態を保持することを意味する。
(ａ,ｂ,ｃ)＝(０,０,０)  …（式６）
同様に、行１０６０は、入力信号ａ,ｂ,ｃの組合せが、（式７）のときに、ＦＦの現在の状態に関わらず、次の状態を１に更新する。
(ａ,ｂ,ｃ)＝(０,０,１),(０,１,０),(０,１,１)  …（式７）
また、行１０７０は、入力信号ａ,ｂ,ｃの組合せが、（式８）のときに、ＦＦの現在の状態に関わらず、次の状態を０に更新する。
(ａ,ｂ,ｃ)
＝(１,０,０),(１,０,１),(１,１,０),(１,１,１)  …（式８）
なお、（式５）のＦＦ論理式においては、現在の状態を反転する計算結果は、得られていない。
【００３３】
図１１を参照して、図１０に示すＦＦ遷移表を作成するための手順を説明する。図１１において、ＦＦ動作条件算出部２０１は、全ての入力信号の組合せについてＱｎを算出したか否かを判定する（Ｓ１１１）。全ての入力信号についてＱｎの算出が完了していた場合、ＦＦ動作条件算出部２０１は、処理を終了する。
【００３４】
全ての入力信号の組合せについてＱｎの算出を完了していなかった場合、ＦＦ動作条件算出部２０１は、未算出の入力信号の組合せの中から今回算出対象とする入力信号の組合せを決定する（Ｓ１１２）。入力信号の組合せを、ＦＦ動作条件算出部２０１は、ＦＦ論理式に代入し、Ｑｎの論理値を算出する（Ｓ１１３）。ＦＦ動作条件算出部２０１は、Ｑｎの算出結果がいずれの値になったかを判定する（Ｓ１１４）。
【００３５】
Ｑｎの算出結果には、Ｑｎ＝Ｑｎ−１、Ｑｎ＝！Ｑｎ−１、Ｑｎ＝１、Ｑｎ＝０の４通りがある。Ｑｎ＝Ｑｎ−１であった場合、ＦＦ動作条件算出部２０１は、ＦＦ遷移表のＱｎ列１０４０の内、今回算出に用いた入力信号の組合せに該当する欄に「Ｑｎ−１」と入力する（Ｓ１１５）。Ｑｎ＝！Ｑｎ−１であった場合、ＦＦ動作条件算出部２０１は、該当する欄に「！Ｑｎ−１」と入力する（Ｓ１１６）。Ｑｎ＝１であった場合、ＦＦ動作条件算出部２０１は、該当する欄に「１」と入力する（Ｓ１１７）。Ｑｎ＝０であった場合、ＦＦ動作条件算出部２０１は、該当する欄に「０」と入力する（Ｓ１１８）。入力の後、ＦＦ動作条件算出部２０１は、ステップ１１１に戻る。
【００３６】
図１２を参照して、図３のステップ３６のＦＦ動作条件算出について説明する。ステップ３６では、ステップ３５で作成したＦＦ遷移表に基づき、各ＦＦ動作に対する入力条件を算出する。図１２は、図１０のＦＦ遷移表１０００に基づいて、各ＦＦ動作に対する入力条件を算出した表である。ここで、図１２において、ＦＦ動作１２１０の「セット」は、ＦＦの状態を１に更新する動作を定義する。「リセット」は、ＦＦの状態を０に更新する動作を定義する。「保持」は、ＦＦの現在の状態を保持する動作を定義する。「反転」は、ＦＦの状態を現在の状態を反転した値に更新する動作を定義する。
【００３７】
入力条件１２２０を、セット動作の入力条件について、説明する。ＦＦがセット動作を行うための入力パターンは、図１０の行１０６０で表される３パターンであるから、これらを論理式に変換する。入力ａが０であり、かつ入力ｂまたは入力ｃが１であるときに、ＦＦがセット動作を行うことから、この入力条件を論理式で表現すると、（式９）で表すことができる。
ｆ(ａ,ｂ,ｃ)＝！ａ＆(ｂ｜ｃ)  …（式９）
リセット、保持の論理式については、図１２に示す通りである。また、入力条件１２２０の内、反転動作に対する「−」は、条件が存在しないことを表し、”ｆｆ１”において、反転動作が起こり得ないことを意味する。
【００３８】
なお、ここでは３入力のロジックコーンについて説明を行ったが、実際には図１３に示すように、入力信号が多くなるほど遷移表１０００Ａは、拡大していく。遷移表１０００Ａを基に算出を行うと、図１４に示すように、条件式が冗長になる。したがって、カルノー図法、クワイン・マクラスキー法などの簡単化手法を用いて、条件式を整理する。これにより、条件式の冗長化を抑止すると共に、以降の処理を効率的に行う。
【００３９】
図１５および図１６を参照して、ＦＦ動作仕様表示指示部２０２が、表示部２０６に出力させる表示について、詳細に説明する。
【００４０】
図１５を参照して、ＦＦ動作仕様表示指示部２０２が、まず始めに出力を指示する表示画面を説明する。図１５において、出力結果１５００は、ｂｌｏｃｋ１〜ｂｌｏｃｋＮのブロック別ＦＦ数１５１０と、合計のＦＦ数１５２０を表示する。
【００４１】
図１６は、出力結果１５００のｂｌｏｃｋ１〜ｂｌｏｃｋＮの中から、ユーザが情報を希望するブロックを選択することにより出力する表示である。図１６において、出力結果１６００は、ユーザが選択したブロックに含まれる全てのＦＦ１６１０に対して、各々の、セット、リセット、保持、反転の各動作の入力条件１６２０を表示する。また、該当の入力条件が存在しない場合は、「−」を表示する。（条件１．１）〜（条件Ｎ．４）の記載は、実際には論理式であり、”ｆｆ１”を図１２に当てはめるならば、（条件１．１）は、条件１２２１より”！ａ＆（ｂ｜ｃ）”、（条件１．２）は、条件１２２２より”ａ”、（条件１．３）は、条件１２２３より”！ａ＆！ｂ＆！ｃ”、（条件１．４）は、条件１２２４より”−”となる。
【００４２】
出力結果１６００により、各ＦＦの動作が、設計者の考える仕様と一致しているか否かを確認することができる。これにより、記述誤り等の不注意、考慮漏れといった原因から発生するバグを抑止することができる。
【００４３】
図１７ないし図２０を参照して、カバレッジ表示指示部２０５が、表示部２０６に出力させる表示について、詳細に説明する。
図１７を参照して、カバレッジ表示指示部２０５がまず始めに出力を指示する表示画面を説明する。図１７において、出力結果１７００は、ｂｌｏｃｋ１〜ｂｌｏｃｋＮのブロック別のＦＦ数１７１０と、合計のＦＦ数１７２０と、各々のブロックにおいて、監視対象となる全ての条件の数１７３０と、その内、論理シミュレーションによって実行された条件の数１７４０と、カバレッジ率１７５０を表示する。カバレッジ率１７５０は、監視対象となる全ての条件の数１７３０に対し、論理シミュレーションによって実行された条件の数１７４０の比率として算出され、百分率で表示する。
【００４４】
出力結果１７００によれば、設計回路中のＦＦに発生し得る全ての動作が、論理シミュレーションによってどれだけ活性化されたかを評価尺度として、検証の十分性を的確かつ定量的に評価することができる。
【００４５】
図１８を参照して、出力結果１７００のｂｌｏｃｋ１〜ｂｌｏｃｋＮの中から、ユーザが情報を希望するブロックを選択することにより出力する表示を説明する。図１８において、出力結果１８００は、ＦＦ１８１０と、入力条件監視結果１８２０と、ＦＦ動作網羅率１８３０とから構成される。
【００４６】
ＦＦ１８１０は、ユーザの選択したブロックに含まれる全ＦＦを表示する。入力条件監視結果１８２０は、ＦＦ１８１０に対して、各々の、セット、リセット、保持、反転の各ＦＦ動作の入力条件を表示し、また、それらの条件が、論理シミュレーションによって実行されたか否かの監視結果を、「○」と「×」で表示する。論理シミュレーション中に１回でも条件に合致するパターンがあった場合は「○」となり、全く合致するパターンが無かった場合は「×」となる。また、該当の入力条件が存在しない場合は、「−」を表示する。
【００４７】
（条件１．１）〜（条件Ｎ．４）の記載は、実際には論理式である。”ｆｆ１”を図１２に当てはめるならば、（条件１．１）は、条件１２２１より”！ａ＆（ｂ｜ｃ）”、（条件１．２）は、条件１２２２より”ａ”、（条件１．３）は、条件１２２３”！ａ＆！ｂ＆！ｃ”となる。
【００４８】
ＦＦ動作網羅率１８３０は、各ＦＦについて、起こり得る全てのＦＦ動作の数１８３１と、その内、論理シミュレーションによって活性化されたＦＦ動作の数１８３２をそれぞれ表示する。
【００４９】
出力結果１８００によれば、カバレッジ測定の結果、検証が不足していると判断される論理回路に対し、具体的に、どのＦＦの、どの動作が活性化されていないのか、また、その動作を活性化させるためには、どのような条件が必要なのかを確認することができ、検証設計にフィードバックするための詳細な情報を得ることができる。
【００５０】
図１９を参照して、出力結果１８００に対し、ユーザが更に詳細な情報を要求した場合に出力する表示を説明する。図１９において、出力結果１９００は、ＦＦ１９１０と、入力条件実行網羅率１９２０とから構成される。入力条件実行網羅率１９２０は、各ＦＦ動作の入力条件に対して、それらの条件を構成する全ての入力信号の組合せの数１９２１と、その内、論理シミュレーションによって実行された入力信号の組合せの数１９２２と、それらの比を百分率で算出した結果１９２３を表示する。該当の入力条件が存在しない場合、入力条件実行網羅率１９２０は、「−」を表示する。
【００５１】
出力結果１９００によれば、各ＦＦ動作について、その動作を発生させる全ての入力ケースの内、論理シミュレーションでどれだけ実行されたかを確認することができる。これにより、検証内容の偏りを定量的に判断することができ、効率的な検証設計が可能となる。
【００５２】
図２０を参照して、出力結果１９００のｆｆ１〜ｆｆＮの中から、ユーザが特定のＦＦに対する詳細な情報を希望したときに出力する表示を説明する。図２０において、出力結果２０００は、ＦＦ動作２０１０と、入力信号２０２０と、監視結果２０３０とから構成される。ＦＦ動作２０１０は、ユーザの選択したＦＦにおいて、起こり得る全てのＦＦ動作を表示する。入力信号２０２０は、ＦＦ動作２０１０に対する入力条件を満たす、全ての入力信号の組合せを表示する。監視結果２０３０は、入力信号２０２０に示す入力信号の組合せが、論理シミュレーションによって実行されたか否かを、「○」と「×」で表示する。論理シミュレーション中に１回でも条件に合致するパターンがあった場合は「○」となり、全く合致するパターンが無かった場合は「×」となる。なお、ここでは、反転の無い論理式について、示している。
【００５３】
出力結果２０００によれば、複合的な入力条件に対し、具体的にどのような入力パターンがテストされていないのかを個別に知ることができ、テストパターン検討のための、より直接的な手掛りとなる情報を得ることができる。
【００５４】
上述した実施例に依れば、ハードウェア記述言語によって記述されるディジタル回路において、本来留意すべき、ＦＦの動作に注目した客観的な検証品質指標を得ることができる。これにより、従来、人間の主観のみでは見逃しがちだった、検証の漏れを抑止すると共に、無駄の無い、高効率な検証を行うことを可能とする。
【符号の説明】
【００５５】
１００…検証支援装置、１１０…メモリ、１２０…ＣＰＵ、１３０…記憶装置、１４０…入力装置、１５０…出力装置、１６０…バス、２００…検証支援装置、２０１…ＦＦ動作条件算出部、２０２…ＦＦ動作仕様表示指示部、２０３…シミュレーション部、２０４…カバレッジ集計部、２０５…カバレッジ表示指示部、２０６…表示部、２０７…論理回路プログラム、２０８…テストパターン、２０９…各ＦＦ動作の入力条件情報、２１０…カバレッジ集計結果。
【図１】
2014132403.tif 000003
【図２】
2014132403.tif 000004
【図３】
2014132403.tif 000005
【図４】
2014132403.tif 000006
【図５】
2014132403.tif 000007
【図６】
2014132403.tif 000008
【図７】
2014132403.tif 000009
【図８】
2014132403.tif 000010
【図９】
2014132403.tif 000011
【図１０】
2014132403.tif 000012
【図１１】
2014132403.tif 000013
【図１２】
2014132403.tif 000014
【図１３】
2014132403.tif 000015
【図１４】
2014132403.tif 000016
【図１５】
2014132403.tif 000017
【図１６】
2014132403.tif 000018
【図１７】
2014132403.tif 000019
【図１８】
2014132403.tif 000020
【図１９】
2014132403.tif 000021
【図２０】
2014132403.tif 000022