(57)【要約】【課題】プロパティ検証に要する時間を短縮することのできるＬＳＩ設計検証装置を提供する。【解決手段】ＬＳＩ設計検証装置１は、算術演算記述抽出部１１が、機能記述１００から算術演算記述を抽出し、入力信号符号表現判定部１２が、抽出された算術演算記述の入力信号がゼロ拡張符号表現であるかを判定し、ビット値固定信号抽出部１３が、入力信号がゼロ拡張符号表現であると判定された算術演算記述の出力信号のビット列から、入力信号のゼロ拡張されたビットの影響を受けるビット値固定信号を抽出し、プロパティ生成部１４が、設計仕様２００にもとづくプロパティを生成するときに、抽出されたビット値固定信号は検証対象から除外してプロパティを生成し、プロパティ検証部１５が、プロパティ生成部１４により生成されたプロパティを使用して機能記述１００のプロパティ検証を実行する。【選択図】図１
2008181210.tif 000002
【特許請求の範囲】
【請求項１】
入力された機能記述に対してプロパティ検証を行うＬＳＩ設計検証装置であって、
前記機能記述の構造を解析し、演算出力信号のビット列の中に固定値となるビットを含む演算記述を抽出し、前記固定値となるビットを検証対象から除外したプロパティを生成し、プロパティ検証に使用することを特徴とするＬＳＩ設計検証装置。
【請求項２】
入力された機能記述に対してプロパティ検証を行うＬＳＩ設計検証装置であって、
前記機能記述から算術演算記述を抽出する算術演算記述抽出手段と、
抽出された前記算術演算記述の入力信号がゼロ拡張符号表現であるかを判定する入力信号符号表現判定手段と、
前記入力信号がゼロ拡張符号表現であると判定されたときに、前記抽出された前記算術演算記述の出力信号のビット列から、前記入力信号のゼロ拡張されたビットの影響を受けるビットをビット値固定信号として抽出するビット値固定信号保存手段と、
前記ビット値固定信号を検証対象から除外したプロパティを生成するプロパティ生成手段と、
生成された前記プロパティを使用して前記機能記述のプロパティ検証を実行するプロパティ検証手段と
を備えることを特徴とするＬＳＩ設計検証装置。
【請求項３】
前記入力信号符号表現判定手段は、
前記機能記述から抽出されたゼロ拡張符号表現の信号が格納されたデータベースを読み出して、前記判定を行うことを特徴とする請求項２に記載のＬＳＩ設計検証装置。
【請求項４】
入力された機能記述をプロパティと比較してプロパティ検証を行うＬＳＩ設計検証装置であって、
前回のプロパティ検証においてタイムアウトを発生させた信号を前記プロパティから除外して次回のプロパティ検証を実行することを特徴とするＬＳＩ設計検証装置。
【請求項５】
入力された機能記述をプロパティと比較してプロパティ検証を行うＬＳＩ設計検証装置であって、
プロパティ検証結果を解析し、タイムアウトを発生させた信号をタイムアウト発生信号として検出するタイムアウト発生信号検出手段と、
検出された前記タイムアウト発生信号および前記タイムアウト発生信号の接続先の信号のビット列の中でプロパティ検証が未終了のビットを抽出する検証未終了ビット抽出手段と、
抽出された前記プロパティ検証が未終了のビットを前記プロパティから除外して、タイムアウト発生信号除外プロパティを生成するタイムアウト発生信号除外プロパティ生成手段と、
プロパティ検証の再実行時に、前記タイムアウト発生信号除外プロパティを使用して前記機能記述のプロパティ検証を実行するプロパティ検証手段と
を備えることを特徴とするＬＳＩ設計検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＬＳＩ設計検証装置に関する。
【背景技術】
【０００２】
近年、ＬＳＩに集積される回路の大規模化、複雑化により、その設計検証の効率化が求められている。そこで、従来のシミュレーションによる設計検証に代わって、設計結果を数学的に解析するフォーマル・ベリフィケーション（形式的論理検証）技術の実用化が進展している。このフォーマル・ベリフィケーションの１つに、プロパティ検証がある。プロパティ検証とは、設計した回路の機能記述言語による機能記述が設計仕様（プロパティ）を満たしているかどうかを検証するものである。
【０００３】
このプロパティ検証を行う検証装置として、検証対象回路の出力に対するプロパティを生成し、設計結果の回路の出力信号がプロパティと一致しているかの比較検証を行い、その検証結果を表示するＬＳＩ検証装置が提案されている（例えば、特許文献１参照。）。
【０００４】
しかし、従来のプロパティ検証装置では、回路動作上問題とならない機能記述に対して、プロパティ違反を指摘することがある。このような、いわゆる擬似違反が発生するのは、おもに、補数表現を用いた算術演算やシフト演算を行う機能記述に対する検証を行った場合である。例えば、上位２ビットに０を拡張したゼロ拡張補数表現を用いた４ビットの変数どうしの乗算を行った場合、８ビットの出力信号の上位４ビットは常に０に固定される。ところが、通常、出力信号に対するプロパティは「各ビットに０と１の両方の値が出力されたら正常」とされるため、上述の演算結果の上位４ビットはプロパティ違反として検出される。
【０００５】
このような違反が検出された場合、それが擬似違反かどうかを、検証者が確認する必要がある。しかし、プロパティ違反の発生した機能記述に影響を及ぼす信号がロジックコーン上の非常に深い位置にある場合など、その確認に膨大な解析時間を要するという問題が発生する。
【０００６】
そのほかに、従来のプロパティ検証装置では、検証対象がロジックコーン上の深い位置にある場合、そのプロパティを検証するための状態を設定するまでに多大な時間を要し、タイムアウトとなることがある。そのようなときに、そのほかの違反箇所を修正して、プロパティ検証を再実行した場合、タイムアウトを発生する記述部分も再度検証されるため、修正箇所のみ確認したい場合でも、前回と同様の処理時間を要するという問題が発生する。
【特許文献１】特開２００５−１９６６８１号公報  （第５−６ページ、図１）
【発明の開示】
【発明が解決しようとする課題】
【０００７】
そこで、本発明の目的は、プロパティ検証に要する時間を短縮することのできるＬＳＩ設計検証装置を提供することにある。
【課題を解決するための手段】
【０００８】
本発明の一態様によれば、入力された機能記述に対してプロパティ検証を行うＬＳＩ設計検証装置であって、前記機能記述の構造を解析し、演算出力信号のビット列の中に固定値となるビットを含む演算記述を抽出し、前記固定値となるビットを検証対象から除外したプロパティを生成し、プロパティ検証に使用することを特徴とするＬＳＩ設計検証装置が提供される。
【０００９】
また、本発明の別の一態様によれば、入力された機能記述に対してプロパティ検証を行うＬＳＩ設計検証装置であって、前記機能記述から算術演算記述を抽出する算術演算記述抽出手段と、抽出された前記算術演算記述の入力信号がゼロ拡張符号表現であるかを判定する入力信号符号表現判定手段と、前記入力信号がゼロ拡張符号表現であると判定されたときに、前記抽出された前記算術演算記述の出力信号のビット列から、前記入力信号のゼロ拡張されたビットの影響を受けるビットをビット値固定信号として抽出するビット値固定信号保存手段と、前記ビット値固定信号を検証対象から除外したプロパティを生成するプロパティ生成手段と、生成された前記プロパティを使用して前記機能記述のプロパティ検証を実行するプロパティ検証手段とを備えることを特徴とするＬＳＩ設計検証装置が提供される。
【００１０】
また、本発明のさらに別の一態様によれば、入力された機能記述をプロパティと比較してプロパティ検証を行うＬＳＩ設計検証装置であって、前回のプロパティ検証においてタイムアウトを発生させた信号を前記プロパティから除外して次回のプロパティ検証を実行することを特徴とするＬＳＩ設計検証装置が提供される。
【００１１】
また、本発明のさらに別の一態様によれば、入力された機能記述をプロパティと比較してプロパティ検証を行うＬＳＩ設計検証装置であって、プロパティ検証結果を解析し、タイムアウトを発生させた信号をタイムアウト発生信号として検出するタイムアウト発生信号検出手段と、検出された前記タイムアウト発生信号および前記タイムアウト発生信号の接続先の信号のビット列の中でプロパティ検証が未終了のビットを抽出する検証未終了ビット抽出手段と、抽出された前記プロパティ検証が未終了のビットを前記プロパティから除外して、タイムアウト発生信号除外プロパティを生成するタイムアウト発生信号除外プロパティ生成手段と、プロパティ検証の再実行時に、前記タイムアウト発生信号除外プロパティを使用して前記機能記述のプロパティ検証を実行するプロパティ検証手段とを備えることを特徴とするＬＳＩ設計検証装置が提供される。
【発明の効果】
【００１２】
本発明によれば、ＬＳＩに集積される回路の機能記述に対するプロパティ検証に要する時間を短縮することができる。
【発明を実施するための最良の形態】
【００１３】
以下、本発明の実施例を図面を参照して説明する。
【実施例１】
【００１４】
図１は、本発明の実施例１に係るＬＳＩ設計検証装置１の構成の例を示すブロック図である。
【００１５】
本実施例のＬＳＩ設計検証装置１へは、設計した回路の機能記述言語による機能記述１００と、その回路の設計仕様２００が入力される。
【００１６】
ＬＳＩ設計検証装置１は、機能記述１００から算術演算記述を抽出する算術演算記述抽出部１１と、抽出された算術演算記述の入力信号がゼロ拡張符号表現であるかを判定する入力信号符号表現判定部１２と、算術演算記述の入力信号がゼロ拡張符号表現であると判定されたときに、その算術演算記述の出力信号のビット列から、入力信号のゼロ拡張されたビットの影響を受けるビットを、ビット値固定信号として抽出するビット値固定信号抽出部１３と、設計仕様２００にもとづくプロパティを生成するときに、抽出されたビット値固定信号は検証対象から除外してプロパティを生成するプロパティ生成部１４と、プロパティ生成部１４により生成されたプロパティを使用して機能記述１００のプロパティ検証を実行し、検証結果３００を出力するプロパティ検証部１５と、を備える。
【００１７】
図２に、ＬＳＩ設計検証装置１に入力される機能記述１００の記述例を示す。
【００１８】
この例では、（Ａ）に示す部分にゼロ拡張補数表現を用いる記述がある。この場合、信号ｄｏｕｔ２、ｄｏｕｔ３は、２ビットの信号ｄｉｎ１、ｄｉｎ２のそれぞれの上位側に、２ビットの‘０'が付加された信号である。
【００１９】
また、（Ｂ）に示す部分には、このゼロ拡張された４ビットの信号ｄｏｕｔ２［３：０］、ｄｏｕｔ３［３：０］を入力として乗算を行い、８ビットの出力信号ｍｕｌ＿ｏｕｔ［７：０］を得る乗算記述がある。
【００２０】
図３に、この乗算記述に乗算において、入力信号のゼロ拡張の影響が、出力信号に及ぶ様子を示す。
【００２１】
４ビットの信号ｄｏｕｔ２［３：０］、ｄｏｕｔ３［３：０］の上位側２ビット、すなわち、ｄｏｕｔ２［３：２］、ｄｏｕｔ３［３：２］が‘０'に固定されているので、ｄｏｕｔ２［３：０］とｄｏｕｔ３［３：０］の乗算を行うと、８ビットの乗算結果のうちの、上位４ビットは、必ず‘０'となる。すなわち、乗算結果の出力信号ｍｕｌ＿ｏｕｔ［７：０］の上位側４ビットｍｕｌ＿ｏｕｔ［７：４］は、ビット値が‘０'に固定された信号となる。
【００２２】
従来、このようなビット値が固定された出力信号に対してプロパティ検証を行うと、プロパティ違反が出力される。しかし、この例の場合は、機能動作的には正常であり、擬似エラーである。
【００２３】
そこで、本実施例のＬＳＩ設計検証装置１は、このような、符号表現に影響される擬似エラーの発生を抑制するプロパティを生成してプロパティ検証を行うようにする。
【００２４】
乗算入力のゼロ拡張されたビット幅と、その影響を受けてゼロ固定となる出力のビット幅との関係は、一義に定まるので、乗算出力のゼロ固定となるビット幅は、入力のゼロ拡張されたビット幅がわかれば、求めることができる。
【００２５】
乗算出力のゼロ固定となるビット幅を求めるために、ＬＳＩ設計検証装置１は、まず、算術演算記述抽出部１１により、機能記述１００から算術演算記述を抽出し、その入力信号にゼロ拡張補数表現が使用されているかどうかを、入力信号符号表現判定部１２により判定する。
【００２６】
このとき、入力信号符号表現判定部１２は、その判定に、機能記述１００から抽出されたゼロ拡張符号表現の信号が格納されたデータベースを使用する。
【００２７】
図４に、このデータベース生成関連のブロック図を示す。
【００２８】
ゼロ拡張符号表現信号データベース１７へは、ゼロ拡張符号表現信号抽出部１６により機能記述１００から抽出された、ゼロ拡張符号表現を使用した信号が格納される。
【００２９】
入力信号符号表現判定部１２は、入力された算術演算記述の入力信号を、ゼロ拡張符号表現信号データベース１７から読み出したゼロ拡張符号表現信号と順次照合し、入力信号に、ゼロ拡張符号表現信号データベース１７から読み出したゼロ拡張符号表現信号が含まれるときは、その入力信号をゼロ拡張符号表現を使用した信号であると判定する。そして、ゼロ拡張符号表現を使用した信号であると判定したとき、入力信号符号表現判定部１２は、ゼロ拡張符号表現信号データベース１７から読み出したゼロ拡張符号表現信号を出力する。
【００３０】
図５に、ゼロ拡張符号表現信号抽出部１６が、機能記述１００からゼロ拡張符号表現信号を抽出するときの処理の手順を示す。
【００３１】
ゼロ拡張符号表現信号抽出部１６は、まず、機能記述１００の構造を解析し（手順Ｓ０１）、補数表現された記述を抽出する（手順Ｓ０２）。
【００３２】
続いて、ゼロ拡張符号表現信号抽出部１６は、その記述が演算記述内で直接符号拡張されたものかどうかを判定する（手順Ｓ０３）。演算記述内で直接符号拡張されたものであるときは（ＹＥＳ）、手順Ｓ０２に戻って、次の補数表現された記述の抽出へ移行する。
【００３３】
一方、抽出した記述が演算記述内で直接符号拡張されたものでないときは（ＮＯ）、ゼロ拡張補数表現を使用しているかどうかを判定する（手順Ｓ０４）。ゼロ拡張補数表現を使用していないときは（ＮＯ）、手順Ｓ０２に戻って、次の補数表現された記述の抽出へ移行する。
【００３４】
これに対して、抽出した記述がゼロ拡張補数表現を使用しているときは（ＹＥＳ）、そのゼロ拡張部分の信号をゼロ拡張符号表現信号として、ゼロ拡張符号表現信号データベース１７へ格納する（手順Ｓ０５）。
【００３５】
例えば、図２に示した機能記述の例では、（Ａ）の部分のｄｏｕｔ２、ｄｏｕｔ３に関する記述が、補数表現された記述として抽出され（手順Ｓ０２）、ゼロ拡張補数表現を使用した記述と判定される（手順Ｓ０４）。そして、このｄｏｕｔ２、ｄｏｕｔ３のゼロ拡張部分の信号、すなわち、ｄｏｕｔ２［３：２］、ｄｏｕｔ３［３：２］が、ゼロ拡張符号表現信号として、ゼロ拡張符号表現信号データベース１７へ格納される（手順Ｓ０５）。
【００３６】
このようにして、機能記述１００から総てのゼロ拡張符号表現信号を抽出し、ゼロ拡張符号表現信号データベース１７へ格納すると、ゼロ拡張符号表現信号抽出部１６の処理は終了する。
【００３７】
次に、ＬＳＩ設計検証装置１におけるプロパティ生成について、図６を用いて説明する。
【００３８】
図６は、ＬＳＩ設計検証装置１が、乗算出力のゼロ固定となるビットを抽出し、その部分を除外したプロパティを生成して、プロパティ検証を実行するまでの動作の流れを示すフロー図である。
【００３９】
入力された機能記述１００に対して、算術演算記述抽出部１１は、構造解析を行い（Ｓ１１）、算術演算記述を抽出する（Ｓ１２）。
【００４０】
抽出された算術演算記述に対して、入力信号符号表現判定部１２は、入力信号にゼロ拡張符号表現信号が使用されているかどうか判定する（Ｓ１３）。入力信号にゼロ拡張符号表現信号が使用されていないときは（ＮＯ）、Ｓ１２へ戻り、次の算術演算記述の抽出へ移行する。
【００４１】
入力信号にゼロ拡張符号表現信号が使用されていると判定したときは（ＹＥＳ）、入力信号符号表現判定部１２は、算術演算記述の入力信号として使用されているゼロ拡張符号表現信号を出力する。
【００４２】
このゼロ拡張符号表現信号の出力を受けて、ビット値固定信号抽出部１３は、その算術演算記述の出力信号のビット列のうち、入力のゼロ拡張符号表現信号のゼロ拡張の影響を受けるビットを特定し（Ｓ１４）、ビット値固定信号として抽出する（Ｓ１５）。
【００４３】
例えば、図２に示した機能記述の例で、（Ｂ）の部分が算術演算記述として抽出され、その入力信号のゼロ拡張符号表現信号として、ｄｏｕｔ２［３：２］、ｄｏｕｔ３［３：２］が入力されると、ビット値固定信号抽出部１３は、ｍｕｌ＿ｏｕｔ［７：４］をビット値固定信号として抽出する。
【００４４】
上述のフローを実行して、総てのビット値固定信号の抽出が終わると、プロパティ生成部１４は、抽出されたビット値固定信号を検証対象から除外するようにして、プロパティを生成する（Ｓ１６）。
【００４５】
最後に、プロパティ検証部１５は、プロパティ生成部１４により生成されたプロパティを使用して機能記述１００のプロパティ検証を実行する（Ｓ１７）。
【００４６】
このような本実施例のＬＳＩ設計検証装置によれば、機能仕様上固定値を出力する信号に対するプロパティが生成されないので、プロパティ検証対象数が削減され、プロパティ検証に要する時間を短縮することができる。
【００４７】
また、プロパティ検証実行時に、機能仕様上固定値を出力する信号に対する擬似エラーが発生しないので、プロパティ検証結果の解析に要する時間を短縮することができる。
【実施例２】
【００４８】
本実施例では、プロパティ検証を繰り返し実行するときに、毎回、同じ信号にタイムアウトが発生することを抑止することのできるＬＳＩ設計検証装置の例を示す。
【００４９】
図７は、本発明の実施例２に係るＬＳＩ設計検証装置２の構成の例を示すブロック図である。
【００５０】
本実施例のＬＳＩ設計検証装置２は、設計した回路の機能記述言語による機能記述１００と、その回路に対するプロパティ４００が入力され、１回目のプロパティ検証では、その入力されたプロパティ４００をそのまま使用して、機能記述１００に対するプロパティ検証を実行するプロパティ検証部２１と、その実行時にタイムアウトが発生したときは、プロパティ検証結果３００を解析し、タイムアウトを発生させた信号をタイムアウト発生信号として検出するタイムアウト発生信号検出部２２と、検出されたタイムアウト発生信号およびそのタイムアウト発生信号の接続先の信号のビット列の中でプロパティ検証が未終了のビットを抽出する検証未終了ビット抽出部２３と、抽出されたプロパティ検証が未終了のビットをプロパティ４００から除外して、タイムアウト発生信号除外プロパティ５００を生成するタイムアウト発生信号除外プロパティ生成部２４と、を備える。
【００５１】
ここで、プロパティ検証部２１は、プロパティ検証の再実行時には、タイムアウト発生信号除外プロパティ生成部２４により生成されたタイムアウト発生信号除外プロパティ５００を使用してプロパティ検証を実行する。
【００５２】
これにより、１回目のプロパティ検証時にタイムアウトが発生したビットは、２回目以降のプロパティ検証の対象から除外される。
【００５３】
次に、本実施例のＬＳＩ設計検証装置２の動作について説明する。
【００５４】
図８は、ＬＳＩ設計検証装置２の動作の流れを示すフロー図である。
【００５５】
プロパティ検証部２１による１回目のプロパティ検証実行でタイムアウトが発生したときに、タイムアウト発生信号検出部２２は、その結果を解析し、タイムアウトを発生させた信号（タイムアウト信号）の検出を行う（Ｓ２１）。
【００５６】
次に、検証未終了ビット抽出部２３が、タイムアウト信号のビット列の中で、プロパティ検証が未終了となっているビットを抽出する（Ｓ２２）。
【００５７】
また、検証未終了ビット抽出部２３は、そのプロパティ検証が未終了となっているビットの情報をタイムアウト発生信号除外プロパティ生成部２４へ送出する（Ｓ２３）。
【００５８】
さらに、検証未終了ビット抽出部２３は、そのプロパティ検証が未終了となっているビットが、他の信号に接続されているかどうかチェックする（Ｓ２４）。これは、プロパティ検証が未終了となっているビットが他の信号に接続されている場合、その接続先の信号にもタイムアウトが発生する可能性があるからである。
【００５９】
プロパティ検証が未終了となっているビットが他の信号に接続されていることが判明したときは（ＹＥＳ）、その接続先の信号を検索し（Ｓ２５）、検出した接続先の信号に対しても、Ｓ２２以降のフローを実行する。その結果、接続先の信号のビット列の中でプロパティ検証が未終了のビットを抽出したときは、その情報をタイムアウト発生信号除外プロパティ生成部２４へ送出する。
【００６０】
プロパティ検証が未終了となっているビットが他の信号に接続されていないことが判明したときは（ＮＯ）、タイムアウト発生信号除外プロパティ生成部２４が、検証未終了ビット抽出部２３から送出されてきた情報をもとに、プロパティ検証が未終了のビットをプロパティ４００から除外して、タイムアウト発生信号除外プロパティ５００を生成する（Ｓ２６）。
【００６１】
その後、機能記述１００が修正されたりして、プロパティ検証の再実行が必要となったときは、プロパティ検証部２１は、このタイムアウト発生信号除外プロパティ５００を用いてプロパティ検証を行う。
【００６２】
このような本実施例によれば、プロパティ検証の再実行時のタイムアウトの発生を抑制することができるので、初回実行時に比べてプロパティ検証に要する時間を短縮することができる。
【図面の簡単な説明】
【００６３】
【図１】本発明の実施例１に係るＬＳＩ設計検証装置の構成の例を示すブロック図。
【図２】機能記述の例を示す図。
【図３】ゼロ拡張補数表現の信号どうしの乗算の様子を示す図。
【図４】実施例１のＬＳＩ設計検証装置の入力信号符号表現判定部が使用するデータベース生成関連のブロック図。
【図５】実施例１のゼロ拡張符号表現信号抽出部の処理の手順を示すフロー図。
【図６】実施例１に係るＬＳＩ設計検証装置の動作の流れを示すフロー図。
【図７】本発明の実施例２に係るＬＳＩ設計検証装置の構成の例を示すブロック図。
【図８】実施例２に係るＬＳＩ設計検証装置の動作の流れを示すフロー図。
【符号の説明】
【００６４】
１、２  ＬＳＩ設計検証装置
１１  算術演算記述抽出部
１２  入力信号符号表現判定部
１３  ビット値固定信号抽出部
１４  プロパティ生成部
１５、２１  プロパティ検証部
１６  ゼロ拡張符号表現信号抽出部
１７  ゼロ拡張符号表現信号データベース
２２  タイムアウト発生信号検出部
２３  検証未終了ビット抽出部
２４  タイムアウト発生信号除外プロパティ生成部
【図１】
2008181210.tif 000003
【図２】
2008181210.tif 000004
【図３】
2008181210.tif 000005
【図４】
2008181210.tif 000006
【図５】
2008181210.tif 000007
【図６】
2008181210.tif 000008
【図７】
2008181210.tif 000009
【図８】
2008181210.tif 000010