(57)【特許請求の範囲】
【請求項１】
回路記述とアサーション記述の等価性を検証する半導体集積回路の検証装置であって、
前記アサーション記述に基づいて前記回路記述のアサーションベース検証を行い、
前提条件が成立するアサーション記述に記述された信号の動作が前記回路記述において守られている場合にパス情報を生成し、前記信号の動作が前記回路記述において守られていない場合にフェイル情報を生成するアサーションベース検証部と、
前記アサーション記述から前記フェイル情報に対応する信号を抽出し、前記抽出された信号に対する前記回路記述の入出力論理を生成する論理生成部と、
前記論理生成部によって生成された入出力論理に基づいて信号制約を生成する信号制約生成部と、
前記信号制約生成部によって生成された信号制約の正当性を評価する評価部と、
前記評価部によって正当と評価された信号制約を出力する出力部と、を備えることを特徴とする半導体集積回路の検証装置。
【請求項２】
前記評価部は、前記信号制約が適用されたときに、前記前提条件が成立しないアサーション記述が存在する場合または前記アサーション記述に記述された信号が固定値となる場合に、前記信号制約を不当と評価する請求項１に記載の半導体集積回路の検証装置。
【請求項３】
前記評価部によって不当と評価された信号制約が存在する場合に、前記アサーション記述を修正するアサーション記述修正部を更に備え、
前記出力部は、前記アサーション記述修正部によって修正されたアサーション記述を出力する請求項１または２に記載の半導体集積回路の検証装置。
【請求項４】
前記論理生成部は、前記入出力論理に基づいて有限状態機械を生成する請求項１ないし３のいずれか１項に記載の半導体集積回路の検証装置。
【請求項５】
前記信号制約生成部は、複数の信号の組合せを統合し、前記統合された複数の信号の組合せの中から項数の最も少ない組合せを前記信号制約として生成する請求項１ないし４のいずれか１項に記載の半導体集積回路の検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、半導体集積回路の検証装置に関し、特に、アサーションベース検証を行う半導体集積回路の検証装置に関する。
【背景技術】
【０００２】
近年、半導体集積回路の検証装置として、アサーション記述のような検証言語記述を用いて検証を行う半導体集積回路の検証装置が知られている（特許文献１）。
【０００３】
この検証装置では、検証結果が不具合となる原因として、回路記述の記述ミス、検証言語記述の記述ミス、仕様において禁止されている入力信号の組合せに起因する異常動作および検証言語記述の前提条件の不足などが考えられる。
【０００４】
一般的な検証装置では、不具合が発生する回路遷移状態の中から任意の１種類の波形が不具合情報として出力される。検証者は、この不具合情報に基づいて、上記４つの原因の中から不具合の原因を特定するために試行錯誤を繰り返す。従って、半導体集積回路の検証には極めて膨大な時間を要する。
【０００５】
特に、フォーマルツールの場合には、数学的な手法を使用することによって入力信号の組合せを網羅した検証を行うので、上記異常動作および上記前提条件の不足に起因する不具合情報が多く発生する。これらの不具合情報は実際には意味の無い情報（以下、「擬似エラー」という）であるにもかかわらず、検証者は全ての擬似エラーを除去しなければならない。例えば、「リクエスト系６信号はワンホットである（全て０の場合も許可する）」という仕様が定められているときに６種類の１ｂｉｔリクエスト信号があった場合には、６４通り（２６信号）のうち５７通り、すなわち８９％の信号の組合せの不具合情報が疑似エラーとなる。このような場合にまで検証者が試行錯誤を行うことは極めて非効率である。
【特許文献１】特開２００６−５３８１３号公報
【発明の開示】
【発明が解決しようとする課題】
【０００６】
本発明の目的は、半導体集積回路の検証効率を向上させる半導体集積回路の検証装置を提供することである。
【課題を解決するための手段】
【０００７】
本発明の第１態様によれば、
回路記述とアサーション記述の等価性を検証する半導体集積回路の検証装置であって、
前記アサーション記述に基づいて前記回路記述のアサーションベース検証を行い、  前提条件が成立するアサーション記述に記述された信号の動作が前記回路記述において守られている場合にパス情報を生成し、前記信号の動作が前記回路記述において守られていない場合にフェイル情報を生成するアサーションベース検証部と、
前記アサーション記述から前記フェイル情報に対応する信号を抽出し、前記抽出された信号に対する前記回路記述の入出力論理を生成する論理生成部と、
前記論理生成部によって生成された入出力論理に基づいて信号制約を生成する信号制約生成部と、
前記信号制約生成部によって生成された信号制約の正当性を評価する評価部と、
前記評価部によって正当と評価された信号制約を出力する出力部と、を備えることを特徴とする半導体集積回路の検証装置が提供される。
【発明の効果】
【０００８】
本発明によれば、半導体集積回路の検証効率を向上させることができる。
【発明を実施するための最良の形態】
【０００９】
以下、本発明の実施例について図面を参照して説明する。なお、以下の実施例は、本発明の実施の一形態であって、本発明の範囲を限定するものではない。
【実施例１】
【００１０】
はじめに、本発明の実施例１について説明する。本発明の実施例１は、不具合を抑制するための信号制約または修正されたアサーション記述を出力する半導体集積回路の検証装置の例である。
【００１１】
図１は、本発明の実施例１に係る半導体集積回路の検証装置１００の構成を示すブロック図である。
【００１２】
この検証装置１００は、入力部１０１、アサーションベース検証部１０２、論理生成部１０３、信号制約生成部１０４、評価部１０５、検証記述言語修正部１０６、および出力部１０７を備えている。
【００１３】
入力部１０１は、回路記述１０１Ａ、アサーション記述１０１Ｂ、およびテスト記述１０１Ｃの入力を受け付け、入力された回路記述１０１Ａ、アサーション記述１０１Ｂ、およびテスト記述１０１Ｃを生成する。入力部１０１は、たとえばキーボードやマウスなどの検証装置１００に接続される入力装置のインタフェースである。回路記述１０１Ａは、たとえば図２に示されるようなレジスタ転送レベル記述（以下、「ＲＴＬ記述」という）である。アサーション記述１０１Ｂは、設計仕様、前提条件、および図３に示されるような記述を含む。テスト記述１０１Ｃは、たとえばテストベクタやシミュレーションパターンである。
【００１４】
アサーションベース検証部１０２は、たとえばフォーマル検証技術またはシミュレーション技術を用いて、回路記述１０１Ａに対するアサーション記述１０１Ｂの前提条件の成否を判断する。また、アサーションベース検証部１０２は、前提条件が成立するアサーション記述１０１Ｂに記述された信号の動作がアサーションベース検証の実行中に回路記述１０１Ａにおいて必ず守られている（すなわち、不具合が発生していない）場合にはパス情報１０２Ａを生成し、アサーション記述１０１Ｂで記述された信号の動作がアサーションベース検証の実行中に回路記述１０１Ａにおいて守られない（すなわち、不具合が発生している）場合にはフェイル情報１０２Ｂを生成する。なお、図４に示されるように、フェイル情報１０２Ｂは、回路記述１０１Ａにおいて不具合が発生するまでの回路遷移状態が記録された波形情報も含む。なお、アサーションベース検証部１０２は、シミュレーション技術を用いるときには、テスト記述１０１Ｃを利用する。
【００１５】
論理生成部１０３は、アサーションベース検証部１０２によってフェイル情報１０２Ｂが生成された場合に、アサーション記述１０１Ｂからフェイル情報１０２Ｂに対応する信号を抽出し、その抽出された信号に対する回路記述１０１Ａの入出力論理１０３Ａを生成する。このとき、論理生成部１０３は、アサーション記述１０１Ｂにおいて前提条件として定義されている信号に関しては、定義されている値以外の信号値が使われている状態を削除する。また、論理生成部１０３は、フェイル情報１０２Ｂに対応する信号を抽出し、その信号に対する回路記述１０１Ａの入出力論理１０３Ａに基づいて、図５に示されるような有限状態機械（以下、「ＦＳＭ（Ｆｉｎｉｔ  Ｓｔａｔｅ  Ｍｏｄｅｌ）」という）１０３Ｂを生成する。このとき、論理生成部１０３は、中間変数を削除し、回路記述１０１Ａに対する入力信号とアサーション記述１０１Ｂに記述されている信号のみを含むＦＳＭ１０３Ｂを生成する。なお、論理生成部１０３は、アサーションベース検証部１０２によって図６に示されるようなアサーション記述１０１Ｂに対する図７に示されるようなフェイル情報１０２Ｂが生成された場合には、図８に示されるようなＦＳＭ１０３Ｂを生成する。
【００１６】
信号制約生成部１０４は、論理生成部１０３によって生成された入出力論理１０３Ａ、または、図５もしくは図８に示されるようなＦＳＭ１０３Ｂに基づいて、回路記述１０１Ａにおいて不具合が発生する状態に至る信号の組合せを抽出し、その抽出された組合せに基づいて信号制約１０４Ａを生成する。なお、信号制約生成部１０４は、図５に示されるようなＦＳＭ１０３Ｂに対応する信号制約１０４Ａとして図９に示されるような信号制約１０４Ａを生成し、図８に示されるようなＦＳＭ１０３Ｂに対応する信号制約１０４Ａとして図１０に示されるような時間遷移が表現された信号制約１０４Ａを生成する。また、信号制約生成部１０４は、入力部１０１から入力された予め作成されたＦＳＭ１０３Ｂに基づいて、信号制約１０４Ａを生成しても良い。また、信号制約部１０４は、複数のＦＳＭ１０３Ｂに対応する複数の信号制約１０４Ａを生成しても良い。
【００１７】
評価部１０５は、信号制約生成部１０４によって生成された信号制約１０４Ａの正当性を評価する。このとき、評価部１０５は、信号制約１０４Ａが適用されたときに、前提条件が成立しないアサーションベース記述１０１Ｂが存在する場合またはアサーション記述１０１Ｂに記述された任意の信号が固定値となる場合に、その信号制約１０４Ａを「不当」と評価する。たとえば、“ＳＴＡＲＴ＝＝０”という信号制約１０４Ａは、任意の信号が固定値となるような制約であるので「不当」と評価される。また、“＄ｏｎｅｈｏｔ（ＧＥＮ＿ＲＥＱ，ＡＳＰ＿ＲＥＱ，ＭＩＳＣ＿ＲＥＱ）；”という信号制約１０４Ａは、アサーション記述１０１Ｂの中に“！ＧＥＮ＿ＲＥＱ＆＆！ＡＳＰ＿ＲＥＱ＆＆！ＭＩＳＣ＿ＲＥＱ  ｜＝＞！ＧＥＮ＿ＡＣＫ＆＆！ＡＳＰ＿ＡＣＫ&&!ＭＩＳＣ_ＡＣＫ”という記述が存在するときには、“！ＧＥＮ＿ＲＥＱ＆＆！ＡＳＰ＿ＲＥＱ＆＆！ＭＩＳＣ＿ＲＥＱ”という状態が成立しないので、「不当」と評価される。
【００１８】
論理生成部１０３、信号制約生成部１０４、および評価部１０５の処理は、不具合が発生しているアサーション記述１０１Ｂ毎に行われる。評価結果が画定した後は、不具合が発生している他のアサーション記述１０１Ｂに対して同様の処理を行う。
【００１９】
アサーション記述修正部１０６は、評価部１０５によって信号制約１０４Ａが「不当」と評価された場合には、その信号制約１０４Ａに対応するアサーション記述１０１Ｂを修正し、修正アサーション記述１０６Ａを生成する。たとえば、アサーション記述修正部１０６は、信号制約１０４Ａが適用されたときに、アサーションベース記述１０１Ｂの前提条件が成立するように、または、アサーション記述１０１Ｂに記述された任意の信号が変動値となるように、「不当」と評価された信号制約１０４をアサーション記述１０１Ｂの前提条件に追加することによって、修正アサーション記述１０６Ａを生成する。なお、アサーション記述修正部１０６は、アサーション記述１０１Ｂに記述されている入力信号に対して論理生成部１０３によって生成されたＦＳＭ１０３Ｂを用いて不具合を抑制するように入力信号の時間定義の変更を行うことによって修正アサーション記述１０６Ａを生成しても良い。
【００２０】
出力部１０７は、評価部１０５によって「正当」と評価された信号制約１０４Ａが存在する場合にはその信号制約１０４Ａを検証結果１０７Ａとして出力する。また、出力部１０７は、評価部１０５によって「不当」と評価された信号制約１０４Ａが存在する場合にはアサーション記述修正部１０６によって生成された修正アサーション記述１０６Ａを検証結果１０７Ａとして出力する。また、出力部１０７は、信号制約生成部１０４が不具合を抑制するような信号制約１０４Ａを生成できない場合、または、評価部１０５によって「不当」と評価された信号制約１０４Ａが存在し、かつ、アサーション記述修正部１０６が修正アサーション記述１０６Ａを生成できない場合には、不具合が発生する回路遷移状態の中から任意に選ばれた１種類の波形を含むフェイル情報１０２Ｂを検証結果１０７Ａとして出力する。たとえば、出力部１０７は、ディスプレイなどの検証装置１００に接続される表示装置のインタフェースである。
【００２１】
本発明の実施例１によれば、アサーションベース検証において、不具合発生時に仕様で禁止されている入力信号の組み合わせによる回路の異常状態や擬似エラーを抑制するために必要な信号制約を作成するので、半導体集積回路の検証効率を向上させることができる。
【００２２】
また、本発明の実施例１によれば、信号制約１０４Ａが生成できない場合に、対象となるアサーション記述１０１Ｂに基づいて、不具合が抑制されるようにアサーション記述１０１Ｂを修正するので、試行錯誤を省略することができる。その結果、半導体集積回路の検証に要する作業時間を大幅に短縮することが出来る。
【００２３】
また、本発明の実施例１によれば、アサーション記述修正部１０６が入力信号のみを修正するので、修正アサーション記述１０６Ａが過剰に生成されることを防ぐことができる。その結果、大きな規模の半導体集積回路に対する検証効率を向上することができる。
【００２４】
また、本発明の実施例１によれば、評価部１０５が信号制約１０４Ａの正当性を評価するので、信号制約１０４Ａが過剰な制約を含むことに起因する検証抜けを防ぐことができる。その結果、半導体集積回路の検証品質を向上させることができる。
【実施例２】
【００２５】
次に、本発明の実施例２について説明する。本発明の実施例２は、信号制約生成部１０４が複数のＦＳＭ１０３Ｂから複数の信号制約１０４Ａを生成するときに行う最適化の例である。なお、本発明の実施例１と同様の内容についての説明は省略する。
【００２６】
図１１は、本発明の実施例２に係る信号制約生成部１０４の最適化処理の処理手順を示すフローチャートである。
【００２７】
はじめに、図１２（ａ）〜（ｃ）に示されるように、信号制約生成部１０４は、複数のＦＳＭ１０３Ｂから生成された複数の信号制約１０４Ａ１〜Ａ３が、複数の信号の組合せに対するものである場合には（Ｓ１１０１−ＹＥＳ）、それらの複数の信号の組合せを統合する（Ｓ１１０２）。このとき、信号制約生成部１０４は、複数の信号制約１０４Ａ１〜Ａ３が同じ信号の組合せに対するものである場合に、論理和演算を行って接合し、重複する項を削除する。その結果、図１２（ｄ）に示されるような信号制約１０４Ａ４が生成される。
【００２８】
次に、図１２（ｅ）に示されるように、信号制約生成部１０４は、現状の論理否定で発生させてはいけない信号の組合せの論理和演算とは別に、発生させる信号の組合せの論理和演算を行うことによって、Ｓ１１０２において生成された信号制約１０４Ａ４と等価の信号制約１０４Ａ５を生成する（Ｓ１１０３）。
【００２９】
次に、信号制約生成部１０４は、Ｓ１１０２において生成された信号制約１０４Ａ４とＳ１１０３において生成された信号制約１０４Ａ５の項数を比較し、項数の最も少ない組合せに対応する信号制約１０４Ａを選択する（Ｓ１１０４）。ここでは、信号制約１０４Ａ４より項数の少ない信号制約１０４Ａ５が選択される。
【００３０】
Ｓ１１０４において選択された信号制約１０４Ａ５が組込関数へ置換できる場合には（Ｓ１１０５−ＹＥＳ）、信号制約生成部１０４は、Ｓ１１０４において選択された信号制約１０４Ａ５を組込関数へ置換し（Ｓ１１０６）、この最適化処理を終了する。たとえば、信号制約生成部１０４は、「ＩＥＥＥ１８００−２００５  ＳｙｓｔｅｍＶｅｒｉｌｏｇ」の組込関数“$ｏｎｅｈｏｔ０”等に対してパターンマッチングが置換可能か否かの判定を行い、置換可能な場合に置換を行う。その結果、図１２（ｆ）に示されるような信号制約１０４Ａ６が生成される。
【００３１】
また、信号制約部１０４は、Ｓ１１０４において選択された信号制約１０４Ａ５が組込関数へ変換できない場合には（Ｓ１１０５−ＮＯ）、組込関数への変換を行うことなく、この最適化処理を終了する。
【００３２】
なお、この最適化処理は、生成された信号制約１０４Ａが複数の信号の組合せに対するものでない場合には行われない（Ｓ１１０１−ＮＯ）。
【００３３】
本発明の実施例２によれば、信号制約生成部１０４が信号制約１０４Ａの論理項を減らすように最適化処理を行うので、使用者が確認し易い形式で信号制約１０４Ａを出力することができる。
【図面の簡単な説明】
【００３４】
【図１】本発明の実施例１に係る半導体集積回路の検証装置１００の構成を示すブロック図である。
【図２】回路記述１０１Ａの一例を示す概略図である。
【図３】アサーション記述１０１Ｂの一例を示す概略図である。
【図４】フェイル情報１０２Ｂの一例を示す概略図である。
【図５】図３および図４に対応するＦＳＭ１０３Ｂの一例を示す概略図である。
【図６】アサーション記述１０１Ｂの一例を示す概略図である。
【図７】フェイル情報１０２Ｂの一例を示す概略図である。
【図８】図６および図７に対応するＦＳＭ１０３Ｂの一例を示す概略図である。
【図９】図５に対応する信号制約１０４Ａの一例を示す概略図である。
【図１０】図８に対応する信号制約１０４Ａの一例を示す概略図である。
【図１１】本発明の実施例２に係る信号制約生成部１０４の最適化処理の処理手順を示すフローチャートである。
【図１２】（ａ）ないし（ｆ）は、図１１において生成される信号制約１０４Ａの一例を示す概略図である。
【符号の説明】
【００３５】
１００  半導体集積回路の検証装置
１０１  入力部
１０２  アサーションベース検証部
１０３  論理生成部
１０４  信号制約生成部
１０５  評価部
１０６  アサーション記述修正部
１０７  出力部
【図１】
0004950942.tif 000002
【図２】
0004950942.tif 000003
【図３】
0004950942.tif 000004
【図４】
0004950942.tif 000005
【図５】
0004950942.tif 000006
【図６】
0004950942.tif 000007
【図７】
0004950942.tif 000008
【図８】
0004950942.tif 000009
【図９】
0004950942.tif 000010
【図１０】
0004950942.tif 000011
【図１１】
0004950942.tif 000012
【図１２】
0004950942.tif 000013