(57)【要約】【課題】ラッチ変換による遅延最適化回路と元の回路との等価性検証に、従来の等価性検証システムを用いるには、遅延最適化回路のラッチやＦＦと、元の回路のＦＦの対応情報を人手で作成し入力する必要があった。【解決手段】データ処理装置１０は、ラッチ変換による遅延最適化回路の情報２２を入力し、これの第１のラッチ、第２のラッチをそれぞれＦＦ、バッファに変換した中間回路情報２３を生成する中間回路生成部１１と、中間回路情報２３と元の論理回路情報２１の等価性を検証する等価性検証部１２と、ラッチ変換による遅延最適化回路の情報２２を入力し、第１のラッチの出力ネットを辿って、次のＦＦ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証部１４とを備える。【選択図】      図１
2005107566.tif 000002
【特許請求の範囲】
【請求項１】
フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路の等価性検証システムであって、
前記遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手段と、中間回路と元の論理回路を入力しその等価性を検証する手段と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手段とを備えたことを特徴とするラッチ変換による遅延最適化回路の等価性検証システム。
【請求項２】
前記元の論理回路のフリップフロップをクロックがローレベルからハイレベルの変化時に入力されるデータを保持するものとし、前記第１のラッチを、クロックがロウレベルのときに入力データを出力側にスルーとし、クロックがハイレベルに変化時ラッチするローアクティブラッチとし、前記第２のラッチを、クロックがハイレベルのときに入力データを出力側にスルーとし、クロックがローレベルに変化時ラッチするハイアクティブラッチとすることを特徴とする請求項１記載のラッチ変換による遅延最適化回路の等価性検証システム。
【請求項３】
前記等価性を検証する手段は、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手段と、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手段とを含むことを特徴とする請求項１、又は２記載のラッチ変換による遅延最適化回路の等価性検証システム。
【請求項４】
フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路の等価性検証方法であって、
前記遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、中間回路と元の論理回路を入力しその等価性を検証する手順と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とを含むことを特徴とするラッチ変換による遅延最適化回路の等価性検証方法。
【請求項５】
前記元の論理回路のフリップフロップをクロックがローレベルからハイレベルの変化時に入力されるデータを保持するものとし、前記第１のラッチを、クロックがロウレベルのときに入力データを出力側にスルーとし、クロックがハイレベルに変化時ラッチするローアクティブラッチとし、前記第２のラッチを、クロックがハイレベルのときに入力データを出力側にスルーとし、クロックがローレベルに変化時ラッチするハイアクティブラッチとすることを特徴とする請求項４記載のラッチ変換による遅延最適化回路の等価性検証方法。
【請求項６】
前記等価性を検証する手順は、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手順と、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手順とを含むことを特徴とする請求項４、又は５記載のラッチ変換による遅延最適化回路の等価性検証方法。
【請求項７】
フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、
中間回路と元の論理回路を入力しその等価性を検証する手順と、
前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とを
コンピュータに実行させるためのプログラム。
【請求項８】
フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、
中間回路と元の論理回路を入力する手順、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手順、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手順からなる論理の等価性を検証する手順と、
前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とを
コンピュータに実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はラッチ変換による遅延最適化回路の等価性検証システムと方法、及びプログラムに関し、特に元の論理回路の非ラッチ化指定されなかったフリップフロップをラッチに変換し、その出力側の組み合わせ回路の適切な位置に前記ラッチとはラッチタイミングが異なる第２のラッチを挿入した遅延最適回路について、元の回路との等価性や、ラッチ組み合わせの妥当性を検証するラッチ変換による遅延最適化回路の等価性検証システムと方法、及びプログラムに関する。
【背景技術】
【０００２】
従来の等価性検証では、第１の方法として、論理回路をレジスタで切った論理木に分割し、分割した論理木同士を比較する方法がとられる。
【０００３】
又、第２の方法として、二つの論理回路における論理の等価性を検証する論理照合方式として二つの論理回路を構成するフリップフロップの対応情報を入力として準備し、対応関係を有するフリップフロップごとに各論理回路から小論理回路を抽出し、小論理回路の組毎に論理照合を行う方式がある（特許文献１参照。）。
【０００４】
【特許文献１】特開平９−２１８５０（段落［０００９］、［００１０］、［００２０］）
【発明の開示】
【発明が解決しようとする課題】
【０００５】
しかし、図２、図３で示されるように、特願２００２−２０７６５８に記載の方法により、元の論理回路の非ラッチ化指定されていないフリップフロップ（以下ＦＦと省略）は、遅延最適化を行った回路ではスルー状態を持つラッチに変換されており、また、そのラッチと反対の時間でスルーを行うラッチが挿入されているため、元の論理回路と遅延最適化の結果の回路のＦＦの対応がとれなくなっている。
【０００６】
従って、遅延最適化を行った回路の元の論理回路との等価性を検証するシステムや方法として前記従来の第１の方法や第２の方法を用いるには、遅延最適化を行った回路のラッチやＦＦと、元の論理回路のＦＦの対応情報を人手で作成する必要があるという問題点がある。
【０００７】
本発明の目的は、遅延最適化の結果の回路から元の論理回路とＦＦの対応がとれる中間回路を自動作成し、両者の等価性検証を可能とし、遅延最適化の結果のラッチ組み合わせの妥当性を検証できる、ラッチ変換による遅延最適化回路の等価性検証システムと方法、及びプログラムを提供することにある。
【課題を解決するための手段】
【０００８】
本発明の第１のラッチ変換による遅延最適化回路の等価性検証システムは、フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路の等価性検証システムであって、前記遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手段と、中間回路と元の論理回路を入力しその等価性を検証する手段と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手段とを備えたことを特徴とする。
【０００９】
本発明の第２のラッチ変換による遅延最適化回路の等価性検証システムは、前記第１のラッチ変換による遅延最適化回路の等価性検証システムであって、前記元の論理回路のフリップフロップをクロックがローレベルからハイレベルの変化時に入力されるデータを保持するものとし、前記第１のラッチを、クロックがロウレベルのときに入力データを出力側にスルーとし、クロックがハイレベルに変化時ラッチするローアクティブラッチとし、前記第２のラッチを、クロックがハイレベルのときに入力データを出力側にスルーとし、クロックがローレベルに変化時ラッチするハイアクティブラッチとすることを特徴とする。
【００１０】
本発明の第３のラッチ変換による遅延最適化回路の等価性検証システムは、前記第１、又は第２のラッチ変換による遅延最適化回路の等価性検証システムであって、前記等価性を検証する手段は、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手段と、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手段とを含むことを特徴とする。
【００１１】
本発明の第１のラッチ変換による遅延最適化回路の等価性検証方法は、フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路の等価性検証方法であって、前記遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、中間回路と元の論理回路を入力しその等価性を検証する手順と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とを含むことを特徴とする。
【００１２】
本発明の第２のラッチ変換による遅延最適化回路の等価性検証方法は、前記第１のラッチ変換による遅延最適化回路の等価性検証方法であって、前記元の論理回路のフリップフロップをクロックがローレベルからハイレベルの変化時に入力されるデータを保持するものとし、前記第１のラッチを、クロックがロウレベルのときに入力データを出力側にスルーとし、クロックがハイレベルに変化時ラッチするローアクティブラッチとし、前記第２のラッチを、クロックがハイレベルのときに入力データを出力側にスルーとし、クロックがローレベルに変化時ラッチするハイアクティブラッチとすることを特徴とする。
【００１３】
本発明の第３のラッチ変換による遅延最適化回路の等価性検証方法は、前記第１、又は第２のラッチ変換による遅延最適化回路の等価性検証方法であって、前記等価性を検証する手順は、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手順と、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手順とを含むことを特徴とする。
【００１４】
本発明の第１のプログラムは、フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、中間回路と元の論理回路を入力しその等価性を検証する手順と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とをコンピュータに実行させることを特徴とする。
【００１５】
本発明の第２のプログラムは、フリップフロップと組み合わせ回路とを含む元の論理回路に対して、ラッチ変換による遅延最適化、即ち前記フリップフロップで非ラッチ化指定されなかったフリップフロップを、フリップフロップが入力データを取り込むクロックのレベルでスルーとなる第１のラッチに変換し、前記クロックレベルとは異なるレベルでスルーとなる第２のラッチを論理回路の所定部分に挿入する遅延最適化を行った回路を入力し、これの第１のラッチをフリップフロップに変換し、第２のラッチをバッファに変換した中間回路を生成する手順と、中間回路と元の論理回路を入力する手順、中間回路の各フリップフロップと元の論理回路の各フリップフロップとの対応付けを行う手順、中間回路の任意のフリップフロップの入力の論理が、元の論理回路上で、前記任意のフリップフロップに対応するフリップフロップの入力の論理に等価であることを確認する手順からなる論理の等価性を検証する手順と、前記遅延最適化を行った回路を入力し、第１のラッチの出力ネットを辿って、次のフリップフロップ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックするラッチ組み合わせ検証手順とをコンピュータに実行させることを特徴とする。
【発明の効果】
【００１６】
特願２００２−２０７６５８の記載の方法により遅延最適化された回路は、そのままでは、従来の等価性検証を適用するには、設計者がレジスタ位置の対応を手作業で指定する必要があるが、本発明は、全て自動で検証できるため、工数の削減を可能とする。
【００１７】
また、第１のラッチの出力ネットを辿って、次のＦＦ或いは次の第１のラッチまでの間に対となる第２のラッチが挿入されていることをチェックしており、遅延最適化のためのＦＦのラッチ変換が適切に行われたかを自動検証できる。
【発明を実施するための最良の形態】
【００１８】
次に、本発明を実施するための最良の形態について図面を参照して詳細に説明する。本実施形態の説明を、特願２００２−２０７６５８に記載された遅延最適化方法で、元の論理回路のＦＦをＬＯＷラッチに変換し、ＬＯＷラッチの出力側にＨＩＧＨラッチを挿入してある場合の例を用いて説明する。
【００１９】
ここでＬＯＷラッチとは、クロックがロウレベルのときに入力データを出力側にスルーとし、クロックがハイレベルでラッチするロウアクティブラッチであり、ＨＩＧＨラッチとは、クロックがハイレベルのときに入力データを出力側にスルーとし、クロックがロウレベルでラッチするハイアクティブラッチのことである。
【００２０】
図１は本発明のラッチ変換による遅延最適化回路の等価性検証システムのブロック図である。図１を参照し、本発明のラッチ変換による遅延最適化回路の等価性検証システムは、プログラム制御で動作するデータ処理装置１０とこれに接続された補助記憶装置２０とキーボード等の入力装置３０とディスプレイ等の出力装置４０を含む。
【００２１】
データ処理装置１０には論理検証部１３と、ラッチ組み合わせ検証部１４を含む。論理検証部１３は、ラッチ変換による遅延最適化回路の情報２２が元の論理回路情報２１に等価であることを検証する手段であり、中間回路生成部１１と等価性検証部１２を含む。
【００２２】
中間回路生成部１１は、前記遅延最適化回路の情報２２を入力とし、中間回路情報２３を生成する。
【００２３】
等価性検証部１２は、中間回路情報２３と元の論理回路情報２１との等価性検証を行う。
【００２４】
ラッチ組み合わせ検証部１４は、遅延最適化処理でＨＩＧＨラッチが正しい位置に挿入されているかをチェックする。
【００２５】
補助記憶装置２０は、ハードディスク装置或いは光ディスク装置等であり、これには元の論理回路情報２１、ラッチ変換による遅延最適化回路の情報２２が記憶されており、中間回路情報２３、検証結果情報２４も記憶される。
【００２６】
尚、中間回路情報２３、検証結果情報２４は補助記憶装置２０に記憶せず、データ処理装置１０の主記憶上の確保されたエリアに一時記憶する様にしてもよい。
【００２７】
又、論理検証部１３と、ラッチ組み合わせ検証部１４は好適にはデータ処理装置１０で実行されるプログラムで実現される。
【００２８】
次に、本発明を実施するための最良の形態の動作について図面を参照して説明する。先ず、図２に、元の論理回路を示す。図２を参照し、２ａは、非ラッチ化指定されたＦＦとする。又、ＦＦはクロックのロウからハイへの変化タイミングの直前（正確にはセットアップタイム分前のタイミング）で、組み合わせ回路２ｇ、２ｈからの入力信号レベルを取り込み、ＦＦ自身の動作遅延時間後に出力し、次のクロックの変化タイミングまではその出力値を保持する。
【００２９】
図３は、図２の元の論理回路に対し、特願２００２−２０７６５８に記載の遅延最適化を行った結果の回路である。
【００３０】
即ち、元の論理回路の非ラッチ化指定されていないＦＦ（２ｂ、２ｃ、２ｄ、２ｅ、２ｆ）がＬＯＷラッチ（３ｂ、３ｃ、３ｄ、３ｅ、３ｆ）に変換してあり、最小遅延補償の為に（これらのＬＯＷラッチ出力はクロックがロウ期間中に変化するが変化した出力が同じサイクルのロウ期間中に次段のＬＯＷラッチやＦＦに取込まれない様にする為に）、ＨＩＧＨラッチ（３ｋ、３ｌ、３ｍ、３ｎ）が挿入してある。
【００３１】
次に図５のフローチャートを参照し、論理検証部１３の動作を説明する。中間回路生成部１１はラッチ変換による遅延最適化回路の情報２２を読み込む（ステップＡ１）。
【００３２】
中間回路生成部１１は、遅延最適化の結果の回路のＦＦから変換されたＬＯＷラッチをＦＦに変換し（ステップＡ２）、ＨＩＧＨラッチをバッファに変換し（ステップＡ３）、変換後の回路を中間回路とし補助記憶装置に記憶する（ステップＡ３）。
【００３３】
即ち、図３で、ＦＦから変換されたＬＯＷラッチ（３ｂ、３ｃ、３ｄ、３ｅ、３ｆ）をＦＦ（４ｂ、４ｃ、４ｄ、４ｅ、４ｆ）に変換し、ＨＩＧＨラッチ（３ｋ、３ｌ、３ｍ、３ｎ）をバッファ（４ｋ、４ｌ、４ｍ、４ｎ）に変換した等価性検証用の中間回路（図４参照）を作成し、記憶する。
【００３４】
このとき、遅延最適化の結果の回路のＬＯＷラッチ（３ｂ、３ｃ、３ｄ、３ｅ、３ｆ）は、元の論理回路のＦＦ（２ｂ、２ｃ、２ｄ、２ｅ、２ｆ）と回路の論理構成上の同じ位置にあるので、中間回路のＦＦ（４ｂ、４ｃ、４ｄ、４ｅ、４ｆ）もまた、元の論理回路のＦＦ（２ｂ、２ｃ、２ｄ、２ｅ、２ｆ）と論理構成上の同じ位置にある。
【００３５】
従って、等価性検証部１２は、元の論理回路のＦＦ（２ａ、２ｂ、２ｃ、２ｄ、２ｅ、２ｆ）と中間回路のＦＦ（２ａ、４ｂ、４ｃ、４ｄ、４ｅ、４ｆ）との対応をとることにより、図２の元の論理回路と図３の中間回路の等価性検証を行うことができる。
【００３６】
図５のフローチャートに戻り、等価性検証部１２の具体動作例を示す。等価性検証部１２は中間回路が生成され記憶されたことを受けて、中間回路と元の回路情報を読み込む（ステップＡ５）。
【００３７】
中間回路の各ＦＦと元の回路の各ＦＦの対応付け情報を作成する。例えば、中間回路の各ＦＦ（２ａ、４ｂ、４ｃ、４ｄ、４ｅ、４ｆ）の入力信号名、或いはこれとＦＦ出力の行き先の回路素子（ゲート、インバータ、セレクタ等）の識別（素子番号或いは出力信号名）を取得し、元の回路情報で同じ入力信号名、或いはこれとＦＦ出力の行き先の回路素子に接続されたＦＦを探しＦＦ名（ＦＦ出力ネット名）の対応リストを作成する（ステップＡ６）。
【００３８】
中間回路でＦＦの一つを選択し（ステップＡ７）、選択したＦＦの入力信号（ネット）の論理木情報（前段のＦＦ名（ＦＦ出力ネット名）や外部入力ネット名による論理記述）を作成し、これのＦＦ名を対応する元の回路のＦＦ名に置換する（ステップＡ８）。
【００３９】
元の論理回路で、対応するＦＦの入力信号について論理木情報を作成する（ステップＡ９）。
【００４０】
ステップＡ８の置換後の論理木情報が、ステップＡ９の論理木情報に一致するかチェックし、少なくとも不一致であればその旨と、それぞれのＦＦ名、入力信号名、論理木情報を検証結果情報に記録する（ステップＡ１０）。
【００４１】
中間回路の全ＦＦについてチェックすれば（ステップＡ１１）、図６のラッチ組み合わせ検証部を呼び出し、そうでなければステップＡ７からＡ１１を繰り返す。
【００４２】
ここで、中間回路情報と元の回路情報にＲＴＬ（Ｒｅｇｉｓｔｏｒ  Ｔｒａｓｆｅｒ−ｌｅｂｅｌ）記述を含む場合は、中間回路の選択したレジスタやＦＦの入力は中間回路のレジスタ名、ＦＦ名で記述されている。この記述のレジスタ名、ＦＦ名を対応する元の回路のレジスタ名、ＦＦ名に置換し、これと元の回路情報の前記選択したレジスタやＦＦに対応するレジスタやＦＦの入力記述（ＲＴＬ記述）の一致をチェックする様にしてもよい。
【００４３】
この様にして、論理検証部１３は、元の回路のＦＦ間の組み合わせ回路の論理と、遅延最適化後の回路のＬＯＷラッチ間の組み合わせ回路の論理とが等価かどうかを検証することを可能とする。
【００４４】
但し、図３の各ＬＯＷラッチから次のＬＯＷラッチまたは非ラッチ化指定のＦＦまで、正しくデータが伝播されるためには、ＬＯＷラッチから次のＬＯＷラッチまたは非ラッチ化指定のＦＦまでにＨＩＧＨラッチが挿入されていなければならない。
【００４５】
ラッチ組み合わせ検証部１４は、元の論理回路のＦＦから変換されたＬＯＷラッチにの出力ネットを辿って、次のＦＦ、または、ＬＯＷラッチまでの間に対になるＨＩＧＨラッチが挿入されているかをチェックする。
【００４６】
図６のフローチャートを参照し、ラッチ組み合わせ検証部１４の詳細動作や結果出力動作を説明する。
【００４７】
ラッチ変換による遅延最適化回路で、ＬＯＷラッチの一つを選択し（ステップＢ１）、これの出力ネットを辿って次ぎのＬＯＷラッチ、或いはＦＦまでのパスを全て抽出する（ステップＢ２）。
【００４８】
抽出した各パスにＨＩＧＨラッチが挿入されているかチェックし、なければそのパス情報（始点のＬＯＷラッチ名（出力ネット名）、経路のゲートやセレクタ等の回路素子識別（出力ネット名、或いは素子番号）、終点のＬＯＷラッチ名或いはＦＦ名）を検証結果情報に記録する（ステップＢ３）。
【００４９】
最適化回路の全ＬＯＷラッチ（ＦＦより変換されたＬＯＷラッチの全て）についてチェックしてなければ（ステップＢ４）、ステップＢ１からＢ４を繰り返し、チェックが完了すると、等価性検証結果、ラッチ組み合わせ検証結果を出力装置に出力する（ステップＣ１）。
【００５０】
以上の説明では、元の論理回路のＦＦがクロックのロウからハイへの変化タイミングで入力信号レベルを取り込むタイプとし、遅延最適化で非ラッチ化指定のＦＦをＬＯＷラッチに変換し、その出力側のパスの適切な位置にＨＩＧＨラッチを挿入し、中間回路生成部がこのＬＯＷラッチ、ＨＩＧＨラッチを前記タイプのＦＦ、バッファに変換した中間回路を生成する例を説明した。
【００５１】
ここで、元の論理回路のＦＦがクロックのハイからロウへの変化タイミングで入力信号レベルを取り込む第２のタイプであれば、遅延最適化では非ラッチ化指定のＦＦをＨＩＧＨラッチに変換し、その出力側のパスの適切な位置にＬＯＷラッチが挿入される。
【００５２】
従って、中間回路生成部はこのＨＩＧＨラッチ、ＬＯＷラッチを第２のタイプのＦＦ、バッファに変換した中間回路を生成することで、同様に遅延最適化回路の元の論理回路との等価性検証を可能にする。
【００５３】
又、この場合はラッチ組み合わせ検証部は、遅延最適化回路のＨＩＧＨラッチから次ぎのＨＩＧＨラッチ、或いはＦＦ間にＬＯＷラッチが挿入されているかをチェックする。
【図面の簡単な説明】
【００５４】
【図１】本発明のラッチ変換による遅延最適化回路の等価性検証システムのブロック図。
【図２】図１の元の論理回路情報２１の例を示す図。
【図３】図１のラッチ変換による遅延最適化回路の情報２２の例を示す図。
【図４】図１の中間回路情報２３の例を示す図。
【図５】本発明の動作を示すフローチャート。
【図６】本発明の動作を示すフローチャート。
【符号の説明】
【００５５】
２ａ〜２ｆ    元の論理回路のＦＦ
２ｇ、２ｈ    元の論理回路の組み合わせ回路
３ｂ〜３ｆ    遅延最適化回路のＬＯＷラッチ
３ｋ〜３ｎ    遅延最適化回路のＨＩＧＨラッチ
３ｇ、３ｈ、３ｉ、３ｊ    遅延最適化回路の組み合わせ回路
４ｂ〜４ｆ    中間回路の変換されたＦＦ
４ｋ〜４ｎ    中間回路の変換されたバッファ
１０    データ処理装置
１１    中間回路生成部
１２    等価性検証部
１３    論理検証部
１４    ラッチ組み合わせ検証部
２０    補助記憶装置
２１    元の論理回路情報
２２    ラッチ変換による遅延最適化回路の情報
２３    中間回路情報
２４    検証結果情報
３０    入力装置
４０    出力装置
【図１】
2005107566.tif 000003
【図２】
2005107566.tif 000004
【図３】
2005107566.tif 000005
【図４】
2005107566.tif 000006
【図５】
2005107566.tif 000007
【図６】
2005107566.tif 000008