(57)【要約】【課題】２つの論理回路が論理的に等価検証を効率的に行い、不一致の場合にその原因となっている論理回路素子の特定を容易にする論理的な等価検証方法及び装置を提供する。【解決手段】それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する方法であって、前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換するステップと、前記変換ステップにおいて変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納するステップと、前記変換された論理式の中で指定された項に対応する前記論理回路素子を特定するステップとを有することを特徴とする方法を提供する。【選択図】　　　　　図４
2004021944.tif 000002
【特許請求の範囲】
【請求項１】
それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する方法であって、
前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換するステップと、
前記変換ステップにおいて変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納するステップと、
前記変換された論理式の中で指定された項に対応する前記論理回路素子を特定するステップとを有することを特徴とする方法。
【請求項２】
前記格納ステップは、前記論理式の展開履歴を更に格納することを特徴とする請求項１記載の方法。
【請求項３】
それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する方法であって、
前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換するステップと、
前記変換ステップにおいて変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納するステップと、
前記変換された論理式の中で不一致の項に対応する前記論理回路素子を特定するステップとを有することを特徴とする方法。
【請求項４】
請求項１乃至３のうちいずれか一項記載の方法をコンピュータによって実現するためのプログラム。
【請求項５】
それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する装置であって、
ユーザとの対話に従って、前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換する変換部と、
前記変換部において変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納する記憶部と、
前記論理コーンの構造及び前記論理式を表示すると共に、前記変換された論理式の中で指定された項に対応する前記論理回路素子を前記論理コーンの構造中に表示する表示部と、
前記項を指定するための入力部とを有することを特徴とする装置。
【発明の詳細な説明】
【０００１】
【産業上の利用分野】
本発明は、一般に、論理回路の試験に係り、特に、２つの論理回路の等価検証において不一致となった場合の原因解析方法に関する。本発明は、例えば、ＬＳＩなどの集積回路のレイアウト設計に好適である。
【０００２】
【従来の技術】
近年の電子機器の高機能化、多機能化の要請から、電子機器に搭載されるＬＳＩなどの集積回路にも高機能化が求められている。ＬＳＩのレイアウト設計など、論理回路の設計においては、まず、シミュレーションによって動作確認され、所期の機能を達成するためのゴールデン又はスペック（Ｓｐｅｃｉｆｉｃａｔｉｏｎ）と呼ばれる回路データを作成する。次いで、ゲート数や遅延時間等に関する様々な制約条件に対応するために、テスト用のスキャン回路、タイミングをとるためのバッファ回路、タイミングクロージャ回路などを挿入することによって、スペックの機能を変えずに組合せ論理回路の構成を修正する。このように実際の回路動作に必要な構成要素を付加してスペックを修正したデータはインプリ（Ｉｍｐｌｅｍｅｎｔａｔｉｏｎ）と呼ばれる。ここで、組合せ論理回路とは、基本的な論理回路素子（論理積、論理和、排他的論理和、否定など）を組合せて構成している回路で、入力が決定されると出力が決定される回路である。入力は、例えば、順序回路から与えられる。ここで、順序回路とは、カウンタやシフトレジスタラッチ等、自分の状態を保持する回路をいう。次いで、スペックの所期の機能が変更されないように、スペックとインプリの論理回路が論理的に等価であるかどうかを検証する必要がある。
【０００３】
等価検証を行う１つの方法として、スペックとインプリに同じ入力パターンを印加して論理シミュレーションを行い、出力が同じ値になるかどうかを調べることが考えられる。しかし、この方法ではすべての入力パターンを試さない限り、等価であることを保証できない。回路の外部入力の数をｎとすると検証に必要な総パターン数は２ｎ　となり、ｎが数十になると、すべてのパターンを尽くしてシミュレーションすることは現実的には不可能である。
【０００４】
そこで、従来は、スペックとインプリの論理回路の等価検証に際して、両者の論理回路図を表示し、組合せ論理回路の一つの出力に影響を与える全ての入力及び論理回路素子によって定義される部分（以下、「論理コーン」と呼ぶ。）をそれぞれの組合せ論理回路において定義し、オペレータが論理回路素子をマニュアルで対応付けるなどすることによって、論理コーン毎に論理回路の等価検証を行っていた。そして、両者が論理的に等価ではないと判断された場合には不一致となった論理コーンの論理式を表示し、かかる論理式から設計者は原因となっている論理回路をマニュアルで特定していた。
【０００５】
【発明が解決しようとする課題】
しかし、インプリを作成する場合に、面積を小さくするための多段化や速度優先等の理由から、スペックの組合せ論理回路構造を変更する場合は少なくない。このため、インプリの論理回路は、スペックに単に新たな論理回路素子を加えた回路ではなく、例えば，４段の素子構造を２段にする等、スペックの論理回路も変更している場合が多い。この結果、対応する論理回路素子を必ずしも簡単に特定することができず、従って回路図や論理式を表示するだけでは、不一致原因となっている論理回路を特定することが困難な場合が多い。特に、近年のＬＳＩの高機能化、多機能化の要請から論理回路の数は増加し、その構成も複雑化してきており、不一致原因となっている論理回路を特定することがますます困難になってきた。このように、従来の論理回路の論理的等価検証は作業性が悪く、時間がかかり、ひいては集積回路の製品化の遅延をもたらしていた。
【０００６】
そこで、本発明では、２つの論理回路が論理的に等価検証を効率的に行い、不一致の場合にその原因となっている論理回路素子の特定を容易にする論理的な等価検証方法及び装置を提供することを例示的な目的とする。
【０００７】
【課題を解決するための手段】
かかる目的を達成するために、本発明の一側面としての論理回路の論理的な等価検証方法は、それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する方法であって、前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換するステップと、前記変換ステップにおいて変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納するステップと、前記変換された論理式の中で指定された項に対応する前記論理回路素子を特定するステップとを有することを特徴とする。かかる方法は、論理式の中で指定された項（例えば、演算子及び変数）に対応する論理回路素子を自動的に特定するので、例えば、ユーザが不一致と判断した項を指定すれば、ユーザは論理コーンのどの論理回路素子が不一致であるかを直ちに知ることができる。前記格納ステップは前記論理式の展開履歴を更に格納してもよい。これにより、前記方法は、論理式を可逆的に、即ち、元に戻すことができるように展開する。なお、前記特定ステップは、前記変換された論理式の中で不一致の項に対応する前記論理回路素子を特定するステップに置換されてもよい。これにより、不一致の判断が自動化され、等価検証の効率性は更に向上する。
【０００８】
上述のいずれかの方法をコンピュータによって実現するためのプログラムも本発明の一側面を構成する。
【０００９】
本発明の別の側面としての論理回路の論理的な等価検証方法は、それぞれ異なる組合せ論理回路を有する２つの論理回路の論理的等価を検証する装置であって、ユーザとの対話に従って、前記２つの論理回路の各々に対して決定された、前記組合せ論理回路の一つの出力に影響を与える全ての入力及び全ての論理回路素子を含む論理コーンを論理式に変換する変換部と、前記変換部において変換された論理式と前記論理コーンに含まれる論理回路素子とを関連付けながら格納する記憶部と、前記論理コーンの構造及び前記論理式を表示すると共に、前記変換された論理式の中で指定された項に対応する前記論理回路素子を前記論理コーンの構造中に表示する表示部と、前記項を指定するための入力部とを有することを特徴とする。かかる装置は、ユーザとの対話形式により等価検証を行い、表示部にユーザが指定した項に対応する論理回路素子を表示する。このため、ユーザは表示部に表示された２つの論理回路間で論理的に等価でない論理回路素子を容易に確認することができる。
【００１０】
本発明の他の目的と更なる特徴は、以下、添付図面を参照して説明される実施例において明らかになるであろう。
【００１１】
【発明の実施形態】
以下、図１を参照して、本発明の一実施形態の等価検証装置１０について説明する。ここで、図１は、等価検証装置１０の原理を説明するための概略ブロック図である。等価検証装置１０は、スペック及びインプリという２つの論理回路の等価検証を行い、本実施形態ではパーソナルコンピュータ（以下、「ＰＣ」という。）として具体化されている。等価検証装置１０は、図１に示すように、制御部１２と、ユーザインターフェース１４と、入力部１６と、表示部１８と、記憶部２０とを有する。
【００１２】
制御部１２は、各部の動作を制御すると共に、等価検証方法において、回路を論理式に変換する変換部や論理式を演算する演算部としても機能する。ユーザインターフェース１４は、キーボードやキーボードやマウスなどのポインティングデバイスから構成された入力部１６からの入力されるユーザからの命令を制御部１２に送信する。ユーザインターフェース１４は、ユーザが制御部１２と対話することを可能にする。ユーザからの命令は、論理式の展開、履歴検索、回路図表示などを含む。表示部１８は、例えば、ＰＣのディスプレイなどである。
【００１３】
記憶部２０は、スペックの論理回路の構造に関する情報を保持するスペック用論理回路データベース２２と、インプリの論理回路の構造に関する情報を保持するインプリ用論理回路データベース２４と、論理式の展開履歴を保持する第１の保持部２６と、スペック及びインプリの回路図と論理式との対応関係を保持する第２の保持部とを有する。第１の保持部は、論理式を戻せるように展開の前後の情報を保持し、第２の保持部は、スペックとインプリのそれぞれに関して、特定の論理式の項と論理回路の論理回路素子との対応関係情報を保持する。本発明は、記憶部２０の情報の一部又は全部が等価検証装置１０にネットワーク接続された別の端末に格納されている場合も含む趣旨であるが、本実施形態では等価検証装置１０に設けられている。
【００１４】
ユーザが等価検証装置１０の入力部１６から等価検証を命令すると、制御部１２はデータベース１２及び１４からスペック及びインプリのデータを抽出して等価検証を行う。かかる等価検証の結果、制御部１２は不一致の組合せ論理回路を抽出し、かかる組合せ回路の中で不一致の論理コーンをそれぞれ抽出し、表示部１８に表示する。これにより、ユーザは、論理コーンに含まれる論理回路素子をＰＣのディスプレイを介して確認することができる。もし、不一致の原因である論理回路素子がこの時点で確認できれば、ユーザは等価検証処理を中止してもよい。論理コーンは、組合せ論理回路の一つの出力に影響を与える全ての入力及び論理回路素子によって定義される部分である。図２に、一例として、２つの論理コーン４及び６を有する組合せ回路２を示す。
【００１５】
ユーザは入力部１６を介して論理式の表示命令を入力することができる。これに応答して、制御部１２はスペック及びインプリのそれぞれの論理コーンを論理式に変換する。制御部１２は、論理式の展開履歴を記憶部２０の第１の保持部に、論理式を元に戻せるように、即ち、可逆的に格納する。この結果、変換後の論理式内の項（後述する演算子及び変数）が最初の論理式のどの項から生成されたものであるかを追跡する履歴情報を付与する。例えば、図２に示す論理コーン４及び６の論理式はそれぞれ以下のようになる。
【００１６】
【数１】
2004021944.tif 000003
【００１７】
【数２】
2004021944.tif 000004
【００１８】
ユーザは必要があれば変換された論理式の展開を入力部１６を介して指示することができる。制御部１２はユーザからの展開指示に応答してスペックとインプリのそれぞれの論理式が比較可能になるまで、本実施形態では和及び積の形式に展開する。ユーザは、一致が明らかで展開不要と判断する論理式については制御部に対して展開を指示しない。このようにして、等価検証装置１０は、スペックと対応するインプリの２つの論理式を同型に近づけ、確実に不一致原因となる論理回路素子を絞り込むことができる。必要があれば、ユーザは、論理式の展開前の形を見たいと希望する場合には、制御部に検索指示を出し、制御部はこれに応答して履歴検索を行う。
【００１９】
一方、制御部１２は、論理式の各項と回路図における論理回路素子とを関連付けて、関連付けた情報を記憶部２０の第２の保持部に格納する。この結果、ユーザは、不一致である論理式の項を発見すると、当該項をクリックすることによって、又は、当該項を入力することによって、制御部１２に論理コーンに含まれる論理回路を表示部１６に表示するように要求する。これに応答して、制御部１２は表示部１６に該当する論理回路素子を、例えば、回路図において色又は太さで強調することによって表示する。これによって、ユーザは不一致の原因である論理回路素子を容易に特定することができる。
【００２０】
以下、第２の保持部が保持する、論理式の内部表現と対応関係データについて説明する。論理式は、演算子及び変数を表すデータ、対応関係データ及び変数名に関する情報を含んでいる。演算子及び変数を表すデータは、演算子の種別、左辺へのポインタ、右辺へのポインタ、及び、対応関係データ先頭を含んでいる。本実施形態では、演算子種別として、０にＡＮＤを、１にＯＲを、２にＮＯＴを、３にＥＯＲを、４にＮＯＰを１０に変数を割り当てられている。対応関係データは、最初の論理式で、各演算子、変数に対して一意となる整数を付ける識別子と、Ｎｅｘｔを含んでいる。図３に、Ａ＋Ｂ＊Ｃという簡単な論理式表現の例を示す。ここで、各演算子および変数名には、一意に識別可能な識別子を割り振っている。
【００２１】
以下、図４乃至図７を参照して、本発明の一実施形態としての等価検証方法について説明する。ここで、図４は、本実施形態の等価検証方法を説明するためのフローチャートである。図５は、スペック６０の論理コーンの回路構成例である。図６は、インプリ７０の論理コーンの回路構成例である。
【００２２】
まず、等価検証方法１０は、図５及び図６に示す不一致と判定されたスペック６０及びインプリ７０の論理コーンを取得する（ステップ１００２）。スペック６０とインプリ７０の論理回路素子をそれぞれＵ１乃至Ｕ９、Ｕ１乃至Ｕ１２とすると、演算子ＯＰと論理回路素子Ｕ１乃至Ｕ９、Ｕ１乃至Ｕ１２はそれぞれ、表１に示すようになる。
【００２３】
【表１】
2004021944.tif 000005
【００２４】
表１においては、スペック６０及びインプリ７０はＳ１から論理回路素子に識別子を割り当てている。スペック６０のｏｐ４やｏｐ５でＵ５が重なっているなど、同じ論理回路素子が登場しているのはＵ５のインバータを考慮しているためである。
【００２５】
次に、スペック６０及びインプリ７０の回路を論理式に変換する（ステップ１００４）。スペック６０の論理式は数式３のようになり、インプリ７０の論理式は数式４のようになる。この過程で、元の回路と論理式との対応表を作成する。
【００２６】
【数３】
2004021944.tif 000006
【００２７】
【数４】
2004021944.tif 000007
【００２８】
次に数式３に示す論理式と数式４に示す論理式を展開又は変換する（ステップ１００６）。数式３に示す論理式を展開又は変換すると以下の数式５のようにする。
【００２９】
【数５】
2004021944.tif 000008
【００３０】
また、数式４に示す論理式を展開又は変換すると以下の数式６のようにする。
【００３１】
【数６】
2004021944.tif 000009
【００３２】
数式５及び６から、（２）項＝（ａ）項、（３）項＝（ｂ）項、（４）項＝（ｅ）項であり、対応データが完全に一致する変数は同色で表示される。これより、残った項である（１）項と（ｃ）項及び（ｄ）項の違いが原因で不一致が発生していることが理解される（数式７参照）。
【００３３】
【数７】
2004021944.tif 000010
【００３４】
スペック６０の論理式変換過程のツリー構造回路図を図７に示す。また、インプリ７０の論理式変換過程のツリー構造回路図を図８に示す。図７及び図８は、明確化のため、本出願にカラー図面として添付する。図７及び図８における処理は、図４において、オペレータからの指示を受け付けて（ステップ１００８）、演算子展開の指示に応じて行われる（ステップ１０１０、１０１２）。論理式の展開においては、等価検証装置１０は展開履歴を作成すると共に論理式と回路図との対応関係を継承する。この結果、オペレータは、後述するように、展開履歴を前方又は後方に検索することもできるし、不一致の原因となっている論理式の項（演算子又は変数）に対応する論理回路素子を回路図に特定することができる。即ち、スペック６０とインプリ７０との間にデータの対応がなく論理式のデータがいずれかに一つだけである場合（ステップ１０１８）、オリジナルの論理式上で当該データに対応する項を強調表示したり、以下に示す図７又は図８の回路図上で強調表示したりすることができる（ステップ１０２０）。データの対応があれば（ステップ１０１８）、一つ前の論理式上で指示された演算子／変数が持つ対応データと一致するものを強調表示することができる（ステップ１０２２）。オペレータは、このように、対応データが存在する論理式の項をチェックすることによって不一致の項を絞り込むことができる。
【００３５】
図７（ａ）は、表１に従ってスペック６０をｏｐ１乃至ｏｐ１７に分解して変数Ｖ１乃至Ｖ１２を割り当てた回路図である。図７（ｂ）は、図７（ａ）に示す▲１▼部と同様であるが、変換対象としてのｏｐ２が強調されている。図７（ｃ）は、図７（ｂ）の回路図をｏｐ２に関して展開した後の回路図である。なお、変更された部分は強調されている。展開では対応したデータの変更はない。
【００３６】
図７（ｄ）は、図７（ａ）に示す▲２▼部と同様であるが、変換対象としてのｏｐ１１及びｏｐ１２が強調されている。図７（ｅ）は、図７（ｄ）に対してｏｐ１１及びｏｐ１２に対して￣（Ｘ＋Ｙ）＝（￣Ｘ）＋（￣Ｙ）を適用して展開した後の回路図である。ｏｐ１１とｏｐ１２からＡＮＤとＮｏｔ（２つ）が作られるので生成された演算子の対応データにはｏｐ１１、ｏｐ１２が格納される。
【００３７】
図７（ｆ）は、図７（ｅ）に対して、ｏｐ１３とその上のＮｏｔ演算及びｏｐ１５とその上のＮｏｔ演算に対して￣（Ｘ＋Ｙ）＝（￣Ｘ）＋（￣Ｙ）を適用して展開した後の回路図である。ｏｐ１１とｏｐ１２のＮｏｔとｏｐ１３から、ＯＲとＮｏｔ（２つ）が作られるので生成された演算子の対応データにはｏｐ１１、ｏｐ１２が格納される。ｏｐ１１とｏｐ１２のＮｏｔとｏｐ１５についても同様である。
【００３８】
図７（ｇ）は、図７（ｆ）に対してｏｐ１２とｏｐ１３のＡＮＤを展開した回路図である。図７（ｈ）は、図７（ｇ）に対してｏｐ１２とｏｐ１３のＡＮＤを展開した回路図である。図７（ｉ）は、図７（ｈ）に対してｏｐ１０を展開した回路図である。図７（ｊ）は局所的最適化（ローカルオプティマイズ）を示す回路図である。図７（ｋ）乃至図７（ｎ）は、それぞれ、数式５の（１）項乃至（４）項に対応する回路図である。
【００３９】
図８（ａ）は、表１に従ってスペック６０をｏｐ１乃至ｏｐ１９に分解して変数Ｖ１乃至Ｖ１５を割り当てた回路図である。図８（ｂ）は、図８（ａ）に示す▲２▼部と同様であるが、展開対象としてのｏｐ１４が強調されている。図８（ｃ）は、図８（ｂ）の回路図をｏｐ１４に関して展開した後の回路図である。図８（ｄ）は、図８（ｃ）の回路図をｏｐ１４に関して展開した後の回路図である。図８（ｅ）は、図８（ｄ）の回路図をｏｐ１３に関して展開した後の回路図である。図８（ｆ）は局所的最適化を示す回路図である。図７（ｇ）乃至図７（ｋ）は、それぞれ、数式６の（ａ）項乃至（ｅ）項に対応する回路図である。
【００４０】
図４において、オペレータからの指示受け付け（ステップ１００８）に応答して指示内容を履歴検索とすれば（ステップ１０１４）、上述したように、オペレータは、スペック又はインプリの論理式を前方又は後方に検索することができる（ステップ１０１６）。
【００４１】
数式６における（ｃ）項のＡ１＊Ｂ１は、最適化前は、Ａ１＊Ｂ１＊Ｂ１である。この最後のＢ１は、Ａ１＊Ｂ１＊（（￣（Ａ０＊Ｂ０））のＢ１と同一である。変形過程の図より、数式７の右辺の２項目のＢ１は、Ｖ９のＢ１であることが分かり、これを（￣Ｂ１）とすることで、右辺の１項目のＡ１＊Ｂ１はＡ１＊Ｂ１＊（￣Ｂ１）＝０になることが容易に分かる。最初の論理式上では次の数式８における下線を引いたＢ１に対応している。
【００４２】
【数８】
2004021944.tif 000011
【００４３】
一方、図４において、指示内容を履歴検索とすれば、近隣の演算子との関係を検索することでＵ９が得られる（ステップ１０１２、１０１４）。Ｕ９は、上述したように、オリジナルの論理式上で強調表示されるか、回路図上で強調表示することができる（ステップ１０２０）。この結果、図９に示すように図６に示すインプリ７０を修正すればよいことが理解される。
【００４４】
以上、本発明の好ましい実施形態を説明したが、本発明はその要旨の範囲内で種々の変形及び変更が可能である。
【００４５】
本出願は更に以下の事項を開示する。
【００４６】
【発明の効果】
以上説明したように本発明によれば、２つの論理回路が論理的に等価検証を効率的に行い、不一致の場合にその原因となっている論理回路素子の特定を容易にする論理的な等価検証方法及び装置を提供する。
【図面の簡単な説明】
【図１】本発明の一実施形態の等価検証装置の概略ブロック図である。
【図２】組合せ論理回路と論理コーンの一例を示す論理回路図である。
【図３】簡単な論理式表現の一例である。
【図４】本実施形態の等価検証方法を説明するためのフローチャートである。
【図５】スペックの論理コーンの回路構成例である。
【図６】インプリの論理コーンの回路構成例である。
【図７】図５に示すスペックの論理式変換過程におけるツリー構造回路図である。
【図８】図６に示すインプリの論理式変換過程におけるツリー構造回路図である。
【図９】スペックの論理コーンと一致するように修正された図６に示すインプリの回路構成例である。
【符号の説明】
１０　　　　　　　　　等価検証装置
１４　　　　　　　　　ユーザインターフェース
１６　　　　　　　　　入力部
１８　　　　　　　　　表示部
２０　　　　　　　　　記憶部
２２　　　　　　　　　スペック用論理回路データベース
２４　　　　　　　　　インプリ用論理回路データベース
２６　　　　　　　　　第１の保持部
２８　　　　　　　　　第２の保持部
【図１】
2004021944.tif 000012
【図２】
2004021944.tif 000013
【図３】
2004021944.tif 000014
【図４】
2004021944.tif 000015
【図５】
2004021944.tif 000016
【図６】
2004021944.tif 000017
【図７】
2004021944.tif 000018
【図８】
2004021944.tif 000019
【図９】
2004021944.tif 000020