JPH0533425B2 - - Google Patents
Info
- Publication number
- JPH0533425B2 JPH0533425B2 JP61228308A JP22830886A JPH0533425B2 JP H0533425 B2 JPH0533425 B2 JP H0533425B2 JP 61228308 A JP61228308 A JP 61228308A JP 22830886 A JP22830886 A JP 22830886A JP H0533425 B2 JPH0533425 B2 JP H0533425B2
- Authority
- JP
- Japan
- Prior art keywords
- verification
- circuit
- logic
- logical
- display
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Expired - Lifetime
Links
Landscapes
- Tests Of Electronic Circuits (AREA)
- Test And Diagnosis Of Digital Computers (AREA)
Description
【発明の詳細な説明】
〔産業上の利用分野〕
本発明は電子計算機を利用した論理検証支援装
置に係わり、特に論理的な誤りがある場合、その
誤りの箇所を限定するのに好適な論理検証支援装
置に関する。
置に係わり、特に論理的な誤りがある場合、その
誤りの箇所を限定するのに好適な論理検証支援装
置に関する。
従来、論理検証は、シミユレーシヨンによる方
法と、表現の等価性を検証する方法が知られてい
る。シミユレーシヨンによる方法は、例えば論理
回路においては、その構成要素と結線関係から計
算される論理値と、その論理回路が満たすべき機
能から期待される論理値を比較し、両者が一致す
るか否かにより検証する方法である。従つて、こ
の方法ではシミユレーシヨン時に入力すべき論理
値の組と、それらの入力に対して期待される論理
値の組をあらかじめ用意し、各組ごとに、前記比
較を実施することになる。
法と、表現の等価性を検証する方法が知られてい
る。シミユレーシヨンによる方法は、例えば論理
回路においては、その構成要素と結線関係から計
算される論理値と、その論理回路が満たすべき機
能から期待される論理値を比較し、両者が一致す
るか否かにより検証する方法である。従つて、こ
の方法ではシミユレーシヨン時に入力すべき論理
値の組と、それらの入力に対して期待される論理
値の組をあらかじめ用意し、各組ごとに、前記比
較を実施することになる。
一方、表現の等価性を検証する方法では、例え
ば、イリノイ大学、電気工学科の学位論文、ロジ
ツク、デザイン、ベリフイケーシヨン、ユージン
グ、スタテイツク、アナリシス（L.H.Hanes：
Logic Design Verification using Static
Analysis、Ph.D Thesis、University of
Illinois、IL、（1983））の６頁から11頁に示され
ているように、検証の対象とする論理回路を階層
的に表現する。そこで、ある論理回路の構成要素
に着目すれば、その構成要素の満たすべき機能
と、その構成要素を１階層下の構成要素及びそれ
らの結線関係から導かれる動作が表現上等価であ
ることを示す方法がとられる。この際、表現の等
価性を検証する方法として、定理証明法等の記号
処理的方法が利用される。特願昭60−214173号で
は、定理証明法を利用した表現の等価性の検証法
を効率的に実施する為に、証明手順を自動的に決
定する機能を持つ証明法が論じられている。
ば、イリノイ大学、電気工学科の学位論文、ロジ
ツク、デザイン、ベリフイケーシヨン、ユージン
グ、スタテイツク、アナリシス（L.H.Hanes：
Logic Design Verification using Static
Analysis、Ph.D Thesis、University of
Illinois、IL、（1983））の６頁から11頁に示され
ているように、検証の対象とする論理回路を階層
的に表現する。そこで、ある論理回路の構成要素
に着目すれば、その構成要素の満たすべき機能
と、その構成要素を１階層下の構成要素及びそれ
らの結線関係から導かれる動作が表現上等価であ
ることを示す方法がとられる。この際、表現の等
価性を検証する方法として、定理証明法等の記号
処理的方法が利用される。特願昭60−214173号で
は、定理証明法を利用した表現の等価性の検証法
を効率的に実施する為に、証明手順を自動的に決
定する機能を持つ証明法が論じられている。
上記従来技術は、対象とする機器に論理的な誤
りがあるか否かを検証する方法であり、論理的な
誤りが存在する場合に、その箇所を見い出すこと
に対する配慮はなされていない。例えば論理回路
の検証において、シミユレーシヨンによる方法で
は、シミユレーシヨンの結果得られる論理値と、
論理回路が満たすべき機能から期待される論理値
が異なるという事実から、対象とする論理回路の
結線関係及び構成要素の各機能を考慮して、誤り
の箇所を見い出す必要がある。通常この手法で
は、シミユレーシヨンの入力データ作成の簡素化
及び、シミユレーシヨンの実行効率を上げる目的
で、大規模な論理回路を一度に処理する方法がと
られる為に、誤りの箇所を見い出すのに多大な労
力が必要である。
りがあるか否かを検証する方法であり、論理的な
誤りが存在する場合に、その箇所を見い出すこと
に対する配慮はなされていない。例えば論理回路
の検証において、シミユレーシヨンによる方法で
は、シミユレーシヨンの結果得られる論理値と、
論理回路が満たすべき機能から期待される論理値
が異なるという事実から、対象とする論理回路の
結線関係及び構成要素の各機能を考慮して、誤り
の箇所を見い出す必要がある。通常この手法で
は、シミユレーシヨンの入力データ作成の簡素化
及び、シミユレーシヨンの実行効率を上げる目的
で、大規模な論理回路を一度に処理する方法がと
られる為に、誤りの箇所を見い出すのに多大な労
力が必要である。
一方、表現の等価性を検証する方法において
は、等価性の検証手順の実施により変化する内容
（以後、検証経過と呼称する）が、対象とする論
理回路の構成要素及びそれらの結線関係を対応付
けられていない。従つて、論理的な誤りが存在す
る場合、表現が異なる部分の意味を解釈し、それ
らと論理回路の構成要素及び結線関係を対応付
け、誤り箇所を見い出す操作が必要である。
は、等価性の検証手順の実施により変化する内容
（以後、検証経過と呼称する）が、対象とする論
理回路の構成要素及びそれらの結線関係を対応付
けられていない。従つて、論理的な誤りが存在す
る場合、表現が異なる部分の意味を解釈し、それ
らと論理回路の構成要素及び結線関係を対応付
け、誤り箇所を見い出す操作が必要である。
このように、従来技術では機器に論理的な誤り
が存在する場合、その箇所を見い出す為に多大の
労力が必要であるという問題があつた。
が存在する場合、その箇所を見い出す為に多大の
労力が必要であるという問題があつた。
本発明の目的は、機器の論理的な接続が正しい
か否かを検証すると同時に、論理的な誤りが存在
する場合、その誤りの存在する箇所を限定するこ
とができる論理検証支援装置を提供することにあ
る。
か否かを検証すると同時に、論理的な誤りが存在
する場合、その誤りの存在する箇所を限定するこ
とができる論理検証支援装置を提供することにあ
る。
上記目的は、検証法として表現の等価性を検証
する方法において、検証の対象とする機器が満た
すべき機能の表現を変換し、その機器の構成要素
及びそれらの接続関係から導かれる動作の表現と
等価であるか否かを調べる過程に、その検証経過
と機器の構成要素及び接続関係を対応付ける手段
と、この対応付けを利用して、その検証経過を要
素関連図上に同時に表示する手段と、検証手順の
進行に応じて変化する前記表示装置の画面表示を
検証失敗時に該検証失敗時の画面表示に固定する
手段とを導入することにより達成される。
する方法において、検証の対象とする機器が満た
すべき機能の表現を変換し、その機器の構成要素
及びそれらの接続関係から導かれる動作の表現と
等価であるか否かを調べる過程に、その検証経過
と機器の構成要素及び接続関係を対応付ける手段
と、この対応付けを利用して、その検証経過を要
素関連図上に同時に表示する手段と、検証手順の
進行に応じて変化する前記表示装置の画面表示を
検証失敗時に該検証失敗時の画面表示に固定する
手段とを導入することにより達成される。
上記方法において、例えば論理回路の検証を例
にとれば、論理回路の表現の等価性を検証する際
の表現法として、信号間の関係に着目した表現法
を採用する。そこで、前記検証経過と回路の構成
要素及び結線関係の対応付けの手段により、表現
の等価性の検証過程における階層レベル間の展開
や、同一レベル内の置換操作を信号間のマツピン
グや信号の伝播に対応させる。さらに表示手段
は、対応付けられた検証経過を論理回路の回路図
と同一画面上に表示する。この結果、表現の等価
性が示せない場合、即ち論理回路に論理的な誤ま
りが存在する場合、検証失敗となり、画面表示は
検証失敗時の画面表示に固定されるので、その誤
りが存在する箇所を表示画面上で容易に限定する
ことが可能となる。
にとれば、論理回路の表現の等価性を検証する際
の表現法として、信号間の関係に着目した表現法
を採用する。そこで、前記検証経過と回路の構成
要素及び結線関係の対応付けの手段により、表現
の等価性の検証過程における階層レベル間の展開
や、同一レベル内の置換操作を信号間のマツピン
グや信号の伝播に対応させる。さらに表示手段
は、対応付けられた検証経過を論理回路の回路図
と同一画面上に表示する。この結果、表現の等価
性が示せない場合、即ち論理回路に論理的な誤ま
りが存在する場合、検証失敗となり、画面表示は
検証失敗時の画面表示に固定されるので、その誤
りが存在する箇所を表示画面上で容易に限定する
ことが可能となる。
以下、本発明の一実施例を論理回路の検証を例
にとり説明する。なお、以下の説明において、表
現の等価性の検証の為に使用する論理回路の機能
やその回路の構成要素及び結線関係の表現を「回
路表現」あるいは「機能の表現」と呼称し、通常
ネツトリストで表現する構成要素及び結線関係を
「回路図情報」と呼称して両者を区別する。
にとり説明する。なお、以下の説明において、表
現の等価性の検証の為に使用する論理回路の機能
やその回路の構成要素及び結線関係の表現を「回
路表現」あるいは「機能の表現」と呼称し、通常
ネツトリストで表現する構成要素及び結線関係を
「回路図情報」と呼称して両者を区別する。
第１図は、本発明の一実施例における装置の全
体構成を示す。第１図において、１は制御装置、
２は表示装置、３は演算処理装置、４は記憶装
置、５は入力装置、６は両面表示データ格納装
置、７は両面表示プログラム格納装置、８が定理
証明プログラム格納装置、９は回路表現変換プロ
グラム格納装置である。
体構成を示す。第１図において、１は制御装置、
２は表示装置、３は演算処理装置、４は記憶装
置、５は入力装置、６は両面表示データ格納装
置、７は両面表示プログラム格納装置、８が定理
証明プログラム格納装置、９は回路表現変換プロ
グラム格納装置である。
次に本装置における論理検証の処理フローを第
２図を参照して説明する。第２図においては、第
１図中の６〜９に示した各格納装置内には、対応
するデータあるいはプログラムがすでに格納され
ているものとする。また、検証すべき回路の回路
表現は、入力装置５を介して記憶装置４内に格納
されているものとする。第２図において、処理２
１では入力装置５を介して検証すべき回路の機能
の表現が入力され、記憶装置４内に格納される。
処理２２では、演算処理装置３上に回路表現変換
プログラム格納装置９内のプログラムが呼び出さ
れ、入力された回路の機能表現が対応する回路情
報に変換され、その情報は画面表示データ格納装
置６に追加される。処理２３では、演算処理装置
３上に画面表示プログラム格納装置７に格納され
たプログラムが呼び出され、画面表示データ格納
装置６内の画面データを基に、対象とする論理回
路の回路図と、回路の機能の表現に関する情報
が、表示装置２上に表示される。以後、処理２８
において検証が正常に終了するか、あるいは処理
２９において、検証が失敗もしくは、あらかじめ
指定された条件で検証が打ち切られるまで、処理
２４〜２７が繰り返される。処理２４では、演算
処理装置３上に、定理証明プログラムと、定理証
明に使用する規則、及び記憶装置４に格納された
回路表現並びに機能の表現が呼び出され、定理証
明法による推論処理が実施される。以後、記憶装
置４は定理証明法による推論処理の作業領域とし
て利用される。処理２５では処理２４で使用され
た規則が予め指定されたものであるか否かが判定
される。処理２４で使用された規則が予め指定し
たものである場合、処理２６，２７が実行され
る。処理２６及び２７における処理は前記処理２
２，２３と同様であり、処理の対象が、回路の機
能の表現から推論結果に置き換わる。検証が正常
に終了した場合、処理２９により、表示画面は、
回路図のみの表示に戻され、新たな機能の入力持
ちの状態に復帰する。
２図を参照して説明する。第２図においては、第
１図中の６〜９に示した各格納装置内には、対応
するデータあるいはプログラムがすでに格納され
ているものとする。また、検証すべき回路の回路
表現は、入力装置５を介して記憶装置４内に格納
されているものとする。第２図において、処理２
１では入力装置５を介して検証すべき回路の機能
の表現が入力され、記憶装置４内に格納される。
処理２２では、演算処理装置３上に回路表現変換
プログラム格納装置９内のプログラムが呼び出さ
れ、入力された回路の機能表現が対応する回路情
報に変換され、その情報は画面表示データ格納装
置６に追加される。処理２３では、演算処理装置
３上に画面表示プログラム格納装置７に格納され
たプログラムが呼び出され、画面表示データ格納
装置６内の画面データを基に、対象とする論理回
路の回路図と、回路の機能の表現に関する情報
が、表示装置２上に表示される。以後、処理２８
において検証が正常に終了するか、あるいは処理
２９において、検証が失敗もしくは、あらかじめ
指定された条件で検証が打ち切られるまで、処理
２４〜２７が繰り返される。処理２４では、演算
処理装置３上に、定理証明プログラムと、定理証
明に使用する規則、及び記憶装置４に格納された
回路表現並びに機能の表現が呼び出され、定理証
明法による推論処理が実施される。以後、記憶装
置４は定理証明法による推論処理の作業領域とし
て利用される。処理２５では処理２４で使用され
た規則が予め指定されたものであるか否かが判定
される。処理２４で使用された規則が予め指定し
たものである場合、処理２６，２７が実行され
る。処理２６及び２７における処理は前記処理２
２，２３と同様であり、処理の対象が、回路の機
能の表現から推論結果に置き換わる。検証が正常
に終了した場合、処理２９により、表示画面は、
回路図のみの表示に戻され、新たな機能の入力持
ちの状態に復帰する。
以下、第１図及び第２図に示した本発明の一実
施例を、具体例を用いて詳細に説明する。具体的
な論理回路としては、４ビツトシフトレジスタを
使用する。第３図は、４ビツトシフトレジスタの
機能の表現を示している。なお、本実施例では表
現の等価性を検証する際の表現形式として参考文
献(1)に記載されているRTL（Register Transfer
Statement）を使用している。図中、（遷移Ｗ
Ａ Ｂ）は、条件Ｗが成立するときＢがＡに転送
されることを示している。以後、Ｗを遷移条件
項、Ａをデステイネーシヨン項、Ｂをソース項と
呼称する。また、（レジスタＡ Ｎ１ Ｎ２）は、
レジスタＡのＮ１ビツトからＮ２ビツトの値を、
（連結Ａ Ｂ）は、ＡとＢのビツト連結を、（立下
りＡ）は、信号Ａの立下り状態をそれぞれ示して
いる。また、第３図中MC、SL、CLK、CLRは、
それぞれ、４ビツトシフトレジスタにおけるモー
ド選択信号、直列入力、クロツク信号、クリア信
号を示している。さらに、以後使用する図におい
て、下線を施した論理式は否定であること、Ｖは
論理式の論理和を、Eqは等号関係を表わす。ま
た、「＄」で始まる記号はそれが変数であること
を意味している。
施例を、具体例を用いて詳細に説明する。具体的
な論理回路としては、４ビツトシフトレジスタを
使用する。第３図は、４ビツトシフトレジスタの
機能の表現を示している。なお、本実施例では表
現の等価性を検証する際の表現形式として参考文
献(1)に記載されているRTL（Register Transfer
Statement）を使用している。図中、（遷移Ｗ
Ａ Ｂ）は、条件Ｗが成立するときＢがＡに転送
されることを示している。以後、Ｗを遷移条件
項、Ａをデステイネーシヨン項、Ｂをソース項と
呼称する。また、（レジスタＡ Ｎ１ Ｎ２）は、
レジスタＡのＮ１ビツトからＮ２ビツトの値を、
（連結Ａ Ｂ）は、ＡとＢのビツト連結を、（立下
りＡ）は、信号Ａの立下り状態をそれぞれ示して
いる。また、第３図中MC、SL、CLK、CLRは、
それぞれ、４ビツトシフトレジスタにおけるモー
ド選択信号、直列入力、クロツク信号、クリア信
号を示している。さらに、以後使用する図におい
て、下線を施した論理式は否定であること、Ｖは
論理式の論理和を、Eqは等号関係を表わす。ま
た、「＄」で始まる記号はそれが変数であること
を意味している。
第３図に示した機能を満たすように設計された
４ビツトシフトレジスタの回路表現の一部を第４
図に、また証明に使用する規則の一部を第５図に
示す。さらに、第３図及び第５図に対応する回路
図をそれぞれ、第６図、第７図に示す。
４ビツトシフトレジスタの回路表現の一部を第４
図に、また証明に使用する規則の一部を第５図に
示す。さらに、第３図及び第５図に対応する回路
図をそれぞれ、第６図、第７図に示す。
以後、本実施例では第２図中の処理２４に使用
する定理証明法としては、特願昭60−214173号に
開示されている方法を使用する。この証明法で
は、推論法として導出と等号調整法を採用してい
る。また、処理２５で使用する、指定された規則
として第４図中の４４，４８及び第５図中の５３
が予め指定されているものとする。これらは、機
能の表現を推論処理により変形していく際、階層
表現のマツピングや同一階層レベル内での置換に
対応するものである。
する定理証明法としては、特願昭60−214173号に
開示されている方法を使用する。この証明法で
は、推論法として導出と等号調整法を採用してい
る。また、処理２５で使用する、指定された規則
として第４図中の４４，４８及び第５図中の５３
が予め指定されているものとする。これらは、機
能の表現を推論処理により変形していく際、階層
表現のマツピングや同一階層レベル内での置換に
対応するものである。
機能検証の例として第３図中の３１を取りあげ
る。３１は、クリア信号によりシフトレジスタの
出力ビツトの全てに信号値０が入つていること
（クリアされること）を示している。この機能の
検証を実施するには３１が第５図の規則の適用に
よつて第４図中の回路表現に帰着されること（等
価であること）を示す。第８図に、この検証経過
（定理証明経過）の一部を、使用された規則と共
に示す。まず、処理２１において、第８図の８１
が入力される。これに対し処理２２において、回
路情報との対応付けが行われる。この時、回路表
現変換プログラムは、８１の表現に対し、その遷
移条件項CLR、デステイネーシヨン項（レジス
タＱ ０ ３）、ソース項０を取り出し、それぞ
れの信号に対応する回路情報を抽出し、抽出した
信号名に情報を付加する。この操作は、例えばネ
ツトリスト中の対応する信号名の属性に１をセツ
トすること等により実施できる。次に、処理２３
では、情報を付加されたネツトリストの表示デー
タを基に表示画面上に回路図を表示する。この
際、処理２２でセツトされたビツトをチエツクす
ることにより、対応する信号線の表示を太線に変
更する。第９図に表示画面を例示する。第９図か
ら今CLRとＱの間の機能を検証しているようす
がわかる。次に、処理２５，２８，３０，２４と
検証過程が進み、推論結果が第８図中の８３の時
点で処理２５へと移る。この間、表示画面は第９
図のままである。処理２６では、第８図中の８３
の第一論理式が取り出され、処理２２と同様に処
理される。しかしながら、この時点でデステイネ
ーシヨン項の第２項に相当する信号線がない為
に、画面表示データ中の１階層下の表示データが
呼び出され信号線のチエツクが行われる。この結
果、処理２７において第１０図に示す画面が得ら
れる。
る。３１は、クリア信号によりシフトレジスタの
出力ビツトの全てに信号値０が入つていること
（クリアされること）を示している。この機能の
検証を実施するには３１が第５図の規則の適用に
よつて第４図中の回路表現に帰着されること（等
価であること）を示す。第８図に、この検証経過
（定理証明経過）の一部を、使用された規則と共
に示す。まず、処理２１において、第８図の８１
が入力される。これに対し処理２２において、回
路情報との対応付けが行われる。この時、回路表
現変換プログラムは、８１の表現に対し、その遷
移条件項CLR、デステイネーシヨン項（レジス
タＱ ０ ３）、ソース項０を取り出し、それぞ
れの信号に対応する回路情報を抽出し、抽出した
信号名に情報を付加する。この操作は、例えばネ
ツトリスト中の対応する信号名の属性に１をセツ
トすること等により実施できる。次に、処理２３
では、情報を付加されたネツトリストの表示デー
タを基に表示画面上に回路図を表示する。この
際、処理２２でセツトされたビツトをチエツクす
ることにより、対応する信号線の表示を太線に変
更する。第９図に表示画面を例示する。第９図か
ら今CLRとＱの間の機能を検証しているようす
がわかる。次に、処理２５，２８，３０，２４と
検証過程が進み、推論結果が第８図中の８３の時
点で処理２５へと移る。この間、表示画面は第９
図のままである。処理２６では、第８図中の８３
の第一論理式が取り出され、処理２２と同様に処
理される。しかしながら、この時点でデステイネ
ーシヨン項の第２項に相当する信号線がない為
に、画面表示データ中の１階層下の表示データが
呼び出され信号線のチエツクが行われる。この結
果、処理２７において第１０図に示す画面が得ら
れる。
以下、検証定理は階層的に実行されるが、本例
の場合、８３の第一論理式に対応する論理式が４
１に与えられている為、この論理式に対する検証
は終了し、８３の第二論理式へと対象が変わる。
当然のことながら、４１がより下位の表現レベル
（ゲートレベル）で与えられており、かつそこに
論理的な誤りが存在する場合、表示画面は第１０
図に固定され、その論理の誤りがRS−フリツプ
フロツプａのクリア処理にあることが見てとれ
る。
の場合、８３の第一論理式に対応する論理式が４
１に与えられている為、この論理式に対する検証
は終了し、８３の第二論理式へと対象が変わる。
当然のことながら、４１がより下位の表現レベル
（ゲートレベル）で与えられており、かつそこに
論理的な誤りが存在する場合、表示画面は第１０
図に固定され、その論理の誤りがRS−フリツプ
フロツプａのクリア処理にあることが見てとれ
る。
以上は、階層的なマツピングの例について示し
たが、例えば、第４図中の４４が使用された場
合、同様の手続きにより第１０図において信号Ａ
より上流へと検証処理が移行する様子が見てとれ
る。
たが、例えば、第４図中の４４が使用された場
合、同様の手続きにより第１０図において信号Ａ
より上流へと検証処理が移行する様子が見てとれ
る。
さて、以上の実施例においては、検証経過の回
路表現と回路図上の信号線の対応を、信号線を太
くすることにより実施したが、対応する構成要素
の入出力部位の色を変えることや、ブリンクさせ
ること等も容易に実現することができる。
路表現と回路図上の信号線の対応を、信号線を太
くすることにより実施したが、対応する構成要素
の入出力部位の色を変えることや、ブリンクさせ
ること等も容易に実現することができる。
なお、本実施例では論理回路の論理検証を例に
とり説明したが、本発明の適用範囲は論理回路の
検証にとどまらず、各種制御系の動作の検証やプ
ラント機器配管等の接続関係のチエツク等にも広
く適用することが可能である。
とり説明したが、本発明の適用範囲は論理回路の
検証にとどまらず、各種制御系の動作の検証やプ
ラント機器配管等の接続関係のチエツク等にも広
く適用することが可能である。
以上、実施例を用いて詳細に説明したごとく、
本発明によれば、表示装置に表示された回路図上
に論理検証経過を同時に表示できるので、論理回
路に論理的な誤りが存在する場合、その誤りが存
箇所を容易に限定することができ、論理検証を効
率的に実施できるという効果がある。
本発明によれば、表示装置に表示された回路図上
に論理検証経過を同時に表示できるので、論理回
路に論理的な誤りが存在する場合、その誤りが存
箇所を容易に限定することができ、論理検証を効
率的に実施できるという効果がある。
(1) テイー、ジエー ワグナー：ハードウエア
ヴエリフイケーシヨン、フイジカル、ドクタ
セイシス、デパートメント オブ コンピユー
タサイエンス、スタンフオード大学（1977）
T.J Wagner：Hardware Verification、Ph.D
Thesis、Deparement of Computer Science、
Stanford Univ.、（1977）
ヴエリフイケーシヨン、フイジカル、ドクタ
セイシス、デパートメント オブ コンピユー
タサイエンス、スタンフオード大学（1977）
T.J Wagner：Hardware Verification、Ph.D
Thesis、Deparement of Computer Science、
Stanford Univ.、（1977）
第１図は、本発明の一実施例の全体構成図、第
２図は、実施例における処理フロー図、第３図、
４図、５図は、実施例における機能表現、回路表
現、規則説明図、第６図、７図は実施例における
回路説明図、第８図は実施例における検証過程説
明図、第９図、１０図は実施例における表示画面
図である。 １……制御装置、２……表示装置、３……演算
処理装置、４……記憶装置、５……入力装置、６
……画面表示データ格納装置、７……画面表示プ
ログラム格納装置、８……定理証明プログラム格
納装置、９……回路表現変換プログラム格納装
置。
２図は、実施例における処理フロー図、第３図、
４図、５図は、実施例における機能表現、回路表
現、規則説明図、第６図、７図は実施例における
回路説明図、第８図は実施例における検証過程説
明図、第９図、１０図は実施例における表示画面
図である。 １……制御装置、２……表示装置、３……演算
処理装置、４……記憶装置、５……入力装置、６
……画面表示データ格納装置、７……画面表示プ
ログラム格納装置、８……定理証明プログラム格
納装置、９……回路表現変換プログラム格納装
置。
Claims (1)
- 【特許請求の範囲】 １ 機器を構成する要素の動作とそれらの論理的
な接続情報と、当該機器の検証すべき機能と検証
に使用する規則等のデータを入力する入力装置
と、 入力されたデータと検証手順を格納する記憶装
置と、 検証の手順を適用することにより、検証の途中
段階に現れる情報を、記憶装置内に格納された該
機器の構成要素及びそれらの接続情報に対応付け
るための情報を求める演算処理装置と、 該演算処理装置で求めた情報と、前記機器の構
成要素及びそれらの論理的接続情報から求められ
る要素関連図を画面上に同時に表示する表示装置
と から成り、 前記演算処理装置は、検証の進行に応じて変化
する前記表示装置の画面表示を、検証失敗時に該
検証失敗時の画面表示に固定する手段を備える ことを特徴とする論理検証支援装置。 ２ 上記機器は論理回路である特許請求の範囲第
１項記載の論理検証支援装置。
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| JP61228308A JPS6383840A (ja) | 1986-09-29 | 1986-09-29 | 論理検証支援装置 |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| JP61228308A JPS6383840A (ja) | 1986-09-29 | 1986-09-29 | 論理検証支援装置 |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| JPS6383840A JPS6383840A (ja) | 1988-04-14 |
| JPH0533425B2 true JPH0533425B2 (ja) | 1993-05-19 |
Family
ID=16874404
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| JP61228308A Granted JPS6383840A (ja) | 1986-09-29 | 1986-09-29 | 論理検証支援装置 |
Country Status (1)
| Country | Link |
|---|---|
| JP (1) | JPS6383840A (ja) |
Families Citing this family (1)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| JPH02242376A (ja) * | 1989-03-15 | 1990-09-26 | Nishimura Giken:Kk | 論理回路の作図及びシミュレーション装置 |
Family Cites Families (3)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| GB8327350D0 (en) * | 1983-10-13 | 1983-11-16 | British Telecomm | Cad display system |
| JPS6154567A (ja) * | 1984-08-24 | 1986-03-18 | Hitachi Ltd | シミユレ−シヨン方法および装置 |
| JPS61130992A (ja) * | 1984-11-30 | 1986-06-18 | 日本電気株式会社 | 論理動作表示装置 |
-
1986
- 1986-09-29 JP JP61228308A patent/JPS6383840A/ja active Granted
Also Published As
| Publication number | Publication date |
|---|---|
| JPS6383840A (ja) | 1988-04-14 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| US5557774A (en) | Method for making test environmental programs | |
| JP2856640B2 (ja) | 論理回路図エディタシステム | |
| US5568396A (en) | Identifying overconstraints using port abstraction graphs | |
| JPH03257671A (ja) | 設計取り込みシステム | |
| US5615124A (en) | Autonomous evolution type hardware design system | |
| US6477689B1 (en) | Architectural structure of a process netlist design tool | |
| US7069521B2 (en) | Method and apparatus for exploring a multi-element design through user directed selective rendering | |
| US4965758A (en) | Aiding the design of an operation having timing interactions by operating a computer system | |
| KR970063709A (ko) | 레이아웃 입력장치 및 방법과 레이아웃 검증장치 및 방법 | |
| US6832359B2 (en) | Apparatus and method for calculating simulation coverage | |
| CN118228644A (zh) | 数字芯片设计的方法、装置、设备、存储介质和程序产品 | |
| JPH0533425B2 (ja) | ||
| JP2000057188A (ja) | ハードウェア・ソフトウェア協調評価装置 | |
| JPH08202743A (ja) | スイッチレベルシミュレーションシステム | |
| JP2825372B2 (ja) | ハードウェア構造表示装置 | |
| JPS59117660A (ja) | シミユレ−シヨン状態復元処理方式 | |
| George et al. | Interactive Learning Tool for Static-1 Hazard Identification in Digital Electronic Circuits | |
| US7072819B2 (en) | Method for locating functional mistakes in digital circuit designs | |
| SRI | DESIGN AND IMPLEMENTATION OF HYBRID FULL ADDER BASED 16-BIT MULTIPLICATION USING FPGA | |
| JPS6029865A (ja) | 論理シミュレーション装置 | |
| Ben-David et al. | PathFinder: A tool for design exploration | |
| JP2954019B2 (ja) | 論理シミュレーション方式 | |
| JPS6315366A (ja) | 回路変換システム | |
| JPH03104138A (ja) | 階層設計処理方式 | |
| JPH06348463A (ja) | 入出力装置模擬部作成方法 |