(57)【要約】【課題】  論理変更により影響を受ける出力端子と影響を受けない出力端子および順序回路の出力信号を判別することで、論理変更により検証すべき信号を明確することで検証効率を向上させることを目的とする。【解決手段】  変更前後の論理回路に共通に存在する出力端子と順序回路の出力信号をすべての事象毎に比較する。【選択図】  図１
2007004560.tif 000002
【特許請求の範囲】
【請求項１】
ハードウェア記述言語により記述された論理回路の変更前後の動作が一致するかどうかを判定する論理検証装置において、
変更前後の論理回路の記述を読み込む論理記述読込手段と、
前記変更前後の論理記述について出力端子と順序回路の出力信号を抽出する信号抽出手段と、
前記抽出した出力端子および順序回路の出力信号において前記変更前後の論理記述内に共通に存在する出力端子および順序回路の出力信号とどちらか一方のみにしか存在しない出力端子および順序回路の出力信号を選別する選別手段と、
前記変更前の論理回路と前記変更後の論理回路とで前記共通に存在する出力端子および順序回路の出力信号の値を比較するためのモニタを生成するモニタ生成手段と、
前記変更前後の論理回路の入力信号にすべての組み合わせを入力し、かつ前記論理回路に存在する順序回路毎に発生しうるすべての事象を発生させる事象発生手段と、
前記変更前後の論理回路に共通に存在する入力信号に同じ値を入力するように前記事象発生手段を制御する同一信号入力制御手段と、
前記事象発生手段にて発生させた事象毎に前記モニタ生成手段にて生成したモニタを用い前記共通に存在する出力端子および順序回路の出力信号の値を比較する比較手段と、
前記選別手段によりどちらか一方のみにしか存在しない出力端子および順序回路の出力信号および前記比較結果から不一致した出力端子および順序回路の出力信号を出力する不一致信号出力手段と、
前記比較結果から一致した出力端子の端子名を出力する一致出力端子出力手段を有することを特徴とした論理検証装置。
【請求項２】
前記モニタ生成手段において、前記論理回路の初期化条件を読み込むことでプロパティを生成する機能を有し、かつ前記事象発生手段および前記比較手段はプロパティ検証により実現することを特徴とした請求項１記載の論理検証装置。
【請求項３】
ハードウェア記述言語により記述された論理回路の変更前後の動作が一致するかどうかを判定する論理検証手法において、
変更前後の論理回路の記述を読み込む論理記述読込工程と、
前記変更前後の論理記述について出力端子と順序回路の出力信号を抽出する信号抽出工程と、
前記抽出した出力端子および順序回路の出力信号において前記変更前後の論理記述内に共通に存在する出力端子および順序回路の出力信号とどちらか一方のみにしか存在しない出力端子および順序回路の出力信号を選別する選別工程と、
前記変更前の論理回路と前記変更後の論理回路とで前記共通に存在する出力端子および順序回路の出力信号の値を比較するためのモニタを生成するモニタ生成工程と、
前記変更前後の論理回路の入力信号にすべての組み合わせを入力し、かつ前記論理回路に存在する順序回路毎に発生しうるすべての事象を発生させる事象発生工程と、
前記変更前後の論理回路に共通に存在する入力信号に同じ値を入力するように前記事象発生工程を制御する同一信号入力制御工程と、
前記事象発生工程にて発生させた事象毎に前記モニタ生成工程にて生成したモニタを用い前記共通に存在する出力端子および順序回路の出力信号の値を比較する比較工程と、
前記選別工程によりどちらか一方のみにしか存在しない出力端子および順序回路の出力信号および前記比較結果から不一致した出力端子および順序回路の出力信号を出力する不一致信号出力工程と、
前記比較結果から一致した出力端子の端子名を出力する一致出力端子出力工程を有することを特徴とした論理検証方法。
【請求項４】
前記モニタ生成工程は前記論理回路の初期化条件を読み込むことで動作仕様記述を生成する機能を有し、かつ前記事象発生工程および前記比較工程はプロパティ検証を用いることを特徴とした請求項３記載の論理検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はハードウェア記述言語で記述した論理回路の検証に関するものである。
【背景技術】
【０００２】
ＬＳＩを含む論理回路の規模は、年毎に増加し機能は複雑化している。それに伴い、論理回路の検証にかかる工数も増加している。一方、市場には消費者が欲するときに製品を投入しなければならず、ＬＳＩを始めとした論理回路の開発期間は短くなっている。そのため、論理回路検証の効率向上を図る必要が生じている。当然ながら、論理回路の開発中は論理検証において検出した不具合を修正するための論理変更や仕様の追加あるいは変更によって論理回路構成は日々変わっていく。そのため論理変更によって新たな不具合が混入されることがあり、このような不具合を早期に発見することも開発期間短縮に向けた重要な要素である。
【０００３】
論理変更により新たな不具合が混入されていないことを確認するためには、通常の検証と同様に既存の検証パターンを実行して検証を行う。また、補完的に、形式的論理検証手法の一つである論理等価検証を変更前後の論理回路に対して実行し、変更個所を特定して確認する方法がとられている。
【０００４】
又、従来例としては、例えば特許文献１をあげることが出来る。
【特許文献１】特開２０００−２０７４４０号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
しかしながら、既存の検証パターンを実行し直す場合は、検証パターンによっては検証を開始してから終了するまで数週間かかるものもあるため、非常に時間がかかってしまう場合がある。特に開発完了が迫った時期に論理変更があった場合、期間内に検証を完了することができず開発スケジュールに支障をきたす可能性がある。
【０００６】
また、他の方法の論理等価検証は、等価でない個所がその後段に続く内部信号や最終的に出力されるどの出力端子に影響を及ぼしているかどうかまではわからない。
【０００７】
以上のような場合において、仮に仕様変更や不具合改訂などにより論理変更された個所が論理回路のどの出力端子や内部信号に影響を及ぼしているかが判別できれば、動作が変わらない信号と変わる信号を把握することができるため、動作が変わる信号にのみ着目して検証を行うだけで、論理変更により新規の不具合が混入されていないかどうかの検証が可能となる。
【０００８】
本発明は、上述した問題に鑑みてなされたものであり、論理変更により影響を受ける出力端子と影響を受けない出力端子および順序回路の出力信号を判別することで、論理変更により検証すべき信号を明確することで検証効率を向上させる論理検証方法を提供するものである。
【課題を解決するための手段】
【０００９】
上記目的を達成するための本発明の第一の特徴は、ハードウェア記述言語により記述された論理回路の変更前後の動作が一致するかどうかを判定する論理検証装置において、変更前後の論理回路の記述を読み込む論理記述読込手段と、前記変更前後の論理記述について出力端子と順序回路の出力信号を抽出する信号抽出手段と、前記抽出した出力端子および順序回路の出力信号において前記変更前後の論理記述内に共通に存在する出力端子および順序回路の出力信号とどちらか一方のみにしか存在しない出力端子および順序回路の出力信号とを選別する選別手段と、前記変更前の論理回路と前記変更後の論理回路とで前記共通に存在する出力端子および順序回路の出力信号の値を比較するためのモニタを生成するモニタ生成手段と、前記変更前後の論理回路の入力信号にすべての組み合わせを入力し、かつ前記論理回路に存在する順序回路毎に発生しうるすべての事象を発生させる事象発生手段と、前記変更前後の論理回路に共通に存在する入力信号に同じ値を入力するように前記事象発生手段を制御する同一信号入力制御手段と、前記事象発生手段にて発生させた事象毎に前記モニタ生成手段にて生成したモニタを用い前記共通に存在する出力端子および順序回路の出力信号の値を比較する比較手段と、前記選別手段によりどちらか一方のみにしか存在しない出力端子および順序回路の出力信号および前記比較結果から不一致した出力端子および順序回路の出力信号を出力する不一致信号出力手段と、前記比較結果から一致した出力端子の端子名を出力する一致出力端子出力手段を有することを特徴とした論理検証装置としたことである。
【００１０】
更に本発明の第一の特徴に関わる論理検証装置は、前記モニタ生成手段において、前記論理回路の初期化条件を読み込むことでプロパティを生成する機能を有し、かつ前記事象発生手段および前記比較手段はプロパティ検証により実現することを特徴とした論理検証装置としたことである。
【００１１】
本発明の第二の特徴は、ハードウェア記述言語により記述された論理回路の変更前後の動作が一致するかどうかを判定する論理検証手法において、変更前後の論理回路の記述を読み込む論理記述読込工程と、前記変更前後の論理記述について出力端子と順序回路の出力信号を抽出する信号抽出工程と、前記抽出した出力端子および順序回路の出力信号において前記変更前後の論理記述内に共通に存在する出力端子および順序回路の出力信号とどちらか一方のみにしか存在しない出力端子および順序回路の出力信号を選別する選別工程と、前記変更前の論理回路と前記変更後の論理回路とで前記共通に存在する出力端子および順序回路の出力信号の値を比較するためのモニタを生成するモニタ生成工程と、前記変更前後の論理回路の入力信号にすべての組み合わせを入力し、かつ前記論理回路に存在する順序回路毎に発生しうるすべての事象を発生させる事象発生工程と、前記変更前後の論理回路に共通に存在する入力信号に同じ値を入力するように前記事象発生工程を制御する同一信号入力制御工程と、前記事象発生工程にて発生させた事象毎に前記モニタ生成工程にて生成したモニタを用い前記共通に存在する出力端子および順序回路の出力信号の値を比較する比較工程と、前記選別工程によりどちらか一方のみにしか存在しない出力端子および順序回路の出力信号および前記比較結果から不一致した出力端子および順序回路の出力信号を出力する不一致信号出力工程と、前記比較結果から一致した出力端子の端子名を出力する一致出力端子出力工程を有することを特徴とした論理検証方法としたことである。
【００１２】
更に本発明の第二の特徴に関わる論理検証方法は、前記モニタ生成工程は前記論理回路の初期化条件を読み込むことで動作仕様記述を出力し、前記事象発生工程および前記比較工程はプロパティ検証を用いることを特徴とした論理検証方法としたことである。
【発明の効果】
【００１３】
以上説明したように、本発明によれば、論理変更により影響を受ける出力端子と影響を受けない出力端子および順序回路の出力信号を判別することで論理変更により検証すべき信号を明確にすることで検証効率を向上させることができる。
【発明を実施するための最良の形態】
【００１４】
以下、図面を参照して本発明の実施形態を説明する。
【００１５】
図1は本発明の一実施例を示す図である。変更前論理記述１はVerilogあるいはVHDLで記述した論理回路の設計データ、変更後論理記述２は変更前論理記述１に対し何らかの論理変更をしたVerilogあるいはVHDLで記述した論理回路の設計データである。論理記述読込手段３は、変更前論理記述１および変更後論理記述２を読み込む。出力端子/順序回路出力抽出手段４は、読み込まれた回路内に存在する出力端子と順序回路の出力信号を抽出する。信号名一致/不一致選別手段５は、前記抽出した信号の中で変更前後の論理回路において共通に存在する信号名があるかどうかを選別する。モニタ生成手段６は、前記信号名一致/不一致選別手段５にて共通に存在すると選別された信号の値を前記変更前後の論理回路間で比較するためのモニタを生成する。また、事象発生手段７は、論理記述読込手段３で読み込まれた前記変更前後の論理回路に対し、前記変更前後の論理回路の入力信号にすべての組み合わせを入力し、かつ前記論理回路に存在する順序回路毎に発生しうるすべての事象を発生する。同一信号入力制御手段８は、事象発生手段７にて前記変更前後の論理回路の入力信号にすべての組み合わせを入力する場合において、前記変更前後の論理回路に共通に存在する入力信号に同じ値を入力するように制御を行う。比較手段９は、事象発生手段７によって発生した事象毎にモニタ生成手段６によって生成されたモニタを用いて前記変更前後の論理回路内に共通に存在する信号の値が一致するかどうかの比較を行う。不一致信号出力手段１０は前記信号名一致/不一致選別手段５にて共通に存在しないと選別された信号および前記比較手段９の比較結果より信号の値が一致しないものを不一致信号データ１１として出力する。また、一致出力端子出力手段１２は前記比較手段９の比較結果より信号の値が一致する出力端子を一致出力端子データ１３として出力する。
【００１６】
図２は、それぞれ本例に用いる検証対象の変更前の論理回路L1、変更後の論理回路L２を示す概略図で、入力端子としてクロックclk、リセット信号reset、およびin1からin7が入力され、out1からout7が出力端子で、変更前の論理回路L1内のlogicA（l1）の部分をlogicB(l2)に変更したものが変更後の論理回路である。また、logicAおよびlogicBの出力信号はlogicC(l3)を経由し最終的に出力端子out3接続されており、logicAおよびlogicBの出力信号は出力端子out3にのみ影響を及ぼし、他の出力端子には影響を及ぼしてはいない。図３はlogicAの回路構成図で、内部信号sigAおよびsigBが入力され、アンド回路and1、オア回路or1、および順序回路ff1,ff2で構成され、ff1の出力が内部信号sigC、ff2の出力が内部信号sigDである。図４はlogicBの回路構成図で、内部信号sigAおよびsigBが入力され、アンド回路and1、オア回路or1、および順序回路ff1,ff2,ff1mで構成され、ff1の出力が内部信号sigC、ff2の出力が内部信号sigD、ff1mの出力が内部信号sigCmで、つまり、logicBはlogicAに対して内部信号sigCとオア回路or1の入力の間に順序回路ff1mが挿入され、ff1mの出力sigCmがor1に入力した回路構成に変更されたものである。図5はlogicCの回路構成図で、sigDは3つの順序回路ff3、ff4、ff5と3つの組み合わせ回路l4、l5、l6を経由して出力端子out3に接続されている。なお、組み合わせ回路l4、l5、l6には図示しない多数の入力信号がある。また、図５中の各順序回路ff3、ff4の出力信号はそれぞれsigE、sigFである。
【００１７】
次に、図2から図５で示した変更前後の論理回路の検証方法の詳細を説明するが、ここでは、図1の事象発生８および比較１０をプロパティ検証を用いて機能を実現した場合を例にとり説明する。図６は図1の事象発生手段７および比較手段９をプロパティ検証を用いて機能を実現した場合の本発明の実施例を示す図である。図６では図1のモニタ生成手段６がプロパティ生成手段１５、同一信号入力制御手段８はブロック生成手段１６、事象発生手段７および比較手段９がプロパティ検証１７に置き換わる。プロパティ生成手段１５は、信号名一致/不一致選別手段５で選別された一致信号情報と論理回路の初期化条件を記述した初期化条件１４の情報に基づきモニタの役割を果たすプロパティを生成する。また、ブロック生成手段１６は、変更前後の論理回路に共通に存在する入力信号に同じ値を入力するような制約を付加した形でプロパティ検証１８に入力する検証用の論理回路を生成する。すなわち、前記検証用の論理回路を使用することで変更前後の論理回路に共通に存在する入力信号に同じ値を入力する制御する必要はなくなる。プロパティ検証１７は前記生成されたプロパティと検証用の論理回路を入力として検証を実行する。図７に本例における論理回路の初期化条件を示す。ここで、論理回路はリセット信号resetが2クロックサイクル期間Highになれば次のサイクルで初期化される仕様とする。図中のXn(…)はnサイクル後の括弧内の状態を表す（n=1,2,…）。
【００１８】
図８は本発明の動作を説明するフローチャートである。ステップS01において、検証対象の論理記述を読み込む。開始直後のステップS01では変更前の論理記述を読み込む。ステップS02において、読み込んだ論理記述から出力端子または順序回路の出力信号を抽出し、信号名登録データに保存する。（信号名登録データは図示しない。）ステップS03において、二つの論理記述すなわち変更前後の論理記述が読み込まれたと判断されたならば、ステップS04へ進み、二つの論理記述が読み込まれていない場合はステップS01に戻り、変更後の論理記述に対して変更前の論理記述と同じ処理をする。ステップS04において、一つ目の信号名登録データすなわち変更前の信号名登録データに登録されている信号を取り出す。ステップS05において取り出した信号と一致するものが二つ目の信号名登録データすなわち変更後の信号名登録データに存在すると判断された場合はステップS06へ進み、判断されなかった場合はステップS07へ進む。ステップS06において、一致した信号名を信号名一致データに保存する。（信号名一致データは図示しない。）ステップS07において、一致するものがない信号名を不一致信号データとして出力する。ステップS08において、ステップS04にと取り出された信号名を変更前および変更後の論理記述に対応する信号名登録データから削除する。ステップS09において、一つ目の信号名登録データが空かどうか判断されればステップS10に進み、判断されなければステップS04に戻る。ステップS10において、二つ目の信号名登録データに残りのデータを不一致信号データとして出力する。本例の変更前後の論理記述に対するステップS１１に進んだ時点の不一致信号データの例を図９に示す。logicB内に存在する内部信号sigCmのみが不一致する信号になる。
【００１９】
ステップS11において、検証用の論理回路を生成する。図10にステップS11において生成した検証用の論理回路L3を示す。変更前後の論理回路L1およびL2をサブブロック（subA,subB）とし、かつ、変更前後の論理回路において共通に存在する同一の入力信号に対しては、前記変更前の論理回路に対応するサブブロックの入力信号と前記変更後の論理回路に対応するサブブロックの入力信号に同じ信号を入力として接続した論理回路を生成する。これにより、変更前後の論理回路に共通に存在する入力信号に同じ値を入力するような制約を付加した形の論理回路になる。
【００２０】
ステップS12において、初期化条件と信号名一致データからプロパティを生成する。図11にステップS12において生成するプロパティを示す。左側のプロパティは初期化された次のクロックサイクルでは変更前後の論理回路に対応するサブブロックの信号の値は一致することを示すプロパティで、右側のプロパティはあるサイクルにおいて変更前後の論理回路に対応するサブブロックの信号の値が一致していれば、次のクロックサイクルにおいても信号の値は一致することを示すプロパティである。前記二つのプロパティを用いることにより回路の初期化以降は、比較する信号間の値は常に等しいことを示すプロパティになる。ここで、図中のsig1,sig2、singnは信号名一致データに登録された変更前後の論理回路内に存在するその他の内部信号であり、すべて順序回路の出力信号である。
【００２１】
ステップS13において、ステップS11で生成した検証用論理回路L3と前記プロパティを入力してプロパティ検証を実行する。ステップS14において、プロパティ検証結果にエラーがあると判断された場合にはステップS15に進み、エラーがあると判断されない場合はステップS16に進む。ステップS15において、エラーとなるプロパティを削除し、エラーとなる信号を不一致信号データとして出力し、ステップS13に戻る。ステップS16において、一致している出力端子を一致信号データとして出力し、本フローは終了する。
【００２２】
本例では内部信号sigD、sigE、sigFと出力端子out3がプロパティ検証でエラーとなる信号であるので、図8のフローチャートのステップS13において、最後にプロパティ検証が実行されるプロパティは、図12に示すように図８のプロパティに対して内部信号sigD、sigE、sigFおよび出力端子out3に関するプロパティが削除されたプロパティになり、また、最終的な不一致信号データと一致出力端子データはそれぞれ図13、図14のようになり、sigCm、sigD、sigE、sigF、およびout3が不一致信号データとして出力され、out1、out2、out3、out4、out5、out6、out7が一致出力端子データとして出力される。
【図面の簡単な説明】
【００２３】
【図１】本発明の一実施例を示す図である。
【図２】変更前後の論理回路の概略図である。
【図３】変更前の論理回路内の変更論理の回路図である。
【図４】変更後の論理回路内の変更論理の回路図である。
【図５】変更論理回路の出力から出力端子の間にある論理の回路図である。
【図６】図1に示す本発明の一実施例においてプロパティ検証を使用した場合の本発明の一実施例を示す図である。
【図７】検証対象の論理回路の初期化条件を示す図である。
【図８】図６に示す本発明の一実施例のフローを示す図である。
【図９】図６のフロー中に示すステップS11に進んだ時点の不一致信号データを示す図である。
【図１０】検証用の論理回路のブロック図である。
【図１１】図６のフロー中に示すステップS12において作成されるプロパティを示す図である。
【図１２】最後にプロパティ検証が実行されるときに用いられるプロパティを示す図である。
【図１３】最終的な不一致信号データを示す図である。
【図１４】一致出力端子データを示す図である。
【符号の説明】
【００２４】
1  変更前論理記述
2  変更後論理記述
3  論理記述読込手段
4  出力端子/順序回路出力手段
5  信号名一致/不一致選別手段
6  モニタ生成手段
7  事象発生手段
8  同一信号入力制御手段
9  比較手段
10  不一致信号出力手段
11  不一致信号データ
12  一致出力端子出力手段
13  一致出力端子データ
14  初期化条件
15  プロパティ生成手段（モニタ生成手段）
16  ブロック生成手段（同一信号入力制御手段）
17  プロパティ検証（事象発生手段、比較手段）
18  最初に出力される不一致信号データ
L1  変更前論理回路
L2  変更後論理回路
l1  logicA
l2  logicB
l3  logincC
l4,l5.l6  組み合わせ回路（comb）
and1  アンド回路
or1  オア回路
ff1,ff2,ff3,ff4,ff5,ff1m  順序回路
【図１】
2007004560.tif 000003
【図２】
2007004560.tif 000004
【図３】
2007004560.tif 000005
【図４】
2007004560.tif 000006
【図５】
2007004560.tif 000007
【図６】
2007004560.tif 000008
【図７】
2007004560.tif 000009
【図８】
2007004560.tif 000010
【図９】
2007004560.tif 000011
【図１０】
2007004560.tif 000012
【図１１】
2007004560.tif 000013
【図１２】
2007004560.tif 000014
【図１３】
2007004560.tif 000015
【図１４】
2007004560.tif 000016