JPH10187656A - 物理的環境表現システムと操作方法及び試験方法 - Google Patents
物理的環境表現システムと操作方法及び試験方法Info
- Publication number
- JPH10187656A JPH10187656A JP32623697A JP32623697A JPH10187656A JP H10187656 A JPH10187656 A JP H10187656A JP 32623697 A JP32623697 A JP 32623697A JP 32623697 A JP32623697 A JP 32623697A JP H10187656 A JPH10187656 A JP H10187656A
- Authority
- JP
- Japan
- Prior art keywords
- input
- bits
- physical environment
- state
- input bits
- 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.)
- Pending
Links
Classifications
-
- G—PHYSICS
- G06—COMPUTING OR CALCULATING; COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F30/00—Computer-aided design [CAD]
- G06F30/30—Circuit design
- G06F30/32—Circuit design at the digital level
- G06F30/33—Design verification, e.g. functional simulation or model checking
- G06F30/3323—Design verification, e.g. functional simulation or model checking using formal methods, e.g. equivalence checking or property checking
Landscapes
- Engineering & Computer Science (AREA)
- Computer Hardware Design (AREA)
- Physics & Mathematics (AREA)
- Theoretical Computer Science (AREA)
- Evolutionary Computation (AREA)
- Geometry (AREA)
- General Engineering & Computer Science (AREA)
- General Physics & Mathematics (AREA)
- Management, Administration, Business Operations System, And Electronic Commerce (AREA)
Abstract
(57)【要約】
【課題】ハードウエアの開発試験等のために、環境内の
ハードウエアシステムの挙動を統合するための独自のア
プリケーションを提供する。 【解決手段】一組の状態ビットを保持する状態ビット記
憶部６１と、一組の入力ビットを保持する入力ビット記
憶部５２と、前記状態ビット記憶部６１内に一組の初期
状態の状態ビットを入力する初期状態入力部６０と、前
記入力ビット及び状態ビットを処理するための一組の状
態遷移関数を実行する状態遷移関数実行部６３と、及
び、物理的環境における制限を表現する一組の制約を満
足させる入力ビットを生成するための訂正関数部５１と
を備える。
ハードウエアシステムの挙動を統合するための独自のア
プリケーションを提供する。 【解決手段】一組の状態ビットを保持する状態ビット記
憶部６１と、一組の入力ビットを保持する入力ビット記
憶部５２と、前記状態ビット記憶部６１内に一組の初期
状態の状態ビットを入力する初期状態入力部６０と、前
記入力ビット及び状態ビットを処理するための一組の状
態遷移関数を実行する状態遷移関数実行部６３と、及
び、物理的環境における制限を表現する一組の制約を満
足させる入力ビットを生成するための訂正関数部５１と
を備える。
Description
【０００１】
【発明の属する技術分野】本発明は、物理的環境の動作
を表現或いはシミュレートするためのシステムに関し、
また、システムの特性を試験するための技術、特に、こ
れに限定されるものではないが、ハードウエアシステム
の特性を試験するための技術に適用可能な技術に関す
る。
を表現或いはシミュレートするためのシステムに関し、
また、システムの特性を試験するための技術、特に、こ
れに限定されるものではないが、ハードウエアシステム
の特性を試験するための技術に適用可能な技術に関す
る。
【０００２】
【従来の技術及び発明が解決しようとする課題】ハード
ウエアシステムは、その挙動がシステムへの入力によっ
て完全に決定されるように、それ自身確定的であるが、
同じ事が、ハードウエアシステムが存在する環境にあて
はまるものではない。代表的には、環境の挙動は、環境
の挙動の確定的モデルを提供することができない非常に
多くの入力に依存しているので、、不確定モデルである
と思われる。例え、全ての入力がアクセスできたとして
も出力が未だ未知であるという意味において、その環境
が数学的に不確定なものであるという可能性もある。
ウエアシステムは、その挙動がシステムへの入力によっ
て完全に決定されるように、それ自身確定的であるが、
同じ事が、ハードウエアシステムが存在する環境にあて
はまるものではない。代表的には、環境の挙動は、環境
の挙動の確定的モデルを提供することができない非常に
多くの入力に依存しているので、、不確定モデルである
と思われる。例え、全ての入力がアクセスできたとして
も出力が未だ未知であるという意味において、その環境
が数学的に不確定なものであるという可能性もある。
【０００３】本発明は、例えばハードウエアシステムの
開発試験のために、その環境内のハードウエアシステム
の挙動を統合する際に独自のアプリケーションを提供す
ることを目的とする。また、本発明は、試験目的のため
のソフトウエアの挙動のモデリングに適用することを目
的とする。
開発試験のために、その環境内のハードウエアシステム
の挙動を統合する際に独自のアプリケーションを提供す
ることを目的とする。また、本発明は、試験目的のため
のソフトウエアの挙動のモデリングに適用することを目
的とする。
【０００４】
【課題を解決するための手段】本発明の第１の態様によ
れば、一組の状態ビットを保持する第１の記憶装置と、
一組の入力ビットを保持する第２の記憶装置と、第１の
記憶装置に初期状態の前記一組の状態ビットを入力する
入力装置と、前記一組の入力ビット及び状態ビットを処
理するための一組の状態遷移関数を実行する手段と、物
理的環境における制限を表現する一組の制約を満足させ
る入力ビットを生成するための手段と、を含んで構成さ
れる物理的環境表現システムが提供される。
れば、一組の状態ビットを保持する第１の記憶装置と、
一組の入力ビットを保持する第２の記憶装置と、第１の
記憶装置に初期状態の前記一組の状態ビットを入力する
入力装置と、前記一組の入力ビット及び状態ビットを処
理するための一組の状態遷移関数を実行する手段と、物
理的環境における制限を表現する一組の制約を満足させ
る入力ビットを生成するための手段と、を含んで構成さ
れる物理的環境表現システムが提供される。
【０００５】本発明の第２の態様によれば、所定の物理
的環境におけるハードウエアシステムのシミュレート動
作の結果を生成するためのコンピュータシステムの操作
方法を提供する。その方法は、物理的環境における制限
を表現する一組の制約を満足させる入力ビットを生成す
るステップと、一組の出力を発生するために一組の状態
遷移関数に応じて一組の状態ビットと共に一組の入力ビ
ットを処理するステップと、前記結果を生成するために
前記出力を用いるステップと、を含む。
的環境におけるハードウエアシステムのシミュレート動
作の結果を生成するためのコンピュータシステムの操作
方法を提供する。その方法は、物理的環境における制限
を表現する一組の制約を満足させる入力ビットを生成す
るステップと、一組の出力を発生するために一組の状態
遷移関数に応じて一組の状態ビットと共に一組の入力ビ
ットを処理するステップと、前記結果を生成するために
前記出力を用いるステップと、を含む。
【０００６】本発明の第３の態様によれば、システムへ
の入力の少なくとも部分集合に対して少なくとも１つの
制約を与えるステップと、それぞれの入力の関係を前記
制約から推論するステップと、少なくとも最初の入力に
対して訂正条件を与えるために前記入力関係を処理する
ステップと、一組の制約のない入力を与えるステップ
と、その訂正条件を前記最初の入力に与えるステップ
と、を含むシステムの特性を試験するための方法を提供
する。
の入力の少なくとも部分集合に対して少なくとも１つの
制約を与えるステップと、それぞれの入力の関係を前記
制約から推論するステップと、少なくとも最初の入力に
対して訂正条件を与えるために前記入力関係を処理する
ステップと、一組の制約のない入力を与えるステップ
と、その訂正条件を前記最初の入力に与えるステップ
と、を含むシステムの特性を試験するための方法を提供
する。
【０００７】標準的な確定的システムは、ミーリー機械
として表される。ミーリー機械は、出力が入力と予め記
憶された状態との両方によって決定される順序論理シス
テムである。ミーリー機械は順序論理回路を有するハー
ドウエア装置によって構成される。そのような装置は、
遷移関数によって各々の次の順序状態に接続されるよう
な複数組の状態ビットからなる状態図によって表現でき
る。
として表される。ミーリー機械は、出力が入力と予め記
憶された状態との両方によって決定される順序論理シス
テムである。ミーリー機械は順序論理回路を有するハー
ドウエア装置によって構成される。そのような装置は、
遷移関数によって各々の次の順序状態に接続されるよう
な複数組の状態ビットからなる状態図によって表現でき
る。
【０００８】物理的順序論理回路を備えた物理的ミーリ
ー機械を提供することは可能だが、本発明の好ましい実
施形態は、その数が各状態ビット及び入力ビット、遷移
関数、観察関数、これら変数に関する二進判定図として
セットされる初期状態に割り当てられるミーリー機械の
ソフトウエアモデルを提供する。
ー機械を提供することは可能だが、本発明の好ましい実
施形態は、その数が各状態ビット及び入力ビット、遷移
関数、観察関数、これら変数に関する二進判定図として
セットされる初期状態に割り当てられるミーリー機械の
ソフトウエアモデルを提供する。
【０００９】
【発明の実施の形態】以下に、本発明の実施形態を添付
図面を参照して説明する。図１は、本発明のアプリケー
ションを示す概略図を示す。図１は、３つの回路ブロッ
ク１０，１１，１２を有する装置を示し、この装置は、
３つの入力Ｉ１，Ｉ２，Ｉ３と１つの出力Ｏを有する。
回路ブロック１０は、４つの入力Ａ，Ｂ，Ｃ，Ｄと１つ
の出力Ｅを有する。例として、回路ブロック１０の入力
Ａ，Ｂには、入力Ｉ２，Ｉ３を備える回路ブロック１１
の出力が供給される。回路ブロック１０の入力Ｃには、
回路の入力Ｉ１が供給され、そして、回路ブロック１０
の入力Ｄには、回路ブロック１２の出力Ｆが供給され
る。回路ブロック１２は、回路ブロック１０の出力Ｅか
ら入力を受信する。
図面を参照して説明する。図１は、本発明のアプリケー
ションを示す概略図を示す。図１は、３つの回路ブロッ
ク１０，１１，１２を有する装置を示し、この装置は、
３つの入力Ｉ１，Ｉ２，Ｉ３と１つの出力Ｏを有する。
回路ブロック１０は、４つの入力Ａ，Ｂ，Ｃ，Ｄと１つ
の出力Ｅを有する。例として、回路ブロック１０の入力
Ａ，Ｂには、入力Ｉ２，Ｉ３を備える回路ブロック１１
の出力が供給される。回路ブロック１０の入力Ｃには、
回路の入力Ｉ１が供給され、そして、回路ブロック１０
の入力Ｄには、回路ブロック１２の出力Ｆが供給され
る。回路ブロック１２は、回路ブロック１０の出力Ｅか
ら入力を受信する。
【００１０】回路ブロック１０の挙動を完全に分離して
設計することは可能である。しかし、そのようなモデル
は、この回路ブロック１０が置かれる環境によって実際
の動作では生じない状態を含むかもしれない。例えば、
入力ＡとＣは、常に相補であるように回路ブロック１１
により制約されるかもしれない。その場合、相補でない
ＡとＢのためのモデルの動作は役に立たない。
設計することは可能である。しかし、そのようなモデル
は、この回路ブロック１０が置かれる環境によって実際
の動作では生じない状態を含むかもしれない。例えば、
入力ＡとＣは、常に相補であるように回路ブロック１１
により制約されるかもしれない。その場合、相補でない
ＡとＢのためのモデルの動作は役に立たない。
【００１１】次に、図２を参照すると、本発明は、回路
ブロック１０の環境モデル２１を提供する。図２に示す
環境は、２つの部分を有し、第１の部分は入力環境２１
Ａであり、第２の部分は出力環境２１Ｂである。一般的
には、回路ブロック１０を含む全体を組み合わせて環境
となるが、ここでは、単純化のため入力環境２１Ａだけ
を考える。入力環境２１Ａの作用は、入力Ａ，Ｂ，Ｃ，
Ｄをシミュレートするのに必要とされるような、制約さ
れない一組の入力Ｐ，Ｑ，Ｒ，Ｓに対する制約を与える
ことである。例えば、回路ブロック１１がフリップフロ
ップならば、入力Ａ，Ｂに対して予め検討された制約、
即ち、これらは互いに相補であるという制約が存在す
る。入力Ｃがリセット入力ならば、入力Ｃに対する制約
はＣ＝０であって、通常動作に対して生じる。
ブロック１０の環境モデル２１を提供する。図２に示す
環境は、２つの部分を有し、第１の部分は入力環境２１
Ａであり、第２の部分は出力環境２１Ｂである。一般的
には、回路ブロック１０を含む全体を組み合わせて環境
となるが、ここでは、単純化のため入力環境２１Ａだけ
を考える。入力環境２１Ａの作用は、入力Ａ，Ｂ，Ｃ，
Ｄをシミュレートするのに必要とされるような、制約さ
れない一組の入力Ｐ，Ｑ，Ｒ，Ｓに対する制約を与える
ことである。例えば、回路ブロック１１がフリップフロ
ップならば、入力Ａ，Ｂに対して予め検討された制約、
即ち、これらは互いに相補であるという制約が存在す
る。入力Ｃがリセット入力ならば、入力Ｃに対する制約
はＣ＝０であって、通常動作に対して生じる。
【００１２】図２において、環境モデル２１Ａは、入力
Ｐの論理演算を実行して環境出力Ａを回路１０の入力と
して供給し、また、同様に、各入力Ｑ，Ｒ，Ｓの論理演
算を実行して各環境出力Ｃ，Ｄ，Ｂを回路１０への入力
Ｃ，Ｄ，Ｂとして供給して、入力Ｐ〜Ｓの論理状態がど
のように又はいつ変化しようとも、回路ブロック１０が
図１に示すように配置されている場合には、存在できる
回路ブロック１０への入力はこれらだけであるようにす
る。
Ｐの論理演算を実行して環境出力Ａを回路１０の入力と
して供給し、また、同様に、各入力Ｑ，Ｒ，Ｓの論理演
算を実行して各環境出力Ｃ，Ｄ，Ｂを回路１０への入力
Ｃ，Ｄ，Ｂとして供給して、入力Ｐ〜Ｓの論理状態がど
のように又はいつ変化しようとも、回路ブロック１０が
図１に示すように配置されている場合には、存在できる
回路ブロック１０への入力はこれらだけであるようにす
る。
【００１３】本発明は、制約Ｔが下記の式（１）で与え
られるならば、Ｉは下記の式（２）の関係を満足させる
新たな入力Ｊから生成されることを提案する。 NOT Ｉ∧Ｔ0 ＋Ｉ∧Ｔ1 ・・・ （１） Ｉ＝NOT Ｊ∧NOT Ｔ0 ＋Ｊ∧Ｔ1 ・・・ （２） ここで、Ｉは入力であり、Ｔ0 とＴ1 のどちらもＩには
依存しない。尚、記号∧は論理積を表す。
られるならば、Ｉは下記の式（２）の関係を満足させる
新たな入力Ｊから生成されることを提案する。 NOT Ｉ∧Ｔ0 ＋Ｉ∧Ｔ1 ・・・ （１） Ｉ＝NOT Ｊ∧NOT Ｔ0 ＋Ｊ∧Ｔ1 ・・・ （２） ここで、Ｉは入力であり、Ｔ0 とＴ1 のどちらもＩには
依存しない。尚、記号∧は論理積を表す。
【００１４】リセット信号に関して上述のように示され
る例において、２つの可能な入力状態がある。第１の状
態はＣ＝リセット＝１であり、第２の状態はＣ＝リセッ
ト＝０である。Ｃ＝０という特定の制約を満足させるた
めには、第１の状態は存在せず第２の状態が常時存在す
る。従って、（リセット＝１）＝０と（リセット＝０）
＝１である。従って、Ｃがリセット＝０によって制約さ
れるような入力を表し、ＱがＪとして示された制約され
ない入力である場合、上述のＩとＪとの関係を用いれ
ば、ＣとＱとの関係は下記の式（３）で与えられる。
る例において、２つの可能な入力状態がある。第１の状
態はＣ＝リセット＝１であり、第２の状態はＣ＝リセッ
ト＝０である。Ｃ＝０という特定の制約を満足させるた
めには、第１の状態は存在せず第２の状態が常時存在す
る。従って、（リセット＝１）＝０と（リセット＝０）
＝１である。従って、Ｃがリセット＝０によって制約さ
れるような入力を表し、ＱがＪとして示された制約され
ない入力である場合、上述のＩとＪとの関係を用いれ
ば、ＣとＱとの関係は下記の式（３）で与えられる。
【００１５】 Ｃ＝Ｑ∧０＋（NOT Ｑ）∧（NOT １） ・・・ （３） 上記に関して他の例については、その制約は下記の式
（４）で与えられる。 Ａ＝NOT Ｂ ・・・ （４） この場合、入力ＢがＢ＝Ｓとなるように入力Ｓで直接与
えられると仮定すれば、入力ＰとＳの値に関係なく入力
Ａに与えられた信号を制約して上述した制約を満足させ
ることが必要である。
（４）で与えられる。 Ａ＝NOT Ｂ ・・・ （４） この場合、入力ＢがＢ＝Ｓとなるように入力Ｓで直接与
えられると仮定すれば、入力ＰとＳの値に関係なく入力
Ａに与えられた信号を制約して上述した制約を満足させ
ることが必要である。
【００１６】もしＡ＝１ならば、その制約によってこれ
はＢ（＝Ｓ）＝０の時のみ生じる。もしＡ＝０ならば、
その制約によってこれはＢ（＝Ｓ）＝１の時のみ生じ
る。従って、その関係は、状態（Ａ＝１，NOT Ｂ）、
（Ａ＝０，Ｂ）によって反映される。従って、本発明の
方法を用いれば、下記の式（５）となる。
はＢ（＝Ｓ）＝０の時のみ生じる。もしＡ＝０ならば、
その制約によってこれはＢ（＝Ｓ）＝１の時のみ生じ
る。従って、その関係は、状態（Ａ＝１，NOT Ｂ）、
（Ａ＝０，Ｂ）によって反映される。従って、本発明の
方法を用いれば、下記の式（５）となる。
【００１７】 Ａ＝Ｐ∧（NOT Ｓ）＋（NOT Ｐ）∧（NOT Ｓ） ・・（５） 本発明の方法は、制約を持つミーリー機械から環境を統
合し、その環境のミーリー機械についての特性を試験す
ることである。基本的な考えは、制約を満足させること
を保証された一組の入力をミーリー機械に発生すること
である。制約がＡで、”！ｉ∧Ａ0 ＋Ａ0 ＋ｉ∧Ａ1 ”
（ここで、ｉは入力でＡ0 とＡ1 のどちらもｉに依存し
ない）と等価ならば（シャノン分解）、ｉは、式”ｉ＝
！ｊ∧！Ａ0 ＋ｊ∧Ａ1 ”により新たな入力ｊから生成
される。ｉに対するこの式は、実際に制約（可能な限り
において）を満足させるものある。その理由は、 Ａ＝！ｉ∧Ａ0 ＋ｉ∧Ａ1 ＝！（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ0 ＋（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ1 ＝（！ｊ∧Ａ0 ＋ｊ∧！Ａ1)∧Ａ0 ＋（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ1 ＝！ｊ∧（Ａ0 ＋！Ａ0 ∧Ａ1)＋ｊ∧（Ａ0 ∧！Ａ1 ＋Ａ1) ＝！ｊ∧（Ａ0 ＋Ａ1)＋ｊ∧（Ａ0 ＋Ａ1) ＝Ａ0 ＋Ａ1 であることによる。
合し、その環境のミーリー機械についての特性を試験す
ることである。基本的な考えは、制約を満足させること
を保証された一組の入力をミーリー機械に発生すること
である。制約がＡで、”！ｉ∧Ａ0 ＋Ａ0 ＋ｉ∧Ａ1 ”
（ここで、ｉは入力でＡ0 とＡ1 のどちらもｉに依存し
ない）と等価ならば（シャノン分解）、ｉは、式”ｉ＝
！ｊ∧！Ａ0 ＋ｊ∧Ａ1 ”により新たな入力ｊから生成
される。ｉに対するこの式は、実際に制約（可能な限り
において）を満足させるものある。その理由は、 Ａ＝！ｉ∧Ａ0 ＋ｉ∧Ａ1 ＝！（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ0 ＋（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ1 ＝（！ｊ∧Ａ0 ＋ｊ∧！Ａ1)∧Ａ0 ＋（！ｊ∧！Ａ0 ＋ｊ∧Ａ1)∧Ａ1 ＝！ｊ∧（Ａ0 ＋！Ａ0 ∧Ａ1)＋ｊ∧（Ａ0 ∧！Ａ1 ＋Ａ1) ＝！ｊ∧（Ａ0 ＋Ａ1)＋ｊ∧（Ａ0 ＋Ａ1) ＝Ａ0 ＋Ａ1 であることによる。
【００１８】これは、制約を満足させるｉに可能な割り
当てがある限りは、ｉの式がそのような割り当てである
ことを意味する。他の入力に関する全ての式を、制約”
Ａ0＋Ａ1 ”を用いて生成できる。ｉの式が制約を満足
させるということを理解することは勿論、ｉの全ての可
能な値が生成されることが保証されなければならない。
それ故、”ｒ”が”Ａ”を満足させる全ての入力への割
り当てであると仮定する。もし、”ｒ（ｉ）＝０”なら
ば、”ｒ（Ａ）＝１”だから”ｒ（Ａ0)＝１”を有さな
ければならない（即ち、”Ａ0 ”は、”ｒ”によって規
定された割り当ての下で”１”になる）。ここで、”ｒ
（ｊ）＝０”を設定すると、ｉの式が０になることは明
らかである。同様に、もし、”ｒ（ｉ）＝１”なら
ば、”ｒ（Ａ1)＝１”であり、もし、”ｒ（ｊ）＝１”
を設定すると、ｉの式は１になる。
当てがある限りは、ｉの式がそのような割り当てである
ことを意味する。他の入力に関する全ての式を、制約”
Ａ0＋Ａ1 ”を用いて生成できる。ｉの式が制約を満足
させるということを理解することは勿論、ｉの全ての可
能な値が生成されることが保証されなければならない。
それ故、”ｒ”が”Ａ”を満足させる全ての入力への割
り当てであると仮定する。もし、”ｒ（ｉ）＝０”なら
ば、”ｒ（Ａ）＝１”だから”ｒ（Ａ0)＝１”を有さな
ければならない（即ち、”Ａ0 ”は、”ｒ”によって規
定された割り当ての下で”１”になる）。ここで、”ｒ
（ｊ）＝０”を設定すると、ｉの式が０になることは明
らかである。同様に、もし、”ｒ（ｉ）＝１”なら
ば、”ｒ（Ａ1)＝１”であり、もし、”ｒ（ｊ）＝１”
を設定すると、ｉの式は１になる。
【００１９】制約の完了で、ｉ、即ち、”Ａ1 ＋！Ａ0
”が決定すると、ｉの式は、”Ａ1”に減少し、入力ｉ
は、完全に記述から除かれることは明らかである。図３
において、制約部５０からの制約は訂正関数実行部５１
に提供されて処理される。これらは、制約されない入力
ビットを記憶する第２の記憶装置である入力ビット記憶
部５２から訂正関数実行部５１に入力する入力ビットに
与えられ、物理的環境における制限を表現する一組の制
約を満足させる制約入力ビット５３が生成される。入力
装置である初期状態入力部６０は、初期状態の状態ビッ
トを第１の記憶装置である状態ビット記憶部６１にセッ
トするために用いられる。そして、制約入力ビット５３
と共にこれらは、状態遷移関数実行部６３及び観察関数
実行部６４に提供される入力として用いられる。
”が決定すると、ｉの式は、”Ａ1”に減少し、入力ｉ
は、完全に記述から除かれることは明らかである。図３
において、制約部５０からの制約は訂正関数実行部５１
に提供されて処理される。これらは、制約されない入力
ビットを記憶する第２の記憶装置である入力ビット記憶
部５２から訂正関数実行部５１に入力する入力ビットに
与えられ、物理的環境における制限を表現する一組の制
約を満足させる制約入力ビット５３が生成される。入力
装置である初期状態入力部６０は、初期状態の状態ビッ
トを第１の記憶装置である状態ビット記憶部６１にセッ
トするために用いられる。そして、制約入力ビット５３
と共にこれらは、状態遷移関数実行部６３及び観察関数
実行部６４に提供される入力として用いられる。
【００２０】１つのアップリケーションは、不変系のシ
ステムをモデルすることである。状態が通常の状態遷移
を経由してアクセス可能でないということにおいて残余
である１つ或いはそれ以上の状態を状態図が持つ場合、
そのような不変系の状態は、残余の状態へのシステムの
初期化によってのみアクセスできる。もし、環境がその
制約に従うならば、そのシステムは残差を維持すること
を保証しなければならない。しかしながら、これは、標
準のモデル−チェッキング技術を用いることで検査され
なければならない。しかし、一度検査されると、状態
は、状態の不変を保証する一組の信号を生成するために
新たな一組の状態ビットを用いる上述した環境統合技術
を用いてエンコードされる。新たなミーリー機械が、順
序的にオリジナルと同等であることを検査するため、２
つの機械の入力と状態観察が等しいという仮定の下に、
オリジナルの状態ビットが、もとの観察関数に加えられ
る。そのとき、その出力と次の状態観察は等しい。
ステムをモデルすることである。状態が通常の状態遷移
を経由してアクセス可能でないということにおいて残余
である１つ或いはそれ以上の状態を状態図が持つ場合、
そのような不変系の状態は、残余の状態へのシステムの
初期化によってのみアクセスできる。もし、環境がその
制約に従うならば、そのシステムは残差を維持すること
を保証しなければならない。しかしながら、これは、標
準のモデル−チェッキング技術を用いることで検査され
なければならない。しかし、一度検査されると、状態
は、状態の不変を保証する一組の信号を生成するために
新たな一組の状態ビットを用いる上述した環境統合技術
を用いてエンコードされる。新たなミーリー機械が、順
序的にオリジナルと同等であることを検査するため、２
つの機械の入力と状態観察が等しいという仮定の下に、
オリジナルの状態ビットが、もとの観察関数に加えられ
る。そのとき、その出力と次の状態観察は等しい。
【００２１】このように、物理的環境を表現するための
システム、及び、ハードウエアシステムのシミュレート
動作の結果を生成するためのコンピュータシステムの操
作方法が述べられている。
システム、及び、ハードウエアシステムのシミュレート
動作の結果を生成するためのコンピュータシステムの操
作方法が述べられている。
【図１】本発明のアプリケーションを示す図
【図２】環境とその環境に従う回路を示す図
【図３】本発明のブロック図
１０，１１，１２ 回路ブロック ２１ａ 入力環境 ２１ｂ 出力環境 ５０ 制約部 ５１ 訂正関数実行部 ５２ 入力ビット記憶部 ６０ 初期状態入力部 ６１ 状態ビット記憶部 ６３ 状態遷移関数実行部 ６４ 観察関数生成部
Claims (10)
- 【請求項１】一組の状態ビットを保持する第１の記憶装
置と、 一組の入力ビットを保持する第２の記憶装置と、 前記第１の記憶装置に初期状態の前記一組の状態ビット
を入力する入力装置と、 前記一組の入力ビット及び状態ビットを処理するために
一組の状態遷移関数を実行する手段と、 物理的環境における制限を表現する一組の制約を満足さ
せる入力ビットを生成する手段と、を含んで構成される
ことを特徴とする物理的環境表現システム。 - 【請求項２】前記一組の入力ビット及び状態ビットから
一組の観察関数を生成する手段を含んで構成される請求
項１に記載の物理的環境表現システム。 - 【請求項３】前記入力ビットを生成する手段は、制約さ
れない入力ビットを提供する手段と、前記制約されない
入力ビットを制約して、前記一組の制約が満足されるよ
うにする手段と、を含んで構成される請求項１又は２に
記載の物理的環境表現システム。 - 【請求項４】前記制約する手段は、一組の訂正条件に前
記制約を転送する手段と、前記制約されない入力ビット
に前記訂正条件を供給する手段とを含んで構成される請
求項３に記載の物理的環境表現システム。 - 【請求項５】所定の物理的環境におけるハードウエアシ
ステムのシミュレート動作の結果を生成するための物理
的環境システムの操作方法であって、 物理的環境における制限を表現する一組の制約を満足さ
せる入力ビットを生成するステップと、 一組の出力を発生するために一組の状態遷移関数に応じ
て一組の状態ビットと共に一組の入力ビットを処理する
ステップと、 前記結果を生成するために前記出力を用いるステップ
と、 を含むことを特徴とする物理的環境システムの操作方
法。 - 【請求項６】前記入力ビットと前記状態ビットに依存し
ない一組の観察関数を生成するステップを含む請求項５
に記載の物理的環境システムの操作方法。 - 【請求項７】前記生成ステップが、一組の制約されない
入力ビットを提供するステップと、前記制約されない入
力ビットに前記制約を提供するステップとを含む請求項
５又は６に記載の物理的環境システムの操作方法。 - 【請求項８】前記一組の制約を提供するステップが、一
組の訂正条件に前記制約を転送するステップと、前記制
約されない入力ビットに前記訂正条件を提供するステッ
プとを含む請求項７に記載の物理的環境システムの操作
方法。 - 【請求項９】前記ハードウエアシステムは、ハードウエ
ア装置の一部を含み、前記物理環境は前記ハードウエア
装置の残差の少なくとも一部の代表である請求項５に記
載の物理的環境システムの操作方法。 - 【請求項１０】システムへの入力の少なくとも部分集合
に対して少なくとも１つの制約を与えるステップと、 それぞれの一組の入力関係を前記制約から推論するステ
ップと、 少なくとも最初の入力に対して訂正条件を提供するため
に入力関係を処理するステップと、 一組の制約されない入力を提供するステップと、 前記最初の入力にその訂正条件を提供するステップと、 を含むことを特徴とする物理的環境システムの試験方
法。
Applications Claiming Priority (2)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| GBGB9624935.4A GB9624935D0 (en) | 1996-11-29 | 1996-11-29 | System and method for representing physical environment |
| GB9624935-4 | 1996-11-29 |
Publications (1)
| Publication Number | Publication Date |
|---|---|
| JPH10187656A true JPH10187656A (ja) | 1998-07-21 |
Family
ID=10803732
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| JP32623697A Pending JPH10187656A (ja) | 1996-11-29 | 1997-11-27 | 物理的環境表現システムと操作方法及び試験方法 |
Country Status (4)
| Country | Link |
|---|---|
| US (1) | US6134512A (ja) |
| EP (1) | EP0845745A1 (ja) |
| JP (1) | JPH10187656A (ja) |
| GB (1) | GB9624935D0 (ja) |
Families Citing this family (7)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US6816821B1 (en) * | 1997-09-03 | 2004-11-09 | Stmicroelectronics Limited | Post image techniques |
| US6784805B2 (en) * | 2000-03-15 | 2004-08-31 | Intrigue Technologies Inc. | State-based remote control system |
| US8531276B2 (en) | 2000-03-15 | 2013-09-10 | Logitech Europe S.A. | State-based remote control system |
| US7080314B1 (en) * | 2000-06-16 | 2006-07-18 | Lucent Technologies Inc. | Document descriptor extraction method |
| DE60110811T2 (de) * | 2000-08-28 | 2006-02-02 | Verisity Ltd. | Verfahren zur bereitstellung von bitweisen einschränkungen während einer test-generierung |
| DE102006018238A1 (de) | 2005-04-20 | 2007-03-29 | Logitech Europe S.A. | System und Verfahren zur adaptiven Programmierung einer Fernbedienung |
| US8508401B1 (en) | 2010-08-31 | 2013-08-13 | Logitech Europe S.A. | Delay fixing for command codes in a remote control system |
Family Cites Families (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US5311521A (en) * | 1990-01-12 | 1994-05-10 | Boris Fitingof | Method and apparatus for implementing post-modulation error correction coding scheme |
| US5258919A (en) * | 1990-06-28 | 1993-11-02 | National Semiconductor Corporation | Structured logic design method using figures of merit and a flowchart methodology |
| US5331568A (en) * | 1991-06-18 | 1994-07-19 | Microelectronics & Computer Technology Corporation | Apparatus and method for determining sequential hardware equivalence |
| US5706473A (en) * | 1995-03-31 | 1998-01-06 | Synopsys, Inc. | Computer model of a finite state machine having inputs, outputs, delayed inputs and delayed outputs |
-
1996
- 1996-11-29 GB GBGB9624935.4A patent/GB9624935D0/en active Pending
-
1997
- 1997-11-21 EP EP97309410A patent/EP0845745A1/en not_active Withdrawn
- 1997-11-24 US US08/979,450 patent/US6134512A/en not_active Expired - Lifetime
- 1997-11-27 JP JP32623697A patent/JPH10187656A/ja active Pending
Also Published As
| Publication number | Publication date |
|---|---|
| EP0845745A1 (en) | 1998-06-03 |
| US6134512A (en) | 2000-10-17 |
| GB9624935D0 (en) | 1997-01-15 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Papadopoulos et al. | Model-based synthesis of fault trees from matlab-simulink models | |
| JP2699377B2 (ja) | ハードウエア論理シミユレータ | |
| US6698003B2 (en) | Framework for multiple-engine based verification tools for integrated circuits | |
| US5291495A (en) | Method for designing a scan path for a logic circuit and testing of the same | |
| US7434101B2 (en) | Highly specialized scenarios in random test generation | |
| KR100337696B1 (ko) | 모델 검사를 위한 동작 환경을 자동적으로 생성하는 방법 | |
| US5960182A (en) | Hardware-software co-simulation system, hardware-software co-simulation method, and computer-readable memory containing a hardware-software co-simulation program | |
| US20080052650A1 (en) | Method for Verification Using Reachability Overapproximation | |
| CN112613259B (zh) | 片上系统后仿真方法、装置及电子设备 | |
| JP2002073719A (ja) | 回路動作モデル記述の生成方法および論理設計検証装置 | |
| KR100764588B1 (ko) | 디지털 회로의 자동 설계 장치, 자동 설계 방법, 및 자동설계 프로그램 | |
| JP2009283004A (ja) | モデルベース診断インタフェース | |
| US5491639A (en) | Procedure for verifying data-processing systems | |
| US20030130813A1 (en) | Adaptive test program generation | |
| Albergo et al. | Understanding xacro misunderstandings | |
| Abramovici et al. | Concurrent fault simulation and functional level modeling | |
| JPH10187656A (ja) | 物理的環境表現システムと操作方法及び試験方法 | |
| JPH10283394A (ja) | 故障シミュレーション方法 | |
| CN114880975A (zh) | 一种硬件木马的生成方法、系统、设备以及介质 | |
| CN1983288A (zh) | 验证操作支持系统及其方法 | |
| CN104951583A (zh) | 数字集成电路仿真方法及仿真器 | |
| CN112784417A (zh) | 一种基于SysML的航电分布式联合仿真方法及系统 | |
| CN116911219A (zh) | 用于逻辑系统设计的仿真的方法、电子设备和存储介质 | |
| Hu et al. | An integrated modeling and simulation methodology for intelligent systems design and testing | |
| JPH1091677A (ja) | シミュレーション／エミュレーションの効率を増すための論理変換方法 |