JPH113361A - 論理回路検証装置、論理回路検証方法及び論理回路検証プログラムを格納したコンピュータ読み取り可能な記録媒体 - Google Patents

Abstract

(57)【要約】 【課題】 論理回路の等価性を判定するための論理回路
検証装置において、ゲーテッドクロック設計された論理
回路の等価性を正しく判定できるようにする。 【解決手段】 等価性判定回路生成部３は、ドントケア
情報のない論理回路では論理の等価性を判定するための
等価性判定回路を生成し、ドントケア情報のある論理回
路では機能の等価性を判定するための等価性判定回路を
生成する。ゲーテッドクロック部分修正部６は、前記論
理回路がゲーテッドクロック設計されている場合は、そ
の部分の検証が可能となるのように前記生成された等価
性判定回路を修正する。等価性判定部７は、修正された
等価性判定回路に基づいて検証すべき論理回路の等価性
を判定する。

Description

【発明の詳細な説明】

【０００１】

【発明の属する技術分野】本発明は、計算機を利用した
ＬＳＩの論理回路設計の自動化に関し、特に論理回路が
正しく設計されているかどうかを検証することを目的と
した論理回路検証に関するものである。

【０００２】

【従来の技術】ＬＳＩの論理回路設計においては、回路
構造は違うが論理又は機能が同一であるように設計され
た２つの論理回路の論理又は機能の等価性を判定（検
証）する作業がシミュレータを使って行われている。し
かし、シミュレータを使った場合、入力パターンの０、
１の組合せは２ⁿ（ｎは入力数）通りとなるため、入力
数が多くなると計算に時間がかかるという問題があっ
た。

【０００３】そこで、２つの論理回路の論理又は機能の
等価性を判定するためのツールとして論理回路検証装置
が利用されている。図１３は、従来の論理回路検証装置
で生成される論理等価性判定回路の一例を示す回路構成
図である。論理回路検証装置は、検証すべき２つの論理
回路を入力して、図１３のような等価性判定回路を生成
し、入力Ｉ１及びＩ２に０、１の組合せパターンを与え
たときに、出力ｏｕｔ＿ｃｈｅｃｋの値が常に１となる
かどうかにより、検証対象となる回路１１及び回路１２
が論理的に等価であるかどうかの判定を行う。ここで、
出力が常に１となるかどうかの判定は、論理回路の機能
を論理関数に変換して行っている。この表現形式には、
後述するＢＤＤ（Binary Decision Diagram)と呼ばれる
グラフ関数（論理構造が異なっても論理的に等価であれ
ば同一の表現形式となる）が一般的に利用されている。

【０００４】このような論理関数による判定において、
ドントケア条件が出力端子及びレジスタ入力に定義され
ている場合に、機能的に等価であるかどうかの判定は次
のように行なう。例えば、図１３において、回路１１の
出力端子ｏｕｔ１をｏｕｔ１１、回路１２の出力端子ｏ
ｕｔ１をｏｕｔ１２として、出力端子ｏｕｔ１における
ドントケア関数をｄｃ＿ｏｕｔ１とする。ここで（ｏｕ
ｔ１１ ｅｘ−ｎｏｒｏｕｔ１２）ｏｒ ｄｃ＿ｏｕｔ
１が常に１であるかどうかをチェックすることで論理又
は機能の等価性を判定することができる。

【０００５】ドントケア条件とは、論理回路の出力端子
及びレジスタに与えられる値がどのような値であって
も、演算結果に関与しない場合を論理式又は論理回路で
表現したものである。例えば、図１４（ａ）に示すよう
に、レジスタ（Ｒｅｇ）１及び２の出力（データ１、デ
ータ２）をＡＬＵ（演算ユニット）３で演算してレジス
タ４に出力するような回路で説明する。図において、Ａ
ＬＵ３への制御信号Ｉ０、Ｉ１が同図（ｂ）のように与
えられているとすると、Ｉ０、Ｉ１が（０、０）又は
（０、１）の場合はＡＬＵ３ではレジスタ１及び２から
のデータに対して＋又は−の演算が行われるが、Ｉ０、
Ｉ１が（１、０）の場合はデータ１がシフトされ、デー
タ２は使われない。また、Ｉ０、Ｉ１が（１、１）の場
合はデータ１、２共に使われない。このＩ０、Ｉ１が
（１、０）及び（１、１）のときに、データ２はドント
ケア、すなわちデータが参照されない状態となる。この
ように入力値の組合せがドントケアである場合には、レ
ジスタの出力が一致しなくても、等価であるとみなすよ
うにしている。すなわち、ドントケア条件が定義されて
いる場合は、論理的に等価であるかではなく、機能的に
等価であるかどうかが判定される。

【０００６】

【発明が解決しようとする課題】上述した論理回路検証
装置は、ゲーテッドクロック設計された論理回路の等価
性を判定する場合にも利用されている。図１５は、ある
部分回路をゲーテッドクロック設計した場合の一例を示
したもので、同図（ａ）はゲーテッドクロック設計され
ていない部分回路を、同図（ｂ）はゲーテッドクロック
設計された部分回路をそれぞれ示している。図１５
（ａ）の部分回路では、レジスタ（Ｒｅｇ）１３のクロ
ック入力ポート（ＣＫ）から入力されるクロック信号
（ｃｌｋ）の立ち上がりでデータ（Ｄ）を取り込む。こ
こで、データＤはマルチプレクサ（ＭＵＸ）１４に入力
されるイネーブル論理出力ｅｎａにより制御され、ｅｎ
ａ＊ｄａｔａ＋ｅｎａ(ＮＯＴ）＊ｏｕｔに従って与え
られる。すなわち、ｅｎａが１のときはｄａｔａがＤポ
ートに入力され、ｅｎａが０のときはレジスタ１３から
のフィードバックがＤポートに入力される。

【０００７】一方、図１５（ｂ）の部分回路において、
データＤはＡＮＤゲート１５に入力されるイネーブル論
理出力ｅｎａにより制御され、ｅｎａ＊ｃｌｋが成立す
るタイミングでレジスタ１３に取り込まれる。

【０００８】ゲーテッドクロック設計では、図１５に示
すようにレジスタ１３のクロック入力ポート（ＣＫ）に
対して論理回路を付加するもので、図１５に示す２つの
部分回路は機能的に等価である。しかし、従来の論理回
路検証装置ではこの２つの部分回路の論理又は機能的な
等価性は判断できないため、等価でないと判定されてい
た。

【０００９】本発明は、上記課題を解決するためになさ
れたもので、ゲーテッドクロック設計された論理回路の
論理又は機能的な等価性を正しく判定することができる
論理回路検証装置、論理回路検証方法及び論理回路検証
プログラムを格納したコンピュータ読み取り可能な記録
媒体を提供することを目的とする。

【００１０】

【課題を解決するための手段】上記目的を達成するた
め、請求項１の発明は、検証すべき少なくとも２つの論
理回路に関する情報及び該論理回路に関するドントケア
情報を入力する回路情報入力手段と、前記論理回路に関
する情報と該論理回路に関するドントケア情報に基づい
て、前記少なくとも２つの論理回路を含む等価性判定回
路を生成する等価性判定回路生成手段と、前記等価性判
定回路に含まれる論理回路がゲーテッドクロック設計さ
れている場合は、前記少なくとも２つの論理回路に含ま
れるレジスタのクロック入力が等しくなるように、前記
等価性判定回路を修正するゲーテッドクロック部分修正
手段と、前記等価性判定回路生成手段で生成された等価
性判定回路又は前記ゲーテッドクロック部分修正手段で
修正された等価性判定回路に基づいて、検証すべき少な
くとも２つの論理回路の論理又は機能の等価性を判定す
る等価性判定手段とを備えたことを特徴とする。

【００１１】なお、上記等価性判定回路生成手段及びゲ
ーテッドクロック部分修正手段は、以下のような構成と
することができる。

【００１２】等価性判定回路生成手段は、等価性判定回
路を生成する際に、検証すべき論理回路に関するドント
ケア情報が無い場合は、論理の等価性を判定するための
等価性判定回路を生成し、検証すべき論理回路に関する
ドントケア情報が有る場合は、機能の等価性を判定する
ための等価性判定回路を生成する。

【００１３】ゲーテッドクロック部分修正手段は、等価
性判定回路を修正する際に、修正すべき論理回路のレジ
スタに対してデータロードとデータ保持の選択を行なう
マルチプレクサを生成し、該マルチプレクサの選択論理
にクロックイネーブル論理を使用するように回路を変更
する。

【００１４】また、ゲーテッドクロック部分修正手段
は、回路を変更する際に、ゲーテッドクロック設計に関
する付加情報を参照して回路を変更する。

【００１５】また、上記目的を達成するため、請求項２
の発明は、少なくとも２つの論理回路の論理又は機能の
等価性を判定する論理回路検証方法において、検証すべ
き論理回路と該論理回路に関するドントケア情報の有無
に従って等価性判定回路を生成し、該生成された等価性
判定回路のゲーテッドクロック設計された部分を等価性
の検証が可能となるように修正し、前記等価性判定回路
に基づいて検証すべき論理回路の論理又は機能の等価性
を判定することを特徴とする。

【００１６】請求項３の発明は、検証すべき少なくとも
２つの論理回路に関する情報及び該論理回路に関するド
ントケア情報を入力する回路情報入力ステップと、前記
論理回路に関する情報と該論理回路に関するドントケア
情報に基づいて、前記少なくとも２つの論理回路を含む
等価性判定回路を生成する等価性判定回路生成ステップ
と、前記等価性判定回路に含まれる論理回路がゲーテッ
ドクロック設計されている場合は、前記少なくとも２つ
の論理回路に含まれるレジスタのクロック入力が等しく
なるように、前記等価性判定回路を修正するゲーテッド
クロック部分修正ステップと、前記等価性判定回路生成
ステップで生成された等価性判定回路又は前記ゲーテッ
ドクロック部分修正ステップで修正された等価性判定回
路に基づいて、検証すべき少なくとも２つの論理回路の
論理又は機能の等価性を判定する等価性判定ステップと
を含むことを特徴とする。

【００１７】なお、上記等価性判定回路生成ステップ及
びゲーテッドクロック部分修正ステップは、以下のよう
な処理を含むことができる。

【００１８】等価性判定回路生成ステップは、等価性判
定回路生成する際に、検証すべき論理回路に関するドン
トケア情報が無い場合は、論理の等価性を判定するため
の等価性判定回路を生成し、検証すべき論理回路に関す
るドントケア情報が有る場合は、機能の等価性を判定す
るための等価性判定回路を生成する。

【００１９】ゲーテッドクロック部分修正ステップは、
等価性判定回路を修正する際に、修正すべき論理回路の
レジスタに対してデータロードとデータ保持の選択を行
なうマルチプレクサを生成し、該マルチプレクサの選択
論理にクロックイネーブル論理を使用するように回路を
変更する。

【００２０】また、ゲーテッドクロック部分修正ステッ
プは、回路を変更する際に、ゲーテッドクロック設計に
関する付加情報を参照して回路を変更する。

【００２１】さらに、上記目的を達成するため、請求項
４の発明は、検証すべき論理回路と該論理回路に関する
ドントケア情報の有無に従って等価性判定回路を生成す
る処理と、該生成された等価性判定回路のゲーテッドク
ロック設計されている部分を等価性の検証が可能となる
ように修正する処理と、前記等価性判定回路に基づいて
検証すべき論理回路の論理又は機能の等価性を判定する
処理とを含み、これら処理をコンピュータに実行させる
ことを特徴とする。

【００２２】請求項５の発明は、検証すべき少なくとも
２つの論理回路に関する情報及び該論理回路に関するド
ントケア情報を入力する回路情報入力ステップと、前記
論理回路に関する情報と該論理回路に関するドントケア
情報に基づいて、前記少なくとも２つの論理回路を含む
等価性判定回路を生成する等価性判定回路生成ステップ
と、前記等価性判定回路に含まれる論理回路がゲーテッ
ドクロック設計されている場合は、前記少なくとも２つ
の論理回路に含まれるレジスタのクロック入力が等しく
なるように、前記等価性判定回路を修正するゲーテッド
クロック部分修正ステップと、前記等価性判定回路生成
ステップで生成された等価性判定回路又は前記ゲーテッ
ドクロック部分修正ステップで修正された等価性判定回
路に基づいて、検証すべき少なくとも２つの論理回路の
論理又は機能の等価性を判定する等価性判定ステップと
を含み、これらステップをコンピュータに実行させるこ
とを特徴とする。

【００２３】なお、上記等価性判定回路生成ステップ及
びゲーテッドクロック部分修正ステップは、以下のよう
な処理を含むことができる。

【００２４】等価性判定回路生成ステップは、検証すべ
き論理回路に関するドントケア情報の有無を判定する処
理と、前記検証すべき論理回路に関するドントケア情報
が無いと判定された場合は、論理の等価性を判定するた
めの等価性判定回路を生成する処理と、前記検証すべき
論理回路に関するドントケア情報が有ると判定された場
合は、機能の等価性を判定するための等価性判定回路を
生成する処理。

【００２５】ゲーテッドクロック部分修正ステップは、
修正すべき論理回路のレジスタに対してデータロードと
データ保持の選択を行なうマルチプレクサを生成する処
理と、該マルチプレクサの選択論理にクロックイネーブ
ル論理を使用するように回路を変更する処理。

【００２６】また、ゲーテッドクロック部分修正ステッ
プは、ゲーテッドクロック設計に関する付加情報を参照
して回路を変更する処理。

【００２７】

【発明の実施の形態】以下、この発明に係わる論理回路
検証装置、論理回路検証方法及び論理回路検証プログラ
ムを格納したコンピュータ読み取り可能な記録媒体の一
実施形態について説明する。

【００２８】図１は、本実施形態に係わる論理回路検証
装置の機能的な構成を示したブロック図である。この論
理回路検証装置１０は、回路情報入力部１、ドントケア
情報入力部２、等価性判定回路生成部３、等価性判定回
路格納部４、ゲーテッドクロック情報入力部５、ゲーテ
ッドクロック部分修正部６、等価性判定部７から構成さ
れている。

【００２９】回路情報入力部１は、論理又は機能的に等
価であることを検証したい２つの論理回路に関する情報
を入力し、等価性判定回路生成部３へ受け渡す。

【００３０】ドントケア情報入力部２は、前記回路情報
入力部１から入力された２つの論理回路に関するドント
ケア情報を入力し、等価性判定回路生成部３へ受け渡
す。

【００３１】等価性判定回路生成部３は、入力された２
つの論理回路に関するドントケア情報の有無を判定し、
ドントケア情報が無い場合は、前記２つの論理回路に関
する情報に基づいて論理の等価性を判定するための等価
性判定回路を生成する。また、ドントケア情報が有る場
合は、前記２つの論理回路に関する情報と、これら論理
回路に関するドントケア情報に基づいて機能の等価性を
判定するための等価性判定回路を生成する。

【００３２】等価性判定回路格納部４は、前記等価性判
定回路生成部３で生成された等価性判定回路の回路デー
タ、及び後述するゲーテッドクロック部分修正部５で修
正がなされた等価性判定回路の回路データを格納する。

【００３３】ゲーテッドクロック情報入力部５は、ゲー
テッドクロック設計に関する付加情報を入力し、ゲーテ
ッドクロック部分修正部６に受け渡す。ゲーテッドクロ
ック設計に関する付加情報とは、ゲーテッドクロック設
計されている場合に、そのゲーテッドクロックされた部
分に特徴的な構成に関する情報であり、後にゲーテッド
クロック設計された部分を修正する際に、必要に応じて
参照される。

【００３４】例えば、後述の実施形態２においては、ゲ
ーテッドクロック設計によって付加されたフリップフロ
ップがクロックイネーブル論理におけるグリッジを除去
するために挿入されたものであるという情報がゲーテッ
ドクロック設計に関する付加情報として入力されてお
り、ゲーテッドクロック部分修正部６では、ゲーテッド
クロック設計された部分を修正する際に、この情報に基
づいて前記フリップフロップを等価性判定に関係ない部
分として除去している。

【００３５】ゲーテッドクロック部分修正部６は、前記
等価性判定回路生成部３で生成された等価性判定回路に
含まれる部分回路（論理回路）がゲーテッドクロック設
計されているかどうかを、レジスタのＣＫポート入力に
ＡＮＤやＯＲなどのゲートがあるかどうかにより判定す
る。そして、ゲーテッドクロック設計されている場合
は、必要に応じてゲーテッドクロック設計に関する付加
情報を参照しながら、前記２つの論理回路のレジスタの
クロック入力が等しくなるように、前記生成された等価
性判定回路のゲーテッドクロック設計された部分を修正
する。

【００３６】ここでは、ゲーテッドクロック設計された
部分を修正するため、修正すべき論理回路のレジスタに
対してデータロードとデータ保持の選択を行なうマルチ
プレクサを生成するとともに、このマルチプレクサの選
択論理にクロックイネーブル論理を使用するように回路
を変更するようにしている。修正された等価性判定回路
は、等価性判定回路格納部４に格納される。

【００３７】等価性判定部７は、前記等価性判定回路生
成部３で生成された等価性判定回路又は前記ゲーテッド
クロック部分修正部６で修正された等価性判定回路に基
づいて、検証すべき少なくとも２つの論理回路の論理又
は機能の等価性を判定する。

【００３８】上記各部からなる論理回路検証装置１０
は、キーボード、マウス、ライトペン、又はフレキシブ
ルディスク装置などの入力装置、ＣＰＵ、及びこのＣＰ
Ｕに接続されたＲＯＭ，ＲＡＭ、磁気ディスクなどの記
憶装置、ディスプレイ装置やプリンタ装置などの出力装
置を含む通常のコンピュータシステムにより構成され
る。

【００３９】次に、上述のように構成された論理回路検
証装置１０において、検証すべき論理回路の論理又は機
能の等価性を判定する場合の処理手順を図２のフローチ
ャートにより説明する。

【００４０】まず、回路情報入力部１から検証すべき２
つの論理回路に関する情報を入力し（ステップ１０
１）、続いてドントケア情報入力部２から前記２つの論
理回路に関するドントケア情報を入力する（ステップ１
０２）。なお、この時に、必要に応じてゲーテッドクロ
ック情報入力部５から前記論理回路のゲーテッドクロッ
ク設計に関する付加情報を入力する。次に、等価性判定
回路生成部３は、入力された２つの論理回路に関するド
ントケア情報があるかどうかを判定する（ステップ１０
３）。ここで、ドントケア情報がない場合は、前記２つ
の論理回路に関する情報に基づいて、例えば図３に示す
ような論理の等価性を判定するための等価性判定回路を
生成する（ステップ１０４）。また、ドントケア情報が
ある場合は、前記２つの論理回路に関するドントケア情
報と、これら論理回路に関するドントケア情報に基づい
て、例えば図４に示すような機能の等価性を判定するた
めの等価性判定回路を生成する（ステップ１０５）。な
お、図４において、ｄｃ＿ｏｌ等の符号は出力またはレ
ジスタのドントケア関数を表わしている。上記ステップ
１０４又はステップ１０５で生成された等価性判定回路
の回路データは等価性判定回路格納部４へ格納される。

【００４１】次に、ゲーテッドクロック部分修正部６
は、前記生成された等価性判定回路がゲーテッドクロッ
ク設計されているかどうかを判定する（ステップ１０
６）。ここで、ゲーテッドクロック設計されている場合
は、必要に応じてゲーテッドクロック設計に関する付加
情報を参照して、前記等価性判定回路のうちゲーテッド
クロック設計された部分の回路を修正する。

【００４２】まず、等価性判定回路格納部４に格納され
ている等価性判定回路について、ゲーテッドクロック設
計された部分のイネーブル信号を取り出し（ステップ１
０７）、このイネーブル信号を制御信号としたマルチプ
レクサをレジスタのデータ入力部分に生成するととも
に、このマルチプレクサの選択論理にクロックイネーブ
ル論理を使用するように回路を変更し、さらにゲーテッ
ドクロック部分を除去する（ステップ１０８）。次に、
ゲーテッドクロック情報に基づいて、等価性判定に関係
しない回路部分を除去する（ステップ１０９）。このス
テップ１０７〜ステップ１０９で修正された等価性判定
回路の回路データは等価性判定回路格納部４に格納され
る。

【００４３】次に、等価性判定部７は、等価性判定回路
格納部４に格納されている等価性判定回路、すなわち前
記等価性判定回路生成部３で生成された等価性判定回
路、又は前記ゲーテッドクロック部分修正部６で修正さ
れた等価性判定回路に基づいて、検証すべき少なくとも
２つの論理回路の論理又は機能の等価性を判定する（ス
テップ１１０）。

【００４４】なお、判定結果は、図示しないディスプレ
イ装置上に、等価である又は等価でないというメッセー
ジを表示したり、プリンタ装置により同様のメッセージ
をプリント出力することにより行う。ここで、等価でな
いという判定がなされたときには、上記メッセージに加
えて、出力結果がともに１にならない入力の組合せを表
示又はプリント出力するようにしてもよい。この場合、
設計者は出力結果がともに１にならない入力の組合せに
基づいて論理回路の論理を検討することにより、元の論
理回路の設計変更を容易に行うことができる。

【００４５】次に、上述した論理回路検証装置１０にお
いて、論理回路の等価性を判定する場合の具体例を実施
形態１、実施形態２として説明する。なお、実施形態１
は検証すべき論理回路に関するドントケア情報が無い場
合、実施形態２はドントケア情報が有る場合の例を示
す。

【００４６】［実施形態１]まず、図５（ａ）、（ｂ）
に示すような２つの論理回路回路１及び回路２が回路情
報入力部１から入力されたとする。図５（ａ）はゲーテ
ッドクロック設計されておらず、同図（ｂ）はゲーテッ
ドクロック設計されている。この例では、入力された回
路にドントケア情報は無いので、等価性判定回路生成部
３は、図６に示すような論理の等価性を判定するための
等価性判定回路を生成して等価性判定回路格納部４に格
納する。なお、図６において、部分回路２０１は図５
（ａ）に、部分回路２０２は図５（ｂ）にそれぞれ対応
している。

【００４７】図６の部分回路２０１ではＤタイプフリッ
プフロップＦＦ１のＱポート出力をＦＦ１＿Ｑとしたと
き、ＦＦ１のＤポート入力ＦＦ１＿Ｄの論理はブール式
で＾Ｉ２＊ＦＦ１＿Ｑ＋Ｉ２＊Ｉ１と表わせる。ここ
で、＊は論理積、＋は論理和、＾は否定論理を表わす。
また、図６の部分回路２０２では、ＦＦ１のＤポートＦ
Ｆ１＿Ｄの論理は＾Ｉ１＊Ｉ２と表わせて、図６の部分
回路２０１とは異なる。一方、出力端子Ｏ１では図４の
部分回路２０１、部分回路２０２とも論理はＩ３＊ＦＦ
１＿Ｑと表わせて同じ論理となる。図６の回路では、Ｆ
Ｆ１のＤポート入力の論理が異なるので、結果として図
６におけるｏｕｔ＿ｃｈｅｃｋは常に１とはならず、こ
のままの等価性判定回路では等価でないと判定されてし
まう。

【００４８】そこで、ゲーテッドクロック部分修正部６
は、図６の等価性判定回路に対して２つのフリップフロ
ップＦＦ１のＣＫポート入力が同じ信号となるように修
正を行う。この修正は次のように行なわれる。すなわち
図６の部分回路２０１ではＦＦ１のＣＫポート入力の論
理はＣＬＫであり、部分回路２０２ではＦＦ１のＣＫポ
ート入力の論理はＣＬＫ＋＾Ｉ２なので、両方のＣＫポ
ート入力の論理をＣＬＫとするような回路変更を行な
う。

【００４９】まず、図６の部分回路２０１ではすでにＣ
ＬＫとなっているので、操作は行なわない。一方、図６
の部分回路２０２では、＾Ｉ２が１のとき、すなわちＩ
２が０のときにＦＦ１のポートにクロックが供給されな
い。すなわち、Ｉ２が０でないときはＦＦ１の値が保持
される。このため、図６の部分回路２０２におけるＦＦ
１のＣＫポート入力の論理をＣＬＫとするためには、Ｉ
２が０のときはＦＦ１の値が保持される論理を付加すれ
ば良い。この例では、ＦＦ１に対してデータロードとデ
ータ保持の選択を行うＭＵＸ５１をＦＦ１のＤポート入
力に接続し、このＭＵＸ５１の選択論理にクロックイネ
ーブル論理を与えるように回路を修正している。このよ
うな修正を行なった結果、図７に示すような等価性判定
回路が生成される。なお、図７における回路要素ＭＵＸ
５１は、例えば図８に示すような論理回路により構成す
ることができる。

【００５０】前記修正により等価性判定回路格納部４に
格納された図７の等価性判定回路は等価性判定部７にお
いて等価性が判定される。図７の回路について見てみる
と、出力端子Ｏ１では部分回路２０３、部分回路２０４
ともに論理はＩ３＊ＦＦ１＿Ｑと表せて同じ論理とな
る。また、ＦＦ１のＤポート入力ＦＦ１＿Ｄの論理につ
いても、部分回路２０３、部分回路２０４ともにＢＤＤ
を用いて表現すると図９（ａ）のように同じ形式で表わ
され、同じ論理であることがわかる。

【００５１】すなわち図９（ａ）において、ＦＦ１＿Ｄ
のＩ２に０を代入すると（０の破線矢印）、ＦＦ１＿Ｑ
が残り、ここでＦＦ１＿Ｑが０であれば（０の破線矢
印）、出力は０となる。また、ＦＦ１＿Ｑが１であれば
（１の実線矢印）、出力は１となる。また、ＦＦ１＿Ｄ
のＩ１に０を代入すると（１の実線矢印）、Ｉ１が残
り、ここでＩ１が０であれば（０の破線矢印）、出力は
０となる。また、Ｉ１が１であれば（１の実線矢印）、
出力は１となる。前記部分回路２０３、部分回路２０４
ともに、Ｉ１、Ｉ２に同じ組合せの０、１を入力した場
合には、同じ経路の矢印方向へ進み、ＦＦ１のＤポート
入力ＦＦ１＿Ｄは同じ出力結果となる。したがって、図
７におけるｏｕｔ＿ｃｈｅｃｋの論理を表わすＢＤＤ
は、図９（ｂ）のように常に１となる。このため、等価
性判定部６では図５（ａ）の論理回路と（ｂ）の論理回
路は等価であると判断される。

【００５２】［実施形態２］次に、別の実施形態を示し
て説明する。まず図１０に示すような２つの論理回路が
回路情報入力部１から入力されたとする。図１０（ａ）
ではゲーテッドクロック設計されておらず、同図（ｂ）
ではゲーテッドクロック設計されている。この例では、
フリップフロップＦＦ１に対するドントケア関数として
Ｂが、また出力端子Ｏ１に対するドントケア関数として
＾Ｉ２がドントケア情報入力部２より入力されたとす
る。

【００５３】次に、等価性判定回路生成部３では、ドン
トケア情報を考慮して図１１に示すような機能の等価性
を判定する等価性判定回路を生成して等価性判定回路格
納部４に格納する。図１１ではドントケア情報を考慮し
ても、ＦＦ１のＤポート入力の機能が部分回路２０５と
部分回路２０６では異なり、ｏｕｔ＿ｃｈｅｃｋは常に
１とはならずに、このままの等価性判定回路では等価で
ないと判定されてしまう。

【００５４】そこで、ゲーテッドクロック部分修正部６
は、図１１の等価性判定回路に対して２つのフリップフ
ロップＦＦ１のＣＫポート入力が同じ信号となるように
修正を行なう。ここで、ゲーテッドクロック情報入力部
５より、フリップフロップＥＮＡ＿ＦＦはクロックイネ
ーブル論理におけるグリッジを除去するために挿入され
たフリップフロップであるという情報が入力されたとす
る。ゲーテッドクロック部分修正部６ではＥＮＡ＿ＦＦ
のＤポート入力の論理がクロックイネーブル論理である
と認識する。図１１の部分回路２０６では、ＥＮＡ＿Ｆ
ＦのＱポート出力が０のときにＦＦ１のＣＫポートにク
ロックが供給されない。これは上記のように認識された
イネーブル論理が０の場合、すなわち論理式＾Ａ＋Ｂが
１のときにＦＦ１の値が保持される。このため、図１１
の部分回路２０６において、＾Ａ＋Ｂが１のときにＦＦ
１の値が保持される論理を付加する。この例では、ＥＮ
Ａ＿ＦＦを削除し、ＦＦ１に対してデータロードとデー
タ保持の選択を行うＭＵＸ６１をＦＦ１のＤポート入力
に接続して、このＭＵＸ６１の選択論理にクロックイネ
ーブル論理を与えるように回路を修正している。このよ
うな修正を行なった結果、図１２に示すような等価性判
定回路が生成される。一方、図１１の部分回路２０５で
はＦＦ１のＣＫポート入力がＣＬＫなので、論理の付加
は行なわれない。この修正により等価性判定回路格納部
４に生成された図１２に示す等価性判定回路は、等価性
判定部６において等価性を判定される。この結果、図１
２におけるｏｕｔ＿ｃｈｅｃｋの論理を表わすＢＤＤは
図９（ｂ）のようになり、常に１であることがわかるた
め、等価性判定部７では図１０（ａ）の論理回路と図１
０（ｂ）の論理回路は等価であると判定される。

【００５５】上述したように、ゲーテッドクロック設計
はレジスタのクロック入力ポート（ＣＫ）に対して論理
回路を付加するものであるため、２つの部分回路は機能
的には等価であっても、従来の論理回路検証装置ではこ
の２つの部分回路の論理または機能的等価性が判断でき
ず、等価でないと判定されていた。しかし、本実施形態
の論理回路検証装置によれば、２つの論理回路のレジス
タのクロック入力が等しくなるように回路を修正するこ
とにより、ゲーテッドクロック設計された部分の検証が
可能となるため、従来装置では正しい検証を行うことが
できなかったゲーテッドクロック設計された論理回路の
論理又は機能的な等価性の検証が可能となる。

【００５６】なお、上記実施形態では、Ｉ１、Ｉ２を１
ビットとして説明しているが、３２ビット又は６４ビッ
トの場合であっても適用することができる。とくに、入
力のビット数が多くなった場合には、シミュレータを使
った場合に比べて計算時間を大幅に短縮することが可能
となる。

【００５７】また、上記実施形態では、論理回路の論理
又は機能的な等価性を２つの回路について検証している
が、等価性の検証は複数の論理回路について実施するこ
ともできる。さらに、上記実施形態では、検証すべき論
理回路としてフリップフロップにより構成されたレジス
タ回路を例として示したが、同期型メモリ（同期型ＲＡ
Ｍ）のようにクロックに同期してデータの書き込みを行
うようなメモリセルにより構成したレジスタ回路にも適
用することができる。

【００５８】上述した論理回路検証装置の動作を実現す
るためのプログラムはコンピュータにより読みとり可能
な記録媒体に保存することができる。この記録媒体をコ
ンピュータシステムにより読み込ませ、前記プログラム
を実行してコンピュータを制御することにより、上述し
た論理回路検証装置による処理を実現することができ
る。ここで、前記記録媒体とは、例えばメモリ装置、磁
気ディスク装置、光ディスク装置などのプログラムを記
録できるようなすべての記録装置が含まれる。

【００５９】

【発明の効果】以上説明したように、この発明に係わる
論理回路検証装置、論理回路検証方法及び論理回路検証
プログラムを格納したコンピュータ読み取り可能な記録
媒体によれば、生成した等価性判定回路のゲーテッドク
ロック設計された部分の検証が可能となるように回路を
修正するようにしたので、従来装置では正しい検証を行
うことができなかったゲーテッドクロック設計された論
理回路の論理又は機能的な等価性の検証が可能となる。

【図面の簡単な説明】

【図１】実施形態に係わる論理回路検証装置の機能的な
構成を示したブロック図。

【図２】論理回路検証装置において論理回路の論理又は
機能の等価性を判定する場合の処理手順を示すフローチ
ャート。

【図３】等価性判定回路生成部により生成される論理の
等価性を判定するための等価性判定回路の一例を示す回
路構成図。

【図４】等価性判定回路生成部により生成される機能の
等価性を判定するための等価性判定回路の一例を示す回
路構成図。

【図５】（ａ）及び（ｂ）は実施形態１で回路情報入力
部から入力された論理回路を示す回路構成図。

【図６】実施形態１の等価性判定回路生成部により生成
される論理の等価性を判定するための等価性判定回路を
示す回路構成図。

【図７】実施形態１の等価性判定回路生成部により生成
される論理の等価性を判定するための等価性判定回路を
示す回路構成図。

【図８】ＭＵＸの論理構造図。

【図９】（ａ）及び（ｂ）は等価性判定部で生成された
ＢＤＤの一例を示す説明図。

【図１０】（ａ）及び（ｂ）は実施形態２で回路情報入
力部から入力された論理回路を示す回路構成図。

【図１１】実施形態２の等価性判定回路生成部により生
成される論理の等価性を判定するための等価性判定回路
を示す回路構成図。

【図１２】実施形態２の等価性判定回路生成部により生
成される機能の等価性を判定するための等価性判定回路
を示す回路構成図。

【図１３】従来の論理回路検証装置で生成される論理等
価性判定回路の一例を示す回路構成図。

【図１４】（ａ）はドントケア条件を説明するための論
理回路図、（ｂ）は制御信号とＡＬＵの機能との関係を
示す説明図。

【図１５】（ａ）はゲーテッドクロック設計されていな
い部分回路を示す回路構成図、（ｂ）はゲーテッドクロ
ック設計された部分回路を示す回路構成図。

【符号の説明】

１ 回路情報入力部 ２ ドントケア情報入力部 ３ 等価性判定回路生成部 ４ 等価性判定回路格納部 ５ ゲーテッドクロック設計対応部 ６ 等価性判定部 ７ ゲーテッドクロック情報入力部

Claims (5)

【特許請求の範囲】
1. 【請求項１】 検証すべき少なくとも２つの論理回路に
   関する情報及び該論理回路に関するドントケア情報を入
   力する回路情報入力手段と、 前記論理回路に関する情報と該論理回路に関するドント
   ケア情報に基づいて、前記少なくとも２つの論理回路を
   含む等価性判定回路を生成する等価性判定回路生成手段
   と、 前記等価性判定回路に含まれる論理回路がゲーテッドク
   ロック設計されている場合は、前記少なくとも２つの論
   理回路に含まれるレジスタのクロック入力が等しくなる
   ように、前記等価性判定回路を修正するゲーテッドクロ
   ック部分修正手段と、 前記等価性判定回路生成手段で生成された等価性判定回
   路又は前記ゲーテッドクロック部分修正手段で修正され
   た等価性判定回路に基づいて、検証すべき少なくとも２
   つの論理回路の論理又は機能の等価性を判定する等価性
   判定手段とを備えたことを特徴とする論理回路検証装
   置。
2. 【請求項２】 少なくとも２つの論理回路の論理又は機
   能の等価性を判定する論理回路検証方法において、 検証すべき論理回路と該論理回路に関するドントケア情
   報の有無に従って等価性判定回路を生成し、 該生成された等価性判定回路のゲーテッドクロック設計
   された部分を等価性の検証が可能となるように修正し、 前記等価性判定回路に基づいて検証すべき論理回路の論
   理又は機能の等価性を判定することを特徴とする論理回
   路検証方法。
3. 【請求項３】 検証すべき少なくとも２つの論理回路に
   関する情報及び該論理回路に関するドントケア情報を入
   力する回路情報入力ステップと、 前記論理回路に関する情報と該論理回路に関するドント
   ケア情報に基づいて、前記少なくとも２つの論理回路を
   含む等価性判定回路を生成する等価性判定回路生成ステ
   ップと、 前記等価性判定回路に含まれる論理回路がゲーテッドク
   ロック設計されている場合は、前記少なくとも２つの論
   理回路に含まれるレジスタのクロック入力が等しくなる
   ように、前記等価性判定回路を修正するゲーテッドクロ
   ック部分修正ステップと、 前記等価性判定回路生成ステップで生成された等価性判
   定回路又は前記ゲーテッドクロック部分修正ステップで
   修正された等価性判定回路に基づいて、検証すべき少な
   くとも２つの論理回路の論理又は機能の等価性を判定す
   る等価性判定ステップとを含むことを特徴とする論理回
   路検証方法。
4. 【請求項４】 検証すべき論理回路と該論理回路に関す
   るドントケア情報の有無に従って等価性判定回路を生成
   する処理と、 該生成された等価性判定回路のゲーテッドクロック設計
   されている部分を等価性の検証が可能となるように修正
   する処理と、 前記等価性判定回路に基づいて検証すべき論理回路の論
   理又は機能の等価性を判定する処理とを含み、これら処
   理をコンピュータに実行させることを特徴とする論理回
   路検証プログラムを格納したコンピュータ読み取り可能
   な記録媒体。
5. 【請求項５】 検証すべき少なくとも２つの論理回路に
   関する情報及び該論理回路に関するドントケア情報を入
   力する回路情報入力ステップと、 前記論理回路に関する情報と該論理回路に関するドント
   ケア情報に基づいて、前記少なくとも２つの論理回路を
   含む等価性判定回路を生成する等価性判定回路生成ステ
   ップと、 前記等価性判定回路に含まれる論理回路がゲーテッドク
   ロック設計されている場合は、前記少なくとも２つの論
   理回路に含まれるレジスタのクロック入力が等しくなる
   ように、前記等価性判定回路を修正するゲーテッドクロ
   ック部分修正ステップと、 前記等価性判定回路生成ステップで生成された等価性判
   定回路又は前記ゲーテッドクロック部分修正ステップで
   修正された等価性判定回路に基づいて、検証すべき少な
   くとも２つの論理回路の論理又は機能の等価性を判定す
   る等価性判定ステップとを含み、これらステップをコン
   ピュータに実行させることを特徴とする論理回路検証プ
   ログラムを格納したコンピュータ読み取り可能な記録媒
   体。