論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体
【課題】人手による作業を行うことなく、比較元回路と、この比較元回路に、論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を自動的に行うこと。
【解決手段】フリップフロップ間にバッファやインバータが存在する場合、全てのバッファと偶数個のインバータを削除する。比較元回路および比較対象回路について、論理的に等価なフリップフロップを削除し、他のフリップフロップにマージして一つのフリップフロップとする。マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加する。比較元回路および比較対象回路について、各フリップフロップが持つ複数の名前を全て調べ、名前が一致するフリップフロップを検証対象のペアとする。ペアを作成したフリップフロップの入力を始点とするロジックコーンについて、比較元回路と比較対象回路の比較検証を行う。
【解決手段】フリップフロップ間にバッファやインバータが存在する場合、全てのバッファと偶数個のインバータを削除する。比較元回路および比較対象回路について、論理的に等価なフリップフロップを削除し、他のフリップフロップにマージして一つのフリップフロップとする。マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加する。比較元回路および比較対象回路について、各フリップフロップが持つ複数の名前を全て調べ、名前が一致するフリップフロップを検証対象のペアとする。ペアを作成したフリップフロップの入力を始点とするロジックコーンについて、比較元回路と比較対象回路の比較検証を行う。
【発明の詳細な説明】
【技術分野】
【0001】
この発明は、二つの回路の論理が等価であるか否かを自動的に検証する論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体に関する。
【背景技術】
【0002】
集積回路の設計において、非同期の異なるクロック信号で駆動される2個のフリップフロップ間のパス(非同期パス)には、データ転送におけるメタ・ステーブル問題の対策として、タイミングを補償するためのシンクロナイザが挿入される。一般に、シンクロナイザは、1個以上のフリップフロップにより構成される。フリップフロップは、入力信号を1クロック遅らせて出力するので、非同期パスにフリップフロップが挿入されても、他の組み合わせ回路等の論理には影響がない。電源の異なるブロック間に挿入されるレベルシフタも、他の組み合わせ回路等の論理に影響を及ぼさない。
【0003】
図14は、論理等価検証を行う2個の回路を示すアルゴリズム説明図である。図14に示す例では、比較元回路1は、出力ポートを始点とし、第1の組み合わせ回路2で構成される第1のロジックコーン4に、第1のフリップフロップA(FF_A)3の入力を始点とし、第2の組み合わせ回路5で構成される第2のロジックコーン8が接続され、この第2のロジックコーン8に、さらに第2のフリップフロップB(FF_B)6の入力を始点とし、第3の組み合わせ回路9で構成される第3のロジックコーン10と第3のフリップフロップC(FF_C)7の入力を始点とする第6のロジックコーン11が接続された構成となっている。第2のフリップフロップB6と第3のフリップフロップC7を駆動するクロック信号は、クロック信号F(CLK_F)であり、第1のフリップフロップA3を駆動するクロック信号は、クロック信号G(CLK_G)である。
【0004】
図14に示す例では、比較対象回路21は、比較元回路1の第2の組み合わせ回路5と第1のフリップフロップA3を結ぶ非同期パスに、第4のフリップフロップD(FF_D)22と第5のフリップフロップE(FF_E)23が挿入されている。第4のフリップフロップD22および第5のフリップフロップE23は、クロック信号G(CLK_G)で駆動される。比較対象回路21では、第1のロジックコーン4に、第1のフリップフロップA3の入力を始点とする第4のロジックコーン24が接続され、この第4のロジックコーン24に、第4のフリップフロップD22の入力を始点とする第5のロジックコーン25が接続され、この第5のロジックコーン25に第2のロジックコーン8が接続された構成となる。このとき、第2のロジックコーン8の始点は、第5のフリップフロップE23となる。
【0005】
また、第4のフリップフロップD22と第5のフリップフロップE23の間に、インバータ26,27やバッファ28,29,30が挿入されることもある。論理等価検証では、比較対象回路21と比較元回路1で名前の一致するものをペアとして、ロジックコーン同士の検証が行われる。そして、すべてのロジックコーンが論理的に一致すれば、比較対象回路21と比較元回路1が論理等価であると判断される。ここで、ロジックコーンは、一般に論理等価検証を行う単位ブロックであり、出力ポート、フリップフロップの入力またはブラックボックスモジュールの入力ピンを始点とし、入力ポート、フリップフロップからの出力またはブラックボックスモジュールの出力ポートを終点とするブロックである。
【0006】
論理等価検証の対象となる二つの論理のうちの一方に他方に無い追加論理が存在する場合の論理回路の論理等価検証方法が公知である。この方法は、追加論理の情報を用いて、追加論理を除いた元論理と元々追加論理を含まない論理との等価性を検証することを特徴とする(例えば、特許文献1参照。)。
【0007】
【特許文献1】特開2001−67379号公報
【発明の開示】
【発明が解決しようとする課題】
【0008】
しかしながら、従来の論理等価検証方法では、同じ名前のものをペアとして、ロジックコーン同士を比較するため、図14において、比較元回路1と比較対象回路21は、論理的に一致するにもかかわらず、それぞれ第1のフリップフロップA3の入力を始点とする第2のロジックコーン8と第4のロジックコーン24との比較で不一致となってしまう。この場合には、設計者が、不一致としてエラー検出された箇所を一つずつ確認したり、比較対象回路21の第5のフリップフロップE23と比較元回路1の第1のフリップフロップA3がペアであることを指示ファイルに記述する必要がある。このような人手による作業には、手間や時間がかかるという不都合や、間違いを犯すおそれがあるという問題点がある。また、前記特許文献1に開示された方法では、追加論理の情報を用いて、追加論理を除くための手間がかかるという問題点がある。
【0009】
この発明は、上述した従来技術による問題点を解消するため、人手による作業を行うことなく、比較元回路と、この比較元回路に、論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を自動的に行うことができる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体を提供することを目的とする。
【課題を解決するための手段】
【0010】
上述した課題を解決し、目的を達成するため、本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体は、以下の特徴を有する。マージ処理によって削除される複数のフリップフロップ間にバッファやインバータが存在する場合、全てのバッファと偶数個のインバータを削除する(論理圧縮工程)。そして、比較元回路について、論理的に等価なフリップフロップを、その挿入箇所から削除して他のフリップフロップにマージ(統合)して一つのフリップフロップとする。比較対象回路についても同様にする(フリップフロップマージ工程)。その際、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加する。その後、マージ処理の済んだ比較元回路および比較対象回路について、フリップフロップの対応付けを行う(マッチング工程)。これには名前が一致するか否かを調べるネームマッチング工程を含む。名前が一致しなければ、別の手段による対応付け処理を行うが、この発明ではこの部分については言及しない。対応付けされたペアに対して、比較元回路と比較対象回路の比較検証を行い(比較検証工程)、レポートを出力する。なお、本明細書において、論理的に等価であるとは、論理的に影響のないことを意味している。従って、論理的に等価なフリップフロップとは、入力と同じ論理を出力するフリップフロップという意味である。
【0011】
この発明によれば、論理的に等価なフリップフロップがその挿入箇所から削除されて他のフリップフロップにマージされる。また、このマージ処理によって削除されるフリップフロップの名前がマージ処理後に残るフリップフロップの名前に追加される。従って、比較元回路と、シンクロナイザやレベルシフタなどのように論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を行う際に、論理的に等価なフリップフロップの挿入が原因で両回路の論理が不一致であるという結果が出るのを防ぐことができる。
【発明の効果】
【0012】
本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体によれば、人手による作業を行うことなく、比較元回路と、この比較元回路に、論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を自動的に行うことができるという効果を奏する。
【発明を実施するための最良の形態】
【0013】
以下に添付図面を参照して、この発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体の好適な実施の形態を詳細に説明する。
【0014】
(論理等価検証装置のハードウェア構成)
まず、この発明の実施の形態にかかる論理等価検証装置のハードウェア構成について説明する。図1は、この発明の実施の形態にかかる論理等価検証装置のハードウェア構成を示すブロック図である。
【0015】
図1において、論理等価検証装置は、CPU101と、ROM102と、RAM103と、HDD(ハードディスクドライブ)104と、HD(ハードディスク)105と、FDD(フレキシブルディスクドライブ)106と、着脱可能な記録媒体の一例としてのFD(フレキシブルディスク)107と、ディスプレイ108と、I/F(インターフェース)109と、キーボード110と、マウス111と、スキャナ112と、プリンタ113と、を備えている。また、各構成部は、バス100によってそれぞれ接続されている。
【0016】
ここで、CPU101は、論理等価検証装置の全体の制御を司る。ROM102は、ブートプログラムなどのプログラムを記憶している。RAM103は、CPU101のワークエリアとして使用される。HDD104は、CPU101の制御に従ってHD105に対するデータのリード/ライトを制御する。HD105は、HDD104の制御で書き込まれたデータを記憶する。
【0017】
FDD106は、CPU101の制御に従ってFD107に対するデータのリード/ライトを制御する。FD107は、FDD106の制御で書き込まれたデータを記憶したり、FD107に記憶されたデータを論理等価検証装置に読み取らせたりする。
【0018】
また、着脱可能な記録媒体として、FD107のほか、CD−ROM(CD−R、CD−RW)、MO、DVD(Digital Versatile Disk)、メモリーカードなどであってもよい。ディスプレイ108は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ108は、例えば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【0019】
I/F109は、通信回線を通じてインターネットなどのネットワーク114に接続され、このネットワーク114を介して他の装置に接続される。そして、I/F109は、ネットワーク114と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F109には、例えばモデムやLANアダプタなどを採用することができる。
【0020】
キーボード110は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス111は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【0021】
スキャナ112は、画像を光学的に読み取り、論理等価検証装置内に画像データを取り込む。なお、スキャナ112は、OCR機能を持たせてもよい。また、プリンタ113は、画像データや文書データを印刷する。プリンタ113には、例えば、レーザプリンタやインクジェットプリンタを採用することができる。
【0022】
(論理等価検証装置の機能的構成)
次に、この発明の実施の形態にかかる論理等価検証装置の機能的構成について説明する。図2は、この発明の実施の形態にかかる論理等価検証装置の機能的構成を示すブロック図である。図2に示すように、論理等価検証装置41は、デザイン読み込み部42、論理圧縮部43、フリップフロップマージ部44、マッチング部45、比較検証部46およびレポート出力部47を備えている。
【0023】
デザイン読み込み部42は、RTL、ネットリスト等の比較元回路データ48およびRTL、ネットリスト等の比較対象回路データ49を読み込む。比較元回路または比較対象回路には、後述するマージ処理によって削除されるフリップフロップ間にバッファやインバータが存在することがある。バッファは、入力と出力の論理が同じであるので、削除されても、論理的な影響はない。また、インバータは、入力と出力の論理が反転するので、偶数個ずつ削除されても、論理的な影響はない。
【0024】
そこで、論理を圧縮するため、論理圧縮部43は、これらのバッファやインバータを削除する。バッファについては、全てを削除してよいが、インバータについては偶数個ずつ削除する。例えば、図14に示す比較対象回路21の例では、論理圧縮部43は、第4のフリップフロップD22と第5のフリップフロップE23の間に存在する全てのバッファ28,29,30と偶数個(2個)のインバータ26,27を削除する。論理圧縮部43は、比較元回路と比較対象回路の両方に対して論理圧縮処理を行う。
【0025】
フリップフロップマージ部44は、論理圧縮部43により論理が圧縮された回路データに基づいて、シンクロナイザやレベルシフタなどの論理的に等価なフリップフロップを、その挿入箇所から削除して前段のフリップフロップにマージ、すなわち統合して一つのフリップフロップとする。その際、フリップフロップマージ部44は、マージのために削除するフリップフロップのレジスタ名を、マージ処理後に残るフリップフロップの名前に追加し、それによって、削除されるフリップフロップのレジスタ名も保持する。
【0026】
例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22と第5のフリップフロップE23は、他の回路の論理に影響を及ぼさないので、フリップフロップマージ部44は、マージ処理によって、この二つのフリップフロップD22,E23を削除し、第1のフリップフロップA3にマージする。そして、フリップフロップマージ部44は、第1のフリップフロップA3のレジスタ名を、FF_A、FF_DおよびFF_Eとする。フリップフロップマージ部44は、比較元回路と比較対象回路の両方に対してマージ処理を行う。フリップフロップマージ部44は、次の(1)〜(4)の条件を満足するときに、マージ処理を行う。
【0027】
(1)マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されていること。ここで、フリップフロップマージ部44は、二つのフリップフロップを駆動するクロック信号について、クロック名が同じである場合、外部より与えたクロックドメイングループが同じである場合、またはクロック信号のバックトレースにより同一クロックドメインと判断される場合に、二つのフリップフロップが同じクロック信号で駆動されていると判断する。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、第1のフリップフロップA3と同じクロック信号G(CLK_G)で駆動されているので、上記(1)の条件を満たす。
【0028】
(2)マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップであること。フリップフロップに複数の入力がある場合、または複数の出力がある場合には、このフリップフロップがマージによって他のフリップフロップに統合されてしまうと、このフリップフロップへ信号を出力する回路の出力先がなくなったり、このフリップフロップから信号を入力する回路に信号が入力されなくなるという不具合が生じる。そのため、マージ処理を行うことができない。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、データラインが1入力1出力タイプのフリップフロップであるので、この(2)の条件を満たす。
【0029】
(3)マージ処理によって削除される複数のフリップフロップ間に論理回路が存在しないこと。(4)マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプであること。フリップフロップには、入力ピンがデータ(DATA)ピンとクロック(CLK)ピンだけである単純なタイプのものや、それらの入力ピン以外に、セット(SET)ピン、もしくはリセット(RESET)ピンを有する単純でないタイプのものや、セット(SET)ピンとリセット(RESET)ピンの両方を有する単純でないタイプのものなどがある。入力ピンの種類が同じフリップフロップ同士であれば、マージ処理を行うことができる。
【0030】
ただし、入力ピンの種類が同じでなくても、前記単純なタイプのフリップフロップは、いずれのタイプのフリップフロップともマージすることができる。この場合、前記単純なタイプのフリップフロップが削除され、単純でないタイプのフリップフロップが残る。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、第1のフリップフロップA3と同じ単純なタイプのフリップフロップであるので、この(4)の条件を満たす。
【0031】
マッチング部45は、フリップフロップマージ部44によりそれぞれマージ処理がなされた比較元回路および比較対象回路の各データに基づいて、比較元回路と比較対象回路のフリップフロップを対応付ける。この時、双方の回路のフリップフロップの名前が一致するか否かを調べる。マッチング部45は、フリップフロップの名前が一致しなければ、別の手段による対応付けを行っても良いが、この発明では言及しない。比較検証部46は、マッチング部45により対応づけられたフリップフロップの入力を始点とするロジックコーンについて、比較元回路と比較対象回路の比較検証を行う。レポート出力部47は、比較検証部46による比較検証結果のレポート50を出力する。
【0032】
なお、上述したデザイン読み込み部42、論理圧縮部43、フリップフロップマージ部44、マッチング部45、比較検証部46およびレポート出力部47は、具体的には、例えば、図1に示したROM102、RAM103、HD105などの記録媒体に記録されたプログラムを、CPU101が実行することによって、またはI/F109によって、その機能を実現する。
【0033】
(論理等価検証処理手順)
次に、この発明の実施の形態にかかる論理等価検証装置の処理手順について説明する。図3は、この発明の実施の形態にかかる論理等価検証装置の処理手順を示すフローチャートである。図3に示すように、論理等価検証処理が開始されると、まず、デザイン読み込み部42により、比較元回路データ48と比較対象回路データ49が読み込まれる(ステップS1)。例えば、比較対象回路データ49は、比較元回路のメタ・ステーブル問題の対策として、比較元回路にフリップフロップを挿入した回路のデータである。
【0034】
次いで、論理圧縮部43により、比較元回路および比較対象回路のそれぞれについて、バッファやインバータを削除する論理圧縮処理が行われる(ステップS2)。論理圧縮処理の詳細については、後述する。次いで、フリップフロップマージ部44により、比較元回路および比較対象回路のそれぞれについて、フリップフロップのマージ処理が行われる(ステップS3)。このマージ処理の詳細については、後述する。
【0035】
次いで、マッチング部45により、比較元回路と比較対象回路で対応するロジックコーンの対応付けを行う。この発明ではフリップフロップの名前が一致するか否かを調べるネームマッチング処理を行う(ステップS4)。ネームマッチング処理の詳細については、後述する。次いで、比較検証部46により、比較元回路と比較対象回路の論理が一致するか否かを調べる比較検証処理が行われる(ステップS5)。そして、レポート出力部47により比較検証結果のレポートが出力され、(ステップS6)図3に示す一連の論理等価検証処理が終了する。
【0036】
(論理圧縮処理手順)
図4は、論理圧縮処理手順を示すフローチャートである。図4に示すように、論理圧縮処理が開始されると、まず、注目したフリップフロップのデータピンに接続する前段の論理プリミティブ検索を行う(ステップS11)。検索の結果、前段の回路がバッファであるか否かを判断する(ステップS12)。バッファである場合(ステップS12:Yes)、そのバッファをバッファ削除リストにスタックし、スタックしたバッファの前段の論理プリミティブ検索を行い(ステップS13)、ステップS12に戻る。
【0037】
ステップS12で、バッファでない場合(ステップS12:No)、検索により得た前段回路がインバータであるか否かを判断する(ステップS14)。インバータである場合(ステップS14:Yes)、インバータカウンタをインクリメントし、そのインバータをインバータ削除リストにスタックする。そして、スタックしたインバータの前段のセル検索を行い(ステップS15)、ステップS12に戻る。ステップS14で、インバータでない場合(ステップS14:No)、検索により得た前段回路がフリップフロップであるか否かを判断する(ステップS16)。
【0038】
フリップフロップでない場合(ステップS16:No)、インバータカウンタのリセット、インバータ削除リストの削除およびバッファ削除リストの削除を行う(ステップS17)。そして、ステップS11に戻る。ステップS16で、フリップフロップである場合(ステップS16:Yes)、インバータ削除リストにスタックされているインバータ群から[スタックされている個数/2]のあまりを除いた残りのインバータを削除し、バッファ削除リストにスタックされているバッファ群を削除する(ステップS18)。そして、ステップS17へ進む。以上のステップS11〜ステップS18の一連の処理を、回路全体について行い、図4に示す一連の論理圧縮処理が終了する。
【0039】
図5は、論理圧縮処理後の回路を示すアルゴリズム説明図である。例えば、図14に示す比較対象回路21に対して論理圧縮処理を行った結果、図5に示すように、第4のフリップフロップD22と第5のフリップフロップE23の間のバッファ(28,29,30)および偶数個のインバータ(26,27)が削除される。
【0040】
(フリップフロップのマージ処理手順)
図6は、フリップフロップのマージ処理手順を示すフローチャートである。ここでは、説明の便宜上、二つのフリップフロップのうち、一方を比較元フリップフロップとし、他方を処理対象フリップフロップとする。図6に示すように、フリップフロップのマージ処理が開始されると、まず、注目した回路がフリップフロップであるか否かを判断する(ステップS21)。フリップフロップである場合(ステップS21:Yes)、これを比較元フリップフロップとし、比較元フリップフロップのデータパスピンの前段の論理プリミティブ検索を行う(ステップS22)。検索により得た前段回路がフリップフロップであるか否かを判断する(ステップS23)。
【0041】
フリップフロップである場合(ステップS23:Yes)、これを処理対象フリップフロップとし、処理対象フリップフロップのクロックが比較元フリップフロップのクロックと同じであるか否かを判断する(ステップS24)。クロックが同じである場合(ステップS24:Yes)、さらに、処理対象フリップフロップのデータラインのファンイン数およびファンアウト数が1であるか否かを判断する(ステップS25)。データラインのファンイン数およびファンアウト数が1である場合(ステップS25:Yes)、ステップS26へ進む。データラインのファンイン数が2以上、もしくはファンアウト数が2以上である場合(ステップS25:No)、また、ステップS21、またはステップS23でNoである場合、ステップS21に戻る。そして、別の回路に注目し、ステップS21〜ステップS25を行う。
【0042】
ステップS26では、処理対象フリップフロップが単純なタイプのものであるか否かを判断する。単純なタイプのフリップフロップについては、先に説明した通りである。単純なタイプである場合(ステップS26:Yes)、比較元フリップフロップが削除リストに登録されているか否かを判断する(ステップS27)。登録されている場合(ステップS27:Yes)、処理対象フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、比較元フリップフロップのマージ先と同じである。そして、比較元フリップフロップのマージ先フリップフロップの名前に処理中のフリップフロップの名前を全て追加する(ステップS28)。
【0043】
ステップS27で、登録されていない場合(ステップS27:No)、処理対象フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、比較元フリップフロップである。そして、比較元フリップフロップの名前に処理中のフリップフロップの名前を全て追加する(ステップS29)。一方、ステップS26で、単純なタイプでない場合(ステップS26:No)、処理対象フリップフロップが比較元フリップフロップと同じタイプであるか否かを判断する(ステップS30)。同じタイプである場合(ステップS30:Yes)、ステップS27へ進む。
【0044】
同じタイプでない場合(ステップS30:No)、さらに、比較元フリップフロップが単純なタイプであるか否かを判断する(ステップS31)。単純なタイプでない場合(ステップS31:No)、ステップS21に戻り、別の回路に注目し、ステップS21以降の処理を行う。単純なタイプである場合(ステップS31:Yes)、処理対象フリップフロップが削除リストに登録されているか否かを判断する(ステップS32)。登録されている場合(ステップS32:Yes)、比較元フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、処理対象フリップフロップのマージ先と同じである。そして、処理対象フリップフロップのマージ先フリップフロップの名前に比較元フリップフロップの名前を全て追加する(ステップS33)。
【0045】
ステップS32で、登録されていない場合(ステップS32:No)、比較元フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、処理対象フリップフロップである。そして、処理対象フリップフロップの名前に比較元フリップフロップの名前を全て追加する(ステップS34)。以上のステップS21〜ステップS34の一連の処理を、回路全体について行う。その後、削除リストに登録されているフリップフロップ全体について、フリップフロップの削除を行い(ステップS35)、図6に示す一連のマージ処理が終了する。
【0046】
図7は、フリップフロップのマージ処理後の回路を示すアルゴリズム説明図である。例えば、図14に示す比較対象回路21に対してフリップフロップのマージ処理を行った結果、図7に示すように、第1のフリップフロップA3と第4のフリップフロップDと第5のフリップフロップEがマージされて、一つのフリップフロップになっている。図示例では、マージ先フリップフロップは、第1のフリップフロップA3であり、この第1のフリップフロップA3は、レジスタ名としてFF_A、FF_DおよびFF_Eを有する。従って、図7に示す比較対象回路21と、図14に示す比較対象回路21で、論理が一致することになる。
【0047】
ここで、フリップフロップのマージパターンおよび削除リストの一例について説明する。図8〜図10は、フリップフロップのマージパターンを示す模式図である。図8に示すパターンは、フリップフロップJ(FF_J)61とフリップフロップK(FF_K)62がともにフリップフロップL(FF_L)63をマージ先としてマージされるパターンである。
【0048】
図9に示すパターンは、フリップフロップM(FF_M)64がフリップフロップN(FF_N)65をマージ先としてマージされ、さらに、そのフリップフロップN(FF_N)65がフリップフロップP(FF_P)66をマージ先としてマージされるパターンである。図10に示すパターンは、フリップフロップQ(FF_Q)67とフリップフロップT(FF_T)69がその間のフリップフロップR(FF_R)68をマージ先としてマージされるパターンである。図11は、削除リストの一例を示す模式図である。図8〜図10に示すフリップフロップのマージが起こると、削除リストは、図11に示すようになる。
【0049】
(マッチング処理手順)
図12は、マッチング処理手順を示すフローチャートである。ここでは、説明の便宜上、比較元回路のフリップフロップを比較元フリップフロップとし、比較対象回路のフリップフロップを処理対象フリップフロップとする。図12に示すように、マッチング処理が開始されると、まず、比較元フリップフロップの全てについて、名前の一致するフリップフロップを処理対象からさがすネームマッチング処理を行う(ステップS41)。
【0050】
そして、名前が一致するフリップフロップ同士をペアとして対応づける。一方、ネームマッチング処理において名前の一致するフリップフロップがなかった比較元フリップフロップには、エラーフラグがつく。ネームマッチング処理の詳細な手順については後述する。全ての比較元フリップフロップについてネームマッチング処理が終了したら、エラーフラグのついた比較元フリップフロップについて、さらに別の手法で対応づけを行う(ステップS42)。例えば、機能的に一致するフリップフロップ同士を対応づけるファンクションマッチング処理を行う。
【0051】
(ネームマッチング処理手順)
図13は、ネームマッチング処理手順のうち、比較元回路のフリップフロップを1つ選択し、それに対応するフリップフロップを比較対象回路から見つける処理を示すフローチャートである。ここでは、説明の便宜上、比較元回路から選択したフリップフロップを比較元フリップフロップとし、比較対象回路のフリップフロップを処理対象フリップフロップとする。図13に示すように、マッチング処理が開始されると、まず、比較元フリップフロップと処理対象フリップフロップで名前が一致するか否かを判断する(ステップS51)。一致しない場合(ステップS51:No)、処理対象フリップフロップに複数の名前があるか否かを判断する(ステップS52)。
【0052】
名前が一つである場合(ステップS52:No)、ステップS55へ進む。複数の名前がある場合(ステップS52:Yes)、処理対象フリップフロップの全ての名前と比較元フリップフロップの名前を比較する(ステップS53)。そして、処理対象フリップフロップのいずれかの名前と比較元フリップフロップの名前が一致するか否かを判断する(ステップS54)。一致しない場合(ステップS54:No)、ステップS55へ進む。ステップS55では、比較元フリップフロップに複数の名前があるか否かを判断する。
【0053】
名前が一つである場合(ステップS55:No)、比較元フリップフロップにエラーフラグを立てて(ステップS56)、ステップS51に戻る。複数の名前がある場合(ステップS55:Yes)、比較元フリップフロップの全ての名前と処理対象フリップフロップの名前を比較する(ステップS57)。そして、比較元フリップフロップのいずれかの名前と処理対象フリップフロップの名前が一致するか否かを判断する(ステップS58)。
【0054】
一致しない場合(ステップS58:No)、ステップS56へ進む。一致する場合(ステップS58:Yes)、また、ステップS51またはステップS54でYesの場合、処理中の処理対象フリップフロップと比較元フリップフロップのマッチング処理を終了する。以上のステップS51〜ステップS58の一連の処理を、比較対象の全フリップフロップについて行い、比較元フリップフロップと同じ名前のフリップフロップを見つける。同じ名前のフリップフロップが見つかった場合はペアとなり(ステップS59)、それらのフリップフロップの入力を始点とするロジックコーンが論理等価検証の対象となる。これを比較元の全フリップフロップについて行う。
【0055】
このネームマッチング処理において、図14に示す比較元回路1の第1のフリップフロップA3は、レジスタ名としてFF_Aを有し、図7に示す比較対象回路21の第1のフリップフロップA3は、レジスタ名にFF_Aを含むので、比較元回路1と比較対象回路21で第1のフリップフロップA3の名前が一致することになる。従って、図14に示す比較元回路1と図14に示す比較対象回路21の比較検証を行うと、いずれの回路でも第2のロジックコーン8が、レジスタ名がFF_Aである第1のフリップフロップA3の入力を始点とすることになるので、名前によるペアが自動で作成され、両回路の論理が一致するという検証結果が得られる。
【0056】
以上説明したように、実施の形態によれば、比較元回路1と、シンクロナイザなどのように論理的に等価なフリップフロップが挿入された比較対象回路21との論理等価検証を行う際に、論理的に等価なフリップフロップの挿入が原因で両回路の論理が不一致であるという結果が出るのを防ぐことができる。従って、従来のような人手による作業を行うことなく、論理的に等価なフリップフロップが挿入された回路について論理等価検証を自動的に行うことができるという効果を奏する。また、論理的に等価なフリップフロップをレベルシフタとして挿入した回路についても、本実施の形態を適用することによって、検証ポイントを削減することができるので、検証に要する時間を削減することができる。
【0057】
なお、本実施の形態で説明した論理等価検証プログラムは、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、CD−ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な伝送媒体であってもよい。以上において本発明は、上述した実施の形態に限らず、種々変更可能である。
【0058】
(付記1)比較元回路と比較対象回路との論理等価検証を行う論理等価検証装置において、比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ手段と、それぞれ、前記フリップフロップマージ手段で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング手段と、を備えることを特徴とする論理等価検証装置。
【0059】
(付記2)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする付記1に記載の論理等価検証装置。
【0060】
(付記3)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする付記1に記載の論理等価検証装置。
【0061】
(付記4)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする付記3に記載の論理等価検証装置。
【0062】
(付記5)前記フリップフロップマージ手段は、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする付記3または4に記載の論理等価検証装置。
【0063】
(付記6)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする付記3に記載の論理等価検証装置。
【0064】
(付記7)前記フリップフロップマージ手段によるマージ処理を行う前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮手段、をさらに備えることを特徴とする付記1に記載の論理等価検証装置。
【0065】
(付記8)比較元回路と比較対象回路との論理等価検証を行う論理等価検証方法において、比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ工程と、それぞれ、前記フリップフロップマージ工程で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング工程と、を含むことを特徴とする論理等価検証方法。
【0066】
(付記9)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする付記8に記載の論理等価検証方法。
【0067】
(付記10)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする付記8に記載の論理等価検証方法。
【0068】
(付記11)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする付記10に記載の論理等価検証方法。
【0069】
(付記12)前記フリップフロップマージ工程では、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする付記10または11に記載の論理等価検証方法。
【0070】
(付記13)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする付記10に記載の論理等価検証方法。
【0071】
(付記14)前記フリップフロップマージ工程の前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮工程、をさらに含むことを特徴とする付記8に記載の論理等価検証方法。
【0072】
(付記15)付記8〜14のいずれか一つに記載の論理等価検証方法をコンピュータに実行させることを特徴とする論理等価検証プログラム。
【0073】
(付記16)付記15に記載の論理等価検証プログラムを記録したことを特徴とするコンピュータに読み取り可能な記録媒体。
【産業上の利用可能性】
【0074】
以上のように、本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体は、論理回路の設計に有用であり、特に、半導体集積回路の設計に適している。
【図面の簡単な説明】
【0075】
【図1】この発明の実施の形態にかかる論理等価検証装置のハードウェア構成を示すブロック図である。
【図2】この発明の実施の形態にかかる論理等価検証装置の機能的構成を示すブロック図である。
【図3】この発明の実施の形態にかかる論理等価検証装置の処理手順を示すフローチャートである。
【図4】この発明の実施の形態にかかる論理圧縮処理手順を示すフローチャートである。
【図5】論理圧縮処理後の回路を示すアルゴリズム説明図である。
【図6】この発明の実施の形態にかかるフリップフロップのマージ処理手順を示すフローチャートである。
【図7】フリップフロップのマージ処理後の回路を示すアルゴリズム説明図である。
【図8】フリップフロップのマージパターンの第1の例を示す模式図である。
【図9】フリップフロップのマージパターンの第2の例を示す模式図である。
【図10】フリップフロップのマージパターンの第3の例を示す模式図である。
【図11】削除リストの一例を示す模式図である。
【図12】この発明の実施の形態にかかるマッチング処理手順を示すフローチャートである。
【図13】この発明の実施の形態にかかるネームマッチング処理手順を示すフローチャートである。
【図14】論理等価検証を行う比較元回路と比較対象回路を示すアルゴリズム説明図である。
【符号の説明】
【0076】
1 比較元回路
3,22,23,61〜69 フリップフロップ
21 比較対象回路
26,27 インバータ
28,29,30 バッファ
41 論理等価検証装置
43 論理圧縮部
44 フリップフロップマージ部
45 マッチング部
48 比較元回路データ
49 比較対象回路データ
【技術分野】
【0001】
この発明は、二つの回路の論理が等価であるか否かを自動的に検証する論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体に関する。
【背景技術】
【0002】
集積回路の設計において、非同期の異なるクロック信号で駆動される2個のフリップフロップ間のパス(非同期パス)には、データ転送におけるメタ・ステーブル問題の対策として、タイミングを補償するためのシンクロナイザが挿入される。一般に、シンクロナイザは、1個以上のフリップフロップにより構成される。フリップフロップは、入力信号を1クロック遅らせて出力するので、非同期パスにフリップフロップが挿入されても、他の組み合わせ回路等の論理には影響がない。電源の異なるブロック間に挿入されるレベルシフタも、他の組み合わせ回路等の論理に影響を及ぼさない。
【0003】
図14は、論理等価検証を行う2個の回路を示すアルゴリズム説明図である。図14に示す例では、比較元回路1は、出力ポートを始点とし、第1の組み合わせ回路2で構成される第1のロジックコーン4に、第1のフリップフロップA(FF_A)3の入力を始点とし、第2の組み合わせ回路5で構成される第2のロジックコーン8が接続され、この第2のロジックコーン8に、さらに第2のフリップフロップB(FF_B)6の入力を始点とし、第3の組み合わせ回路9で構成される第3のロジックコーン10と第3のフリップフロップC(FF_C)7の入力を始点とする第6のロジックコーン11が接続された構成となっている。第2のフリップフロップB6と第3のフリップフロップC7を駆動するクロック信号は、クロック信号F(CLK_F)であり、第1のフリップフロップA3を駆動するクロック信号は、クロック信号G(CLK_G)である。
【0004】
図14に示す例では、比較対象回路21は、比較元回路1の第2の組み合わせ回路5と第1のフリップフロップA3を結ぶ非同期パスに、第4のフリップフロップD(FF_D)22と第5のフリップフロップE(FF_E)23が挿入されている。第4のフリップフロップD22および第5のフリップフロップE23は、クロック信号G(CLK_G)で駆動される。比較対象回路21では、第1のロジックコーン4に、第1のフリップフロップA3の入力を始点とする第4のロジックコーン24が接続され、この第4のロジックコーン24に、第4のフリップフロップD22の入力を始点とする第5のロジックコーン25が接続され、この第5のロジックコーン25に第2のロジックコーン8が接続された構成となる。このとき、第2のロジックコーン8の始点は、第5のフリップフロップE23となる。
【0005】
また、第4のフリップフロップD22と第5のフリップフロップE23の間に、インバータ26,27やバッファ28,29,30が挿入されることもある。論理等価検証では、比較対象回路21と比較元回路1で名前の一致するものをペアとして、ロジックコーン同士の検証が行われる。そして、すべてのロジックコーンが論理的に一致すれば、比較対象回路21と比較元回路1が論理等価であると判断される。ここで、ロジックコーンは、一般に論理等価検証を行う単位ブロックであり、出力ポート、フリップフロップの入力またはブラックボックスモジュールの入力ピンを始点とし、入力ポート、フリップフロップからの出力またはブラックボックスモジュールの出力ポートを終点とするブロックである。
【0006】
論理等価検証の対象となる二つの論理のうちの一方に他方に無い追加論理が存在する場合の論理回路の論理等価検証方法が公知である。この方法は、追加論理の情報を用いて、追加論理を除いた元論理と元々追加論理を含まない論理との等価性を検証することを特徴とする(例えば、特許文献1参照。)。
【0007】
【特許文献1】特開2001−67379号公報
【発明の開示】
【発明が解決しようとする課題】
【0008】
しかしながら、従来の論理等価検証方法では、同じ名前のものをペアとして、ロジックコーン同士を比較するため、図14において、比較元回路1と比較対象回路21は、論理的に一致するにもかかわらず、それぞれ第1のフリップフロップA3の入力を始点とする第2のロジックコーン8と第4のロジックコーン24との比較で不一致となってしまう。この場合には、設計者が、不一致としてエラー検出された箇所を一つずつ確認したり、比較対象回路21の第5のフリップフロップE23と比較元回路1の第1のフリップフロップA3がペアであることを指示ファイルに記述する必要がある。このような人手による作業には、手間や時間がかかるという不都合や、間違いを犯すおそれがあるという問題点がある。また、前記特許文献1に開示された方法では、追加論理の情報を用いて、追加論理を除くための手間がかかるという問題点がある。
【0009】
この発明は、上述した従来技術による問題点を解消するため、人手による作業を行うことなく、比較元回路と、この比較元回路に、論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を自動的に行うことができる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体を提供することを目的とする。
【課題を解決するための手段】
【0010】
上述した課題を解決し、目的を達成するため、本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体は、以下の特徴を有する。マージ処理によって削除される複数のフリップフロップ間にバッファやインバータが存在する場合、全てのバッファと偶数個のインバータを削除する(論理圧縮工程)。そして、比較元回路について、論理的に等価なフリップフロップを、その挿入箇所から削除して他のフリップフロップにマージ(統合)して一つのフリップフロップとする。比較対象回路についても同様にする(フリップフロップマージ工程)。その際、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加する。その後、マージ処理の済んだ比較元回路および比較対象回路について、フリップフロップの対応付けを行う(マッチング工程)。これには名前が一致するか否かを調べるネームマッチング工程を含む。名前が一致しなければ、別の手段による対応付け処理を行うが、この発明ではこの部分については言及しない。対応付けされたペアに対して、比較元回路と比較対象回路の比較検証を行い(比較検証工程)、レポートを出力する。なお、本明細書において、論理的に等価であるとは、論理的に影響のないことを意味している。従って、論理的に等価なフリップフロップとは、入力と同じ論理を出力するフリップフロップという意味である。
【0011】
この発明によれば、論理的に等価なフリップフロップがその挿入箇所から削除されて他のフリップフロップにマージされる。また、このマージ処理によって削除されるフリップフロップの名前がマージ処理後に残るフリップフロップの名前に追加される。従って、比較元回路と、シンクロナイザやレベルシフタなどのように論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を行う際に、論理的に等価なフリップフロップの挿入が原因で両回路の論理が不一致であるという結果が出るのを防ぐことができる。
【発明の効果】
【0012】
本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体によれば、人手による作業を行うことなく、比較元回路と、この比較元回路に、論理的に等価なフリップフロップが挿入された比較対象回路との論理等価検証を自動的に行うことができるという効果を奏する。
【発明を実施するための最良の形態】
【0013】
以下に添付図面を参照して、この発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体の好適な実施の形態を詳細に説明する。
【0014】
(論理等価検証装置のハードウェア構成)
まず、この発明の実施の形態にかかる論理等価検証装置のハードウェア構成について説明する。図1は、この発明の実施の形態にかかる論理等価検証装置のハードウェア構成を示すブロック図である。
【0015】
図1において、論理等価検証装置は、CPU101と、ROM102と、RAM103と、HDD(ハードディスクドライブ)104と、HD(ハードディスク)105と、FDD(フレキシブルディスクドライブ)106と、着脱可能な記録媒体の一例としてのFD(フレキシブルディスク)107と、ディスプレイ108と、I/F(インターフェース)109と、キーボード110と、マウス111と、スキャナ112と、プリンタ113と、を備えている。また、各構成部は、バス100によってそれぞれ接続されている。
【0016】
ここで、CPU101は、論理等価検証装置の全体の制御を司る。ROM102は、ブートプログラムなどのプログラムを記憶している。RAM103は、CPU101のワークエリアとして使用される。HDD104は、CPU101の制御に従ってHD105に対するデータのリード/ライトを制御する。HD105は、HDD104の制御で書き込まれたデータを記憶する。
【0017】
FDD106は、CPU101の制御に従ってFD107に対するデータのリード/ライトを制御する。FD107は、FDD106の制御で書き込まれたデータを記憶したり、FD107に記憶されたデータを論理等価検証装置に読み取らせたりする。
【0018】
また、着脱可能な記録媒体として、FD107のほか、CD−ROM(CD−R、CD−RW)、MO、DVD(Digital Versatile Disk)、メモリーカードなどであってもよい。ディスプレイ108は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ108は、例えば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【0019】
I/F109は、通信回線を通じてインターネットなどのネットワーク114に接続され、このネットワーク114を介して他の装置に接続される。そして、I/F109は、ネットワーク114と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F109には、例えばモデムやLANアダプタなどを採用することができる。
【0020】
キーボード110は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス111は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【0021】
スキャナ112は、画像を光学的に読み取り、論理等価検証装置内に画像データを取り込む。なお、スキャナ112は、OCR機能を持たせてもよい。また、プリンタ113は、画像データや文書データを印刷する。プリンタ113には、例えば、レーザプリンタやインクジェットプリンタを採用することができる。
【0022】
(論理等価検証装置の機能的構成)
次に、この発明の実施の形態にかかる論理等価検証装置の機能的構成について説明する。図2は、この発明の実施の形態にかかる論理等価検証装置の機能的構成を示すブロック図である。図2に示すように、論理等価検証装置41は、デザイン読み込み部42、論理圧縮部43、フリップフロップマージ部44、マッチング部45、比較検証部46およびレポート出力部47を備えている。
【0023】
デザイン読み込み部42は、RTL、ネットリスト等の比較元回路データ48およびRTL、ネットリスト等の比較対象回路データ49を読み込む。比較元回路または比較対象回路には、後述するマージ処理によって削除されるフリップフロップ間にバッファやインバータが存在することがある。バッファは、入力と出力の論理が同じであるので、削除されても、論理的な影響はない。また、インバータは、入力と出力の論理が反転するので、偶数個ずつ削除されても、論理的な影響はない。
【0024】
そこで、論理を圧縮するため、論理圧縮部43は、これらのバッファやインバータを削除する。バッファについては、全てを削除してよいが、インバータについては偶数個ずつ削除する。例えば、図14に示す比較対象回路21の例では、論理圧縮部43は、第4のフリップフロップD22と第5のフリップフロップE23の間に存在する全てのバッファ28,29,30と偶数個(2個)のインバータ26,27を削除する。論理圧縮部43は、比較元回路と比較対象回路の両方に対して論理圧縮処理を行う。
【0025】
フリップフロップマージ部44は、論理圧縮部43により論理が圧縮された回路データに基づいて、シンクロナイザやレベルシフタなどの論理的に等価なフリップフロップを、その挿入箇所から削除して前段のフリップフロップにマージ、すなわち統合して一つのフリップフロップとする。その際、フリップフロップマージ部44は、マージのために削除するフリップフロップのレジスタ名を、マージ処理後に残るフリップフロップの名前に追加し、それによって、削除されるフリップフロップのレジスタ名も保持する。
【0026】
例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22と第5のフリップフロップE23は、他の回路の論理に影響を及ぼさないので、フリップフロップマージ部44は、マージ処理によって、この二つのフリップフロップD22,E23を削除し、第1のフリップフロップA3にマージする。そして、フリップフロップマージ部44は、第1のフリップフロップA3のレジスタ名を、FF_A、FF_DおよびFF_Eとする。フリップフロップマージ部44は、比較元回路と比較対象回路の両方に対してマージ処理を行う。フリップフロップマージ部44は、次の(1)〜(4)の条件を満足するときに、マージ処理を行う。
【0027】
(1)マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されていること。ここで、フリップフロップマージ部44は、二つのフリップフロップを駆動するクロック信号について、クロック名が同じである場合、外部より与えたクロックドメイングループが同じである場合、またはクロック信号のバックトレースにより同一クロックドメインと判断される場合に、二つのフリップフロップが同じクロック信号で駆動されていると判断する。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、第1のフリップフロップA3と同じクロック信号G(CLK_G)で駆動されているので、上記(1)の条件を満たす。
【0028】
(2)マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップであること。フリップフロップに複数の入力がある場合、または複数の出力がある場合には、このフリップフロップがマージによって他のフリップフロップに統合されてしまうと、このフリップフロップへ信号を出力する回路の出力先がなくなったり、このフリップフロップから信号を入力する回路に信号が入力されなくなるという不具合が生じる。そのため、マージ処理を行うことができない。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、データラインが1入力1出力タイプのフリップフロップであるので、この(2)の条件を満たす。
【0029】
(3)マージ処理によって削除される複数のフリップフロップ間に論理回路が存在しないこと。(4)マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプであること。フリップフロップには、入力ピンがデータ(DATA)ピンとクロック(CLK)ピンだけである単純なタイプのものや、それらの入力ピン以外に、セット(SET)ピン、もしくはリセット(RESET)ピンを有する単純でないタイプのものや、セット(SET)ピンとリセット(RESET)ピンの両方を有する単純でないタイプのものなどがある。入力ピンの種類が同じフリップフロップ同士であれば、マージ処理を行うことができる。
【0030】
ただし、入力ピンの種類が同じでなくても、前記単純なタイプのフリップフロップは、いずれのタイプのフリップフロップともマージすることができる。この場合、前記単純なタイプのフリップフロップが削除され、単純でないタイプのフリップフロップが残る。例えば、図14に示す比較対象回路21の例では、第4のフリップフロップD22および第5のフリップフロップE23は、第1のフリップフロップA3と同じ単純なタイプのフリップフロップであるので、この(4)の条件を満たす。
【0031】
マッチング部45は、フリップフロップマージ部44によりそれぞれマージ処理がなされた比較元回路および比較対象回路の各データに基づいて、比較元回路と比較対象回路のフリップフロップを対応付ける。この時、双方の回路のフリップフロップの名前が一致するか否かを調べる。マッチング部45は、フリップフロップの名前が一致しなければ、別の手段による対応付けを行っても良いが、この発明では言及しない。比較検証部46は、マッチング部45により対応づけられたフリップフロップの入力を始点とするロジックコーンについて、比較元回路と比較対象回路の比較検証を行う。レポート出力部47は、比較検証部46による比較検証結果のレポート50を出力する。
【0032】
なお、上述したデザイン読み込み部42、論理圧縮部43、フリップフロップマージ部44、マッチング部45、比較検証部46およびレポート出力部47は、具体的には、例えば、図1に示したROM102、RAM103、HD105などの記録媒体に記録されたプログラムを、CPU101が実行することによって、またはI/F109によって、その機能を実現する。
【0033】
(論理等価検証処理手順)
次に、この発明の実施の形態にかかる論理等価検証装置の処理手順について説明する。図3は、この発明の実施の形態にかかる論理等価検証装置の処理手順を示すフローチャートである。図3に示すように、論理等価検証処理が開始されると、まず、デザイン読み込み部42により、比較元回路データ48と比較対象回路データ49が読み込まれる(ステップS1)。例えば、比較対象回路データ49は、比較元回路のメタ・ステーブル問題の対策として、比較元回路にフリップフロップを挿入した回路のデータである。
【0034】
次いで、論理圧縮部43により、比較元回路および比較対象回路のそれぞれについて、バッファやインバータを削除する論理圧縮処理が行われる(ステップS2)。論理圧縮処理の詳細については、後述する。次いで、フリップフロップマージ部44により、比較元回路および比較対象回路のそれぞれについて、フリップフロップのマージ処理が行われる(ステップS3)。このマージ処理の詳細については、後述する。
【0035】
次いで、マッチング部45により、比較元回路と比較対象回路で対応するロジックコーンの対応付けを行う。この発明ではフリップフロップの名前が一致するか否かを調べるネームマッチング処理を行う(ステップS4)。ネームマッチング処理の詳細については、後述する。次いで、比較検証部46により、比較元回路と比較対象回路の論理が一致するか否かを調べる比較検証処理が行われる(ステップS5)。そして、レポート出力部47により比較検証結果のレポートが出力され、(ステップS6)図3に示す一連の論理等価検証処理が終了する。
【0036】
(論理圧縮処理手順)
図4は、論理圧縮処理手順を示すフローチャートである。図4に示すように、論理圧縮処理が開始されると、まず、注目したフリップフロップのデータピンに接続する前段の論理プリミティブ検索を行う(ステップS11)。検索の結果、前段の回路がバッファであるか否かを判断する(ステップS12)。バッファである場合(ステップS12:Yes)、そのバッファをバッファ削除リストにスタックし、スタックしたバッファの前段の論理プリミティブ検索を行い(ステップS13)、ステップS12に戻る。
【0037】
ステップS12で、バッファでない場合(ステップS12:No)、検索により得た前段回路がインバータであるか否かを判断する(ステップS14)。インバータである場合(ステップS14:Yes)、インバータカウンタをインクリメントし、そのインバータをインバータ削除リストにスタックする。そして、スタックしたインバータの前段のセル検索を行い(ステップS15)、ステップS12に戻る。ステップS14で、インバータでない場合(ステップS14:No)、検索により得た前段回路がフリップフロップであるか否かを判断する(ステップS16)。
【0038】
フリップフロップでない場合(ステップS16:No)、インバータカウンタのリセット、インバータ削除リストの削除およびバッファ削除リストの削除を行う(ステップS17)。そして、ステップS11に戻る。ステップS16で、フリップフロップである場合(ステップS16:Yes)、インバータ削除リストにスタックされているインバータ群から[スタックされている個数/2]のあまりを除いた残りのインバータを削除し、バッファ削除リストにスタックされているバッファ群を削除する(ステップS18)。そして、ステップS17へ進む。以上のステップS11〜ステップS18の一連の処理を、回路全体について行い、図4に示す一連の論理圧縮処理が終了する。
【0039】
図5は、論理圧縮処理後の回路を示すアルゴリズム説明図である。例えば、図14に示す比較対象回路21に対して論理圧縮処理を行った結果、図5に示すように、第4のフリップフロップD22と第5のフリップフロップE23の間のバッファ(28,29,30)および偶数個のインバータ(26,27)が削除される。
【0040】
(フリップフロップのマージ処理手順)
図6は、フリップフロップのマージ処理手順を示すフローチャートである。ここでは、説明の便宜上、二つのフリップフロップのうち、一方を比較元フリップフロップとし、他方を処理対象フリップフロップとする。図6に示すように、フリップフロップのマージ処理が開始されると、まず、注目した回路がフリップフロップであるか否かを判断する(ステップS21)。フリップフロップである場合(ステップS21:Yes)、これを比較元フリップフロップとし、比較元フリップフロップのデータパスピンの前段の論理プリミティブ検索を行う(ステップS22)。検索により得た前段回路がフリップフロップであるか否かを判断する(ステップS23)。
【0041】
フリップフロップである場合(ステップS23:Yes)、これを処理対象フリップフロップとし、処理対象フリップフロップのクロックが比較元フリップフロップのクロックと同じであるか否かを判断する(ステップS24)。クロックが同じである場合(ステップS24:Yes)、さらに、処理対象フリップフロップのデータラインのファンイン数およびファンアウト数が1であるか否かを判断する(ステップS25)。データラインのファンイン数およびファンアウト数が1である場合(ステップS25:Yes)、ステップS26へ進む。データラインのファンイン数が2以上、もしくはファンアウト数が2以上である場合(ステップS25:No)、また、ステップS21、またはステップS23でNoである場合、ステップS21に戻る。そして、別の回路に注目し、ステップS21〜ステップS25を行う。
【0042】
ステップS26では、処理対象フリップフロップが単純なタイプのものであるか否かを判断する。単純なタイプのフリップフロップについては、先に説明した通りである。単純なタイプである場合(ステップS26:Yes)、比較元フリップフロップが削除リストに登録されているか否かを判断する(ステップS27)。登録されている場合(ステップS27:Yes)、処理対象フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、比較元フリップフロップのマージ先と同じである。そして、比較元フリップフロップのマージ先フリップフロップの名前に処理中のフリップフロップの名前を全て追加する(ステップS28)。
【0043】
ステップS27で、登録されていない場合(ステップS27:No)、処理対象フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、比較元フリップフロップである。そして、比較元フリップフロップの名前に処理中のフリップフロップの名前を全て追加する(ステップS29)。一方、ステップS26で、単純なタイプでない場合(ステップS26:No)、処理対象フリップフロップが比較元フリップフロップと同じタイプであるか否かを判断する(ステップS30)。同じタイプである場合(ステップS30:Yes)、ステップS27へ進む。
【0044】
同じタイプでない場合(ステップS30:No)、さらに、比較元フリップフロップが単純なタイプであるか否かを判断する(ステップS31)。単純なタイプでない場合(ステップS31:No)、ステップS21に戻り、別の回路に注目し、ステップS21以降の処理を行う。単純なタイプである場合(ステップS31:Yes)、処理対象フリップフロップが削除リストに登録されているか否かを判断する(ステップS32)。登録されている場合(ステップS32:Yes)、比較元フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、処理対象フリップフロップのマージ先と同じである。そして、処理対象フリップフロップのマージ先フリップフロップの名前に比較元フリップフロップの名前を全て追加する(ステップS33)。
【0045】
ステップS32で、登録されていない場合(ステップS32:No)、比較元フリップフロップを削除リストにスタックする。この場合のマージ先フリップフロップは、処理対象フリップフロップである。そして、処理対象フリップフロップの名前に比較元フリップフロップの名前を全て追加する(ステップS34)。以上のステップS21〜ステップS34の一連の処理を、回路全体について行う。その後、削除リストに登録されているフリップフロップ全体について、フリップフロップの削除を行い(ステップS35)、図6に示す一連のマージ処理が終了する。
【0046】
図7は、フリップフロップのマージ処理後の回路を示すアルゴリズム説明図である。例えば、図14に示す比較対象回路21に対してフリップフロップのマージ処理を行った結果、図7に示すように、第1のフリップフロップA3と第4のフリップフロップDと第5のフリップフロップEがマージされて、一つのフリップフロップになっている。図示例では、マージ先フリップフロップは、第1のフリップフロップA3であり、この第1のフリップフロップA3は、レジスタ名としてFF_A、FF_DおよびFF_Eを有する。従って、図7に示す比較対象回路21と、図14に示す比較対象回路21で、論理が一致することになる。
【0047】
ここで、フリップフロップのマージパターンおよび削除リストの一例について説明する。図8〜図10は、フリップフロップのマージパターンを示す模式図である。図8に示すパターンは、フリップフロップJ(FF_J)61とフリップフロップK(FF_K)62がともにフリップフロップL(FF_L)63をマージ先としてマージされるパターンである。
【0048】
図9に示すパターンは、フリップフロップM(FF_M)64がフリップフロップN(FF_N)65をマージ先としてマージされ、さらに、そのフリップフロップN(FF_N)65がフリップフロップP(FF_P)66をマージ先としてマージされるパターンである。図10に示すパターンは、フリップフロップQ(FF_Q)67とフリップフロップT(FF_T)69がその間のフリップフロップR(FF_R)68をマージ先としてマージされるパターンである。図11は、削除リストの一例を示す模式図である。図8〜図10に示すフリップフロップのマージが起こると、削除リストは、図11に示すようになる。
【0049】
(マッチング処理手順)
図12は、マッチング処理手順を示すフローチャートである。ここでは、説明の便宜上、比較元回路のフリップフロップを比較元フリップフロップとし、比較対象回路のフリップフロップを処理対象フリップフロップとする。図12に示すように、マッチング処理が開始されると、まず、比較元フリップフロップの全てについて、名前の一致するフリップフロップを処理対象からさがすネームマッチング処理を行う(ステップS41)。
【0050】
そして、名前が一致するフリップフロップ同士をペアとして対応づける。一方、ネームマッチング処理において名前の一致するフリップフロップがなかった比較元フリップフロップには、エラーフラグがつく。ネームマッチング処理の詳細な手順については後述する。全ての比較元フリップフロップについてネームマッチング処理が終了したら、エラーフラグのついた比較元フリップフロップについて、さらに別の手法で対応づけを行う(ステップS42)。例えば、機能的に一致するフリップフロップ同士を対応づけるファンクションマッチング処理を行う。
【0051】
(ネームマッチング処理手順)
図13は、ネームマッチング処理手順のうち、比較元回路のフリップフロップを1つ選択し、それに対応するフリップフロップを比較対象回路から見つける処理を示すフローチャートである。ここでは、説明の便宜上、比較元回路から選択したフリップフロップを比較元フリップフロップとし、比較対象回路のフリップフロップを処理対象フリップフロップとする。図13に示すように、マッチング処理が開始されると、まず、比較元フリップフロップと処理対象フリップフロップで名前が一致するか否かを判断する(ステップS51)。一致しない場合(ステップS51:No)、処理対象フリップフロップに複数の名前があるか否かを判断する(ステップS52)。
【0052】
名前が一つである場合(ステップS52:No)、ステップS55へ進む。複数の名前がある場合(ステップS52:Yes)、処理対象フリップフロップの全ての名前と比較元フリップフロップの名前を比較する(ステップS53)。そして、処理対象フリップフロップのいずれかの名前と比較元フリップフロップの名前が一致するか否かを判断する(ステップS54)。一致しない場合(ステップS54:No)、ステップS55へ進む。ステップS55では、比較元フリップフロップに複数の名前があるか否かを判断する。
【0053】
名前が一つである場合(ステップS55:No)、比較元フリップフロップにエラーフラグを立てて(ステップS56)、ステップS51に戻る。複数の名前がある場合(ステップS55:Yes)、比較元フリップフロップの全ての名前と処理対象フリップフロップの名前を比較する(ステップS57)。そして、比較元フリップフロップのいずれかの名前と処理対象フリップフロップの名前が一致するか否かを判断する(ステップS58)。
【0054】
一致しない場合(ステップS58:No)、ステップS56へ進む。一致する場合(ステップS58:Yes)、また、ステップS51またはステップS54でYesの場合、処理中の処理対象フリップフロップと比較元フリップフロップのマッチング処理を終了する。以上のステップS51〜ステップS58の一連の処理を、比較対象の全フリップフロップについて行い、比較元フリップフロップと同じ名前のフリップフロップを見つける。同じ名前のフリップフロップが見つかった場合はペアとなり(ステップS59)、それらのフリップフロップの入力を始点とするロジックコーンが論理等価検証の対象となる。これを比較元の全フリップフロップについて行う。
【0055】
このネームマッチング処理において、図14に示す比較元回路1の第1のフリップフロップA3は、レジスタ名としてFF_Aを有し、図7に示す比較対象回路21の第1のフリップフロップA3は、レジスタ名にFF_Aを含むので、比較元回路1と比較対象回路21で第1のフリップフロップA3の名前が一致することになる。従って、図14に示す比較元回路1と図14に示す比較対象回路21の比較検証を行うと、いずれの回路でも第2のロジックコーン8が、レジスタ名がFF_Aである第1のフリップフロップA3の入力を始点とすることになるので、名前によるペアが自動で作成され、両回路の論理が一致するという検証結果が得られる。
【0056】
以上説明したように、実施の形態によれば、比較元回路1と、シンクロナイザなどのように論理的に等価なフリップフロップが挿入された比較対象回路21との論理等価検証を行う際に、論理的に等価なフリップフロップの挿入が原因で両回路の論理が不一致であるという結果が出るのを防ぐことができる。従って、従来のような人手による作業を行うことなく、論理的に等価なフリップフロップが挿入された回路について論理等価検証を自動的に行うことができるという効果を奏する。また、論理的に等価なフリップフロップをレベルシフタとして挿入した回路についても、本実施の形態を適用することによって、検証ポイントを削減することができるので、検証に要する時間を削減することができる。
【0057】
なお、本実施の形態で説明した論理等価検証プログラムは、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、CD−ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な伝送媒体であってもよい。以上において本発明は、上述した実施の形態に限らず、種々変更可能である。
【0058】
(付記1)比較元回路と比較対象回路との論理等価検証を行う論理等価検証装置において、比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ手段と、それぞれ、前記フリップフロップマージ手段で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング手段と、を備えることを特徴とする論理等価検証装置。
【0059】
(付記2)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする付記1に記載の論理等価検証装置。
【0060】
(付記3)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする付記1に記載の論理等価検証装置。
【0061】
(付記4)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする付記3に記載の論理等価検証装置。
【0062】
(付記5)前記フリップフロップマージ手段は、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする付記3または4に記載の論理等価検証装置。
【0063】
(付記6)前記フリップフロップマージ手段は、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする付記3に記載の論理等価検証装置。
【0064】
(付記7)前記フリップフロップマージ手段によるマージ処理を行う前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮手段、をさらに備えることを特徴とする付記1に記載の論理等価検証装置。
【0065】
(付記8)比較元回路と比較対象回路との論理等価検証を行う論理等価検証方法において、比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ工程と、それぞれ、前記フリップフロップマージ工程で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング工程と、を含むことを特徴とする論理等価検証方法。
【0066】
(付記9)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする付記8に記載の論理等価検証方法。
【0067】
(付記10)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする付記8に記載の論理等価検証方法。
【0068】
(付記11)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする付記10に記載の論理等価検証方法。
【0069】
(付記12)前記フリップフロップマージ工程では、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする付記10または11に記載の論理等価検証方法。
【0070】
(付記13)前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする付記10に記載の論理等価検証方法。
【0071】
(付記14)前記フリップフロップマージ工程の前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮工程、をさらに含むことを特徴とする付記8に記載の論理等価検証方法。
【0072】
(付記15)付記8〜14のいずれか一つに記載の論理等価検証方法をコンピュータに実行させることを特徴とする論理等価検証プログラム。
【0073】
(付記16)付記15に記載の論理等価検証プログラムを記録したことを特徴とするコンピュータに読み取り可能な記録媒体。
【産業上の利用可能性】
【0074】
以上のように、本発明にかかる論理等価検証装置、論理等価検証方法、論理等価検証プログラムおよび記録媒体は、論理回路の設計に有用であり、特に、半導体集積回路の設計に適している。
【図面の簡単な説明】
【0075】
【図1】この発明の実施の形態にかかる論理等価検証装置のハードウェア構成を示すブロック図である。
【図2】この発明の実施の形態にかかる論理等価検証装置の機能的構成を示すブロック図である。
【図3】この発明の実施の形態にかかる論理等価検証装置の処理手順を示すフローチャートである。
【図4】この発明の実施の形態にかかる論理圧縮処理手順を示すフローチャートである。
【図5】論理圧縮処理後の回路を示すアルゴリズム説明図である。
【図6】この発明の実施の形態にかかるフリップフロップのマージ処理手順を示すフローチャートである。
【図7】フリップフロップのマージ処理後の回路を示すアルゴリズム説明図である。
【図8】フリップフロップのマージパターンの第1の例を示す模式図である。
【図9】フリップフロップのマージパターンの第2の例を示す模式図である。
【図10】フリップフロップのマージパターンの第3の例を示す模式図である。
【図11】削除リストの一例を示す模式図である。
【図12】この発明の実施の形態にかかるマッチング処理手順を示すフローチャートである。
【図13】この発明の実施の形態にかかるネームマッチング処理手順を示すフローチャートである。
【図14】論理等価検証を行う比較元回路と比較対象回路を示すアルゴリズム説明図である。
【符号の説明】
【0076】
1 比較元回路
3,22,23,61〜69 フリップフロップ
21 比較対象回路
26,27 インバータ
28,29,30 バッファ
41 論理等価検証装置
43 論理圧縮部
44 フリップフロップマージ部
45 マッチング部
48 比較元回路データ
49 比較対象回路データ
【特許請求の範囲】
【請求項1】
比較元回路と比較対象回路との論理等価検証を行う論理等価検証装置において、
比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ手段と、
それぞれ、前記フリップフロップマージ手段で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング手段と、
を備えることを特徴とする論理等価検証装置。
【請求項2】
比較元回路と比較対象回路との論理等価検証を行う論理等価検証方法において、
比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ工程と、
それぞれ、前記フリップフロップマージ工程で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング工程と、
を含むことを特徴とする論理等価検証方法。
【請求項3】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする請求項2に記載の論理等価検証方法。
【請求項4】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする請求項2に記載の論理等価検証方法。
【請求項5】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする請求項4に記載の論理等価検証方法。
【請求項6】
前記フリップフロップマージ工程では、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする請求項4または5に記載の論理等価検証方法。
【請求項7】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする請求項4に記載の論理等価検証方法。
【請求項8】
前記フリップフロップマージ工程の前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮工程、をさらに含むことを特徴とする請求項2に記載の論理等価検証方法。
【請求項9】
請求項2〜8のいずれか一つに記載の論理等価検証方法をコンピュータに実行させることを特徴とする論理等価検証プログラム。
【請求項10】
請求項9に記載の論理等価検証プログラムを記録したことを特徴とするコンピュータに読み取り可能な記録媒体。
【請求項1】
比較元回路と比較対象回路との論理等価検証を行う論理等価検証装置において、
比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ手段と、
それぞれ、前記フリップフロップマージ手段で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング手段と、
を備えることを特徴とする論理等価検証装置。
【請求項2】
比較元回路と比較対象回路との論理等価検証を行う論理等価検証方法において、
比較元回路および比較対象回路の各設計データに基づいて、前記比較元回路および前記比較対象回路のそれぞれについて、論理的に等価なフリップフロップを、該フリップフロップの挿入箇所から削除して他のフリップフロップにマージするフリップフロップマージ工程と、
それぞれ、前記フリップフロップマージ工程で論理的に等価なフリップフロップが削除された比較元回路および比較対象回路について、対応するフリップフロップの名前が一致するか否かを調べるマッチング工程と、
を含むことを特徴とする論理等価検証方法。
【請求項3】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップの名前を、マージ処理後に残るフリップフロップの名前に追加することを特徴とする請求項2に記載の論理等価検証方法。
【請求項4】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じクロック信号で駆動されている場合に、マージ処理を行うことを特徴とする請求項2に記載の論理等価検証方法。
【請求項5】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップのデータラインが1入力1出力タイプのフリップフロップである場合に、マージ処理を行うことを特徴とする請求項4に記載の論理等価検証方法。
【請求項6】
前記フリップフロップマージ工程では、マージ処理によって削除される複数のフリップフロップにおいて、前段のフリップフロップの出力の論理と後段のフリップフロップの入力の論理が同じである場合に、マージ処理を行うことを特徴とする請求項4または5に記載の論理等価検証方法。
【請求項7】
前記フリップフロップマージ工程では、マージ処理によって削除されるフリップフロップが、マージ処理後に残るフリップフロップと同じタイプである場合に、マージ処理を行うことを特徴とする請求項4に記載の論理等価検証方法。
【請求項8】
前記フリップフロップマージ工程の前に、マージ処理によって削除される複数のフリップフロップ間にバッファもしくは偶数個のインバータが存在する場合、該バッファおよび該インバータを削除する論理圧縮工程、をさらに含むことを特徴とする請求項2に記載の論理等価検証方法。
【請求項9】
請求項2〜8のいずれか一つに記載の論理等価検証方法をコンピュータに実行させることを特徴とする論理等価検証プログラム。
【請求項10】
請求項9に記載の論理等価検証プログラムを記録したことを特徴とするコンピュータに読み取り可能な記録媒体。
【図1】
【図2】
【図3】
【図4】
【図5】
【図6】
【図7】
【図8】
【図9】
【図10】
【図11】
【図12】
【図13】
【図14】
【図2】
【図3】
【図4】
【図5】
【図6】
【図7】
【図8】
【図9】
【図10】
【図11】
【図12】
【図13】
【図14】
【公開番号】特開2008−262337(P2008−262337A)
【公開日】平成20年10月30日(2008.10.30)
【国際特許分類】
【出願番号】特願2007−103846(P2007−103846)
【出願日】平成19年4月11日(2007.4.11)
【出願人】(308014341)富士通マイクロエレクトロニクス株式会社 (2,507)
【Fターム(参考)】
【公開日】平成20年10月30日(2008.10.30)
【国際特許分類】
【出願日】平成19年4月11日(2007.4.11)
【出願人】(308014341)富士通マイクロエレクトロニクス株式会社 (2,507)
【Fターム(参考)】
[ Back to top ]