米国特許情報 | 欧州特許情報 | 国際公開(PCT)情報 | Google の米国特許検索
 
     特許分類
A 農業
B 衣類
C 家具
D 医学
E スポ−ツ;娯楽
F 加工処理操作
G 机上付属具
H 装飾
I 車両
J 包装;運搬
L 化学;冶金
M 繊維;紙;印刷
N 固定構造物
O 機械工学
P 武器
Q 照明
R 測定; 光学
S 写真;映画
T 計算機;電気通信
U 核技術
V 電気素子
W 発電
X 楽器;音響


  ホーム -> 計算機;電気通信 -> キヤノン株式会社

発明の名称 論理検証装置および論理検証方法
発行国 日本国特許庁(JP)
公報種別 公開特許公報(A)
公開番号 特開2007−4560(P2007−4560A)
公開日 平成19年1月11日(2007.1.11)
出願番号 特願2005−184950(P2005−184950)
出願日 平成17年6月24日(2005.6.24)
代理人 【識別番号】100090538
【弁理士】
【氏名又は名称】西山 恵三
発明者 長尾 宙馬
要約 課題
論理変更により影響を受ける出力端子と影響を受けない出力端子および順序回路の出力信号を判別することで、論理変更により検証すべき信号を明確することで検証効率を向上させることを目的とする。

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




 

 


     NEWS
会社検索順位 特許の出願数の順位が発表

URL変更
平成6年
平成7年
平成8年
平成9年
平成10年
平成11年
平成12年
平成13年


 
   お問い合わせ info@patentjp.com patentjp.com   Copyright 2007-2013