JPH0760324B2 - シーケンシャル回路及びその生成方法、及びコントローラ及び有限状態マシン - Google Patents

シーケンシャル回路及びその生成方法、及びコントローラ及び有限状態マシン

Info

Publication number
JPH0760324B2
JPH0760324B2 JP3062481A JP6248191A JPH0760324B2 JP H0760324 B2 JPH0760324 B2 JP H0760324B2 JP 3062481 A JP3062481 A JP 3062481A JP 6248191 A JP6248191 A JP 6248191A JP H0760324 B2 JPH0760324 B2 JP H0760324B2
Authority
JP
Japan
Prior art keywords
task
circuit
given
improved
sequential
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 - Fee Related
Application number
JP3062481A
Other languages
English (en)
Other versions
JPH04219804A (ja
Inventor
ハレル ズヴィ
ピィ． カーシャン ロバート
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
AT&T Corp
Original Assignee
AT&T Corp
Priority date (The priority date 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 date listed.)
Filing date
Publication date
Application filed by AT&T Corp filed Critical AT&T Corp
Publication of JPH04219804A publication Critical patent/JPH04219804A/ja
Publication of JPH0760324B2 publication Critical patent/JPH0760324B2/ja
Anticipated expiration legal-status Critical
Expired - Fee Related legal-status Critical Current

Links

Classifications

    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F15/00—Digital computers in general; Data processing equipment in general
    • 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
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design

Landscapes

  • Engineering & Computer Science (AREA)
  • Theoretical Computer Science (AREA)
  • Computer Hardware Design (AREA)
  • Physics & Mathematics (AREA)
  • General Engineering & Computer Science (AREA)
  • General Physics & Mathematics (AREA)
  • Evolutionary Computation (AREA)
  • Geometry (AREA)
  • Debugging And Monitoring (AREA)
  • Tests Of Electronic Circuits (AREA)
  • Test And Diagnosis Of Digital Computers (AREA)

Description

【発明の詳細な説明】
【０００１】
【産業上の利用分野】本発明は、コントロールインテン
シブ（制御指向型）システムに関し、特に形式的確認に
基づく方法論によるこの種のシステムの有限状態機械
（マシン）によるインプリメンテーションの開発に関す
る。
【０００２】
【従来の技術】メモリを有するデジタル回路は一般にシ
ーケンシャル回路あるいは有限状態マシンと呼称され
る。有限状態マシンは２つのカテゴリーに分類され得
る。その１つは、その適切なオペレーションが、それ自
体を再帰的に呼び出すようなルーチンによって記述され
なければならないシグナルプロセシングマシンであり、
他の１つは、再帰的ではないコントロールインテンシブ
（制御指向）マシンである。例えば、ＦＩＲフィルタは
第一のカテゴリーに属している。通信プロトコルハード
ウエアは第二のカテゴリーに属する。制御指向有限状態
マシンの設計は困難な仕事である。通常、この種の設計
の目的は、正確かつデータストラクチャの変更に関して
頑強かつサポートし易いインプリメンテーションを効率
的かつ迅速に開発することである。
【０００３】特定の形式的確認（フォーマルベリフィケ
ーション）フレームワークの値は、インプリメンテーシ
ョンがテストされる要求の観点あるいは一般性によって
測られる。例えば、各々の状態においてプロトコルが何
ら不都合なことをしないことを確認することが可能であ
る。このことは、あるアプリケーションにおいては充分
であるが別のアプリケーションにおいては充分ではな
い。例えば、通信プロトコルに関してはこの種の確認は
不充分である。なぜなら、第一義的な関心事はメッセー
ジがデスティネーションにおいて受信されることであ
り、この種の確認はこのことを保証しないからである。
【０００４】インプリメンテーションの適切な振舞いを
保証するために、振舞いのテストが大量になされなけれ
ばならない。通常、このことは大量のシミュレーション
を意味するが、今日ではシミュレーションは不適切であ
ると一般に認識されている（全ての事象に対するシミュ
レートさるべき入力信号の可能なシーケンスの組が無限
である）。他方、フォーマルベリフィケーション技法
は、全ての状況下におけるシステムの一般的な振舞いに
係る結論を有限の組を用いて引き出す能力を有してい
る。
【０００５】種々の要求が有限状態マシンの広範な性質
を扱うので、フォーマルベリフィケーションは高レベル
モデルすなわちインプリメンテーションの抽象化された
ものに対して最も容易に最も頻繁に適用される。この種
の確認は不充分である。高レベルモデルの確認がインプ
リメンテーションに対する実際の意味を持つためには、
高レベルモデルから当該インプリメンテーションへの形
式的関連すなわち変換が存在しなければならない。
【０００６】抽象的なモデルから実際のインプリメンテ
ーションへの形式的変換が存在しない場合においても、
当該モデルの形式解析は便利である。例えば、プロトコ
ルを実現する有限状態マシンに関連して、形式解析はプ
ロトコルそれ自体の概念そのものにおける欠陥を見いだ
す。しかしながら、この種の欠陥が存在しない場合にイ
ンプリメンテーションが”確認された”ものとみなすこ
とは、確認されたモデルと実際のインプリメンテーショ
ンとの間に形式的かつテスト可能な関連が存在しない場
合には不適切である。
【０００７】高レベルモデルすなわちスタンダードとイ
ンプリメンテーションとの間の形式的関連を定義する簡
潔な方法は、モデルすなわちスタンダードにおける状態
をインプリメンテーションの状態の組と関連させること
である。例えば、この種の関連は、通信プロトコルの高
レベルモデルのレシーバ・レディ状態が、当該プロトコ
ルのインプリメンテーションに係るある状態マシンコン
ポーネントがレシーバ・レディ状態にあるようなインプ
リメンテーション状態の組に対応していることを要求す
る。この状態マシンコンポーネントがレシーバ・レディ
状態にあるようなインプリメンテーション状態の組は非
常に大きい。なぜなら、当該状態は、レシーバ・レディ
状態を有する状態マシンコンポーネントとともに生ずる
回路におけるポインタ、バッファ、カウンタ等の対応す
る全ての可能な値によって決定されるからである。高レ
ベルモデルあるいはスタンダードに従ってレシーバ・レ
ディ状態からの正確な遷移がトランスミット状態へのも
のであると仮定した場合でも、あるインプリメンテーシ
ョン状態に対しては（すなわち、ポインタ、バッファ等
のある値に対しては）当該インプリメンテーションはモ
デルあるいはスタンダードに追随するが他の場合は追随
しない。高レベルモデルあるいはスタンダードがインプ
リメンテーションを抽象化していることを実際に確認す
るためには、当該抽象化が各々高レベル状態及び遷移に
対応する単一のインプリメンテーション状態及び遷移に
対するのみならず、全ての手入れベル状態及び遷移に対
するものであることを例示することが必要である。実
際、インプリメンテーションの最大の弱点は動作の”境
界”（バッファが空である、一杯である等）で発生し、
これらの”境界”は非常に複雑な場合がある。
【０００８】
【発明が解決しようとする課題】上述されているよう
に、モデルの全ての可能な状態（すなわち、ポインタ、
バッファ等の全ての可能な組合せ）をシミュレートする
ために力ずくの方法を用いることも可能ではあるが、こ
れはほとんど実用的ではない。高レベルモデルあるいは
スタンダードがわずか５０から５００の状態を有するの
に対して、インプリメンテーションは通常、その数が近
似によってしか評価され得ないほど大量の状態を有して
いる。例えば、”平均的な”プロトコルインプリメンテ
ーションのポインタ、バッファ及び状態マシンコントロ
ーラの値の可能な組合せの全てが与えられた場合、回路
の状態空間はおよそ１０の一万乗個の到達可能な状態を
有することになる。力ずくの方法による確認が地球上の
全ての人間によって完全に並列可能でありかつ全ての人
間に対してその仕事を遂行するためにスーパーコンピュ
ータが与えられていたとしても、１０の一万乗回もの確
認作業は太陽が燃えつきるまで終了しない。
【０００９】インプリメンテーションの全ての可能な遷
移を直接指し示す（すなわち、ポインタ、バッファ等の
全ての可能な値を示す）ことはほとんど不可能であるの
で、インプリメンテーションが高レベル抽象化に対して
忠実であることを結論付ける代替法がなければならな
い。
【００１０】結論として、フォーマルベリフィケーショ
ンを高レベル記述を低レベル機能に変換する総合的かつ
証明されている方法と結びつけることは、有限状態マシ
ンが表現する非常な複雑さという観点からは未だに不充
分である。この複雑さを低減するために、当業者は複雑
な問題をより簡単な表現に置き換えることを試みてい
る。第１４回国際コロキウム（西ドイツ・カルルスルー
エ（Ｋａｒｌｓｒｕｈｅ）、１９８７年７月１３−１７
日）のプロシーディングである”レクチャー・ノート・
イン・コンピュータ・サイエンス”（”Ｌｅｃｔｕｒｅ
Ｎｏｔｅ ｉｎＣｏｍｐｕｔｅｒ Ｓｃｉｅｎｃ
ｅ”）（シュプリンガー・フェアラーク（Ｓｐｒｉｎｇ
ｅｒ Ｖｅｒｌａｇ））において、ケー・ジー・ラーセ
ン（Ｋ．Ｇ．Ｌａｒｓｅｎ）らは、システムを分解して
サブシステムの持つ、全体のシステムに対しても真であ
るような性質を示すことにより、構成的証明を与えてい
る。しかしながら、彼らは、彼らの用いた（複雑な問題
の等価かつ簡潔な問題による）置換が有効であることを
証明する方法論を与えていない。
【００１１】簡潔に述べれば、制御指向有限状態マシン
の開発に対して必要とされているものは、フォーマルベ
リフィケーション、高レベルデザインから改善されたイ
ンプリメンテーションへの振舞いを保存するような形式
的変換、及び当該改善されたインプリメンテーションに
よって結果としてもたらされる複雑さを処理するための
手段を含む、自動化されたソフトウエア・エイデッド・
デザイン法である。
【００１２】
【課題を解決するための手段】本発明により、高レベル
から低レベルへの変換が連続した改善に基づく形式的な
トップダウン開発プロシージャの形態で与えられる。標
準プロトコルの形式的抽象化等の高レベル（抽象的）か
ら始めて、連続した改善を通じて次第により詳細なモデ
ルが生成される。前記改善は、抽象化のあるレベルで確
認された性質がそののちの全ての抽象化のレベルにおい
て成立することを保証するように行なわれる。前記連続
した改善は、プロトコルの最終的なインプリメンテーシ
ョンを形成する低レベル”モデル”で終了する。
【００１３】本発明の一実施例において、本発明に係る
分析／開発装置は、ストアされたプログラムによって制
御されるマシンにおいて実行された場合に規定されたタ
スクを実行することが保証された規定されたシステムの
唯一のＣ言語コード表現を生成する。当該コードは、当
該コードのインストラクションを実行する、ソフトウエ
アによって制御されたプロセッサのメモリにストアさ
れ、それによって所望の有限状態マシンを実現する。他
の実施例においては、前記コードが特定のシステムの集
積回路を製造するために用いられるレイアウトマスクの
組に変換される”ネットリスト”を生成するために用い
られる。
【００１４】
【実施例】前述されているように、本発明は、与えられ
た機能をインプリメントする有限状態マシンを生成しか
つ当該インプリメントされたマシンが企図された機能を
ミスすることなく実行することを確認することの必要性
に係るものである。本発明は、プログラムによって制御
されたプロセッサあるいは特別に設計された装置におい
て目標とする有限状態マシンを実現する。プロセッサに
置いて目標とする有限状態マシンをインプリメントする
プログラムを構成し、かつハードウエア実施例における
回路のストラクチャを指示するコードは、以下に記述さ
れているアナライザ／デベロッパによって開発される。
【００１５】まず始めに、本発明が唯一のエンドプロダ
クトを生成し、それが本発明の原理に従って開発された
有限状態マシンであることに留意されたい。当該マシン
は以下に記述されているような独特の性質を有してい
る。本発明は他のプロダクトも生成し、それは”従来
の”ハードウエア（例えば集積回路）あるいはソフトウ
エアによって制御されたハードウエアのいずれかによっ
て実現される前記有限状態マシン（ＦＳＭ）を開発する
のに適した、形式的に確認されたスペシフィケーション
である。ソフトウエアによって制御される実施例に関し
ては、技術的な努力により制御システムの開発がソフト
ウエアによって制御されたハードウエアにおける制御シ
ステムの開発へ大幅にシフトしてきており、多くの労働
時間がソフトウエア生成にかけられていることにも留意
されたい。この種のソフトウエア生成に係る労力は本発
明に係る方法によって大幅に低減され得る。すなわち、
本発明をソフトウエア制御ハードウエアを生成するため
のツールとみなすことは適切である。
【００１６】本発明の原理に従って確認された有限状態
マシンのデザインを開発することは、インタラクティブ
なデザインプロセスを企図している。本発明に従ったデ
ザインアナライザ／デベロッパの全体的なブロック図を
示した図１において、ユーザは改善ブロック１０にデザ
インさるべきシステムの高レベルスペシフィケーション
を入力する。ブロック１０が、当該スペシフィケーショ
ンが内部矛盾を有さないと判断すると、当該システムス
ペシフィケーション情報はベリフィケーションブロック
２０へ渡される。ブロック２０はユーザからタスクのス
ペシフィケーションを受け取り、規定されたタスクがブ
ロック１０によって与えられたシステムスペシフィケー
ションによって規定されるストラクチャによって適切に
実行されることを確認する。ブロック１０あるいは２０
においてエラーが検出されると、エラーメッセージがス
テータスライン１１あるいは／及び２１上でユーザ宛送
出され、当該ユーザには入力ライン１２及び２２を介し
て当該エラーを修正する機会が与えられる。エラーが検
出されない場合には、本発明に係るデザイン反復手続き
は完了する。
【００１７】次の反復は、ユーザがシステムに係るより
詳細な情報を提供しかつ前記システムが実行すべきタス
クのより広範な組を識別した際に開始される。その時点
において、ブロック１０はユーザによって与えられたシ
ステムスペシフィケーションの改善を分析し、当該改善
されたスペシフィケーションがそれ以前の反復において
確認されたスペシフィケーションに包摂されていること
を決定する。エラーが検出されない場合には、当該改善
されたスペシフィケーションはブロック２０に渡され、
新たに規定されたタスクが当該改善されたスペシフィケ
ーションによって規定されたストラクチャによって適切
に実行されるか否かが評価される。
【００１８】この種の反復を数多く繰り返すことによっ
て、ブロック１０によって保持されているシステムスペ
シフィケーションは充分に詳細になり、必要なタスクの
全てを実行し得るほど強固になる。すなわち、スペシフ
ィケーションは適応され得る入力に応答して期待され
る、すなわち目標とされる全ての出力が充分生成される
ほど強固である。一般には、その時点で当該デザインプ
ロセスはブロック３０に進む。ブロック３０は、ブロッ
ク１０内のシステムスペシフィケーションを、ユーザが
デザインしたマシンを作り上げることを可能にする形態
に変換する。今日では、前記形態はストアード・プログ
ラム・プロセッサ上で実行されるプログラムであり、デ
ザインされた有限状態マシンを形成する組合せ回路を規
定する論理式の集合である。あるいは、前記形態は、集
積回路のレイアウトを生成するネットリストである。
【００１９】図２は、図１に示された装置のより詳細な
記述を表わしている。改善ブロック１０は、改善ストレ
ージブロック１３、改善ベリフィケーションブロック１
４及びシステム定義ストレージブロック１５を有してい
る。ブロック１３及び１５はブロック１４に対して信号
を供給し、それに応じてブロック１４はブロック１５へ
の修正信号を供給する。ブロック１４はステータスライ
ン１１へも信号を供給する。本発明に係るデザインプロ
セスは、空のシステムストレージブロック１５を有する
ところから開始される。ユーザはデザインさるべきシス
テムの高レベル定義をブロック１３に対して与え、解析
が進行する。一般には、ブロック１４はブロック１３の
内容を解析して、ブロック１３のシステム定義がブロッ
ク１５のシステム定義に包切されていることを決定す
る。しかしながら、第一回目の反復においては、この解
析に係る肯定的な結論が自動的に得られる。なぜなら、
ブロック１５が空であるからである。この肯定的結論
（すなわち、スペシフィケーションがエラーを含まない
という結論）により、ブロック１３はその内容をブロッ
ク１５へ転送し、ステータスライン１１上に、ユーザに
現時点における反復が成功したという結論を知らせるメ
ッセージを送出する。
【００２０】次の反復が開始される場合には、ブロック
１３への改善されたシステム定義及びマッピングを入力
する。当該マッピングは、ブロック１５におけるシステ
ムスペシフィケーションに係る状態及び当該状態におけ
る動作を、ブロック１３におけるシステムスペシフィケ
ーションに係る状態及び当該状態における動作にマッピ
ングするものである。すなわち、当該マッピングは、図
３に示されているように、状態を状態へ、及び動作を動
作へマッピングする。
【００２１】図３は、ブロック１５におけるシステム定
義の一部をレベル１として、かつ、ブロック１３におけ
るより改善されたシステム定義をレベル２として示して
いる。具体的には、レベル１は、状態”ＲＥＡＤＹ”及
び状態”ＭＳＧ”、動作”ＳＥＮＤ−ＭＳＧ”、及び当
該動作が生じた場合に状態”ＭＳＧ”の選択が存在する
ことを示している。図３は、さらに、レベル２からレベ
ル１へのマッピングΦが存在することをも示している。
レベル２は、状態”ＲＥＡＤＹ”及び動作”ＳＥＮＤ＿
ＭＳＧ１”、”ＳＥＮＤ＿ＭＳＧ２”、．．．、”ＳＥ
ＮＤ＿ＭＳＧＭ”に続く状態”ＭＳＧ１”、”ＭＳＧ
２”、．．．、”ＭＳＧＭ”が存在することを示してい
る。マッピングΦは、 Φ（レベル２の状態）＝＞レベル１における状態、及
び、 Φ（レベル２の動作）＝＞レベル１における動作、 というものである。
【００２２】ブロック１４は、改善された定義及びマッ
ピングをブロック１５に保持されている定義と比較して
解析する。エラーが検出されると、ステータスライン１
１は診断メッセージをユーザに提供する。その後、ユー
ザはブロック１３に保持されている改善された定義を修
正して再度トライすることが可能である。エラーが検出
されない場合には、改善ストレージブロック１３の内容
がブロック１４を介してシステム定義ストレージブロッ
ク１５へ転送される。この反復プロセスは、ブロック１
５におけるシステム定義が充分に詳細になるまで続行さ
れる。
【００２３】図２に示された入力に関して、システムを
規定する方法が複数個存在すること、及び本発明がその
選択に依存していないことに留意されたい。利用可能な
選択には、ブール代数による表現、指示グラフ記述、そ
の他が含まれる。本実施例においては、従来技術に係る
信号グラフを用いたアプローチが用いられている。当該
アプローチにおいては、システムがプロセス状態と当該
プロセス状態間の遷移との集合体として規定される。各
々のプロセス状態においては、当該状態の関数としての
ある選択が可能である。各々の状態遷移には、当該プロ
セス状態と当該プロセス状態がコミュニケートする他の
プロセス状態とにおける選択の観点から表現された可能
なプレディケートが関連している。
【００２４】システムをプロセス状態（ノード）と遷移
（エッジ）との集合として記述するためのシンタクス
は、データフロー型言語を形成する。この種の言語は、
ノードを識別する手段及びエッジを識別する手段を有し
ている。コーディネーションに係るｓ／ｒモデルに基づ
いてモデル化されたＳ／Ｒ言語は、本明細書において用
いられている言語である。これは、基本的には、表２ー
３７において定義されている。
【００２５】ブロック１４において実行される最初のフ
ォーマルベリフィケーションは、ブロック１３での改善
されたシステム定義における全てのエッジがブロック１
５のシステム定義における一つのエッジに正確にマッピ
ングされている、すなわち対応している、ことを決定す
るタスクである。基本的には、当該タスクはブロック１
４でのスペシフィケーションの状態空間表現における各
々のエッジを調べるものであり、規定されたマッピング
に従って、ブロック１５でのスペシフィケーションの状
態空間表現において対応するエッジが存在することを決
定する。より詳細な記述を以下に行う。
【００２６】ブロック１０内での反復が各々成功したと
いう結論を出すと、ブロック１３内のスペシフィケーシ
ョンはブロック１５に転送され、ブロック１５内のシス
テム定義情報は確認ブロック２０に渡される。上述され
ているように、ブロック２０は、ブロック１５内に保持
されているシステム定義が当該システムに係る必要なタ
スクを適切に実行することが可能であることを確認す
る。ユーザはタスク定義をブロック２３に入力する。ブ
ロック２４は、図２に示された解析／開発装置が、前記
タスクが適切に実行されているか否かを評価することを
許可するユーザ還元情報を受容する。より具体的に述べ
れば、ユーザはタスク定義をブロック２３に、かつ還元
マッピングをブロック２４に供給する。各々の還元Ｒｉ
はタスクＴｉに関連している。タスクＴｉに関して、シ
ステム動作の正しさは、タスクが還元Ｒｉによって定義
された還元版によって実行されるか否かを決定すること
によって確認される。
【００２７】ブロック２４における還元はブロック１５
によって与えられるシステム定義とともに確認される。
確認は還元確認ブロック２５において実行される。確認
は、一度に一つのタスクに関してなされる。すなわち、
各々の還元は、それが有効な還元であるか否か、すなわ
ち当該還元が還元されたシステムを前記タスクとともに
不変に保つか否か、を決定するためにテストされる。同
時に、前記タスクは、ブロック２６において、その還元
されたシステムに関して前記タスクが適切に実行され得
ることを決定するためにテストされる。ブロック２５あ
るいはブロック２６においてエラーが検出された場合に
は、ステータスライン２１がユーザに対して、ユーザが
システム定義、規定されたタスク、あるいは前記還元を
修正することを可能とする診断メッセージを提供する。
エラーが検出されない場合には、本発明に係る処理は次
のタスク及び対応する還元マッピングに進み、全てのタ
スクがテストを通過するまで反復される。各々の還元マ
ップの確認に関して実行される実際のテストは、システ
ム改善（ブロック１４）に関するマッピングを確認する
際に実行されるテストと同一のものである。すなわち、
数学的には、（あるタスクに関連して）システム還元と
還元されていないシステムとの間の関連は、ブロック１
５内のシステム定義とブロック１３内の改善されたシス
テム定義との間の関連と非常に似ている。ある文献にお
いては、これらのマッピングは”ホモモルフィズム”と
呼称される。
【００２８】ブロック２５において還元が確認される
と、ブロック２６は規定された各々のタスクが還元され
たシステムによって適切に実行されるか否かを決定す
る。ブロック２５での確認は、タスクが還元されたシス
テムによって実行されるならばそれらは還元されていな
いシステムによっても実行されるということを保証す
る。もちろん、還元されたシステムをチェックするのに
は実質的に少しの時間しかかからない。タスクがシステ
ムによって実行されることをチェックするためのアルゴ
リズムは多数存在する。これらのアルゴリズムの一例
が、アール・ピー・カーシャン（Ｒ．Ｐ．Ｋｕｒｓｈａ
ｎ）による”コーディネーションの解析に関する還元可
能性”という表題の記事（”離散事象システム：モデル
及びその応用”（レクチャー・ノート・イン・コンピュ
ータ・サイエンス（ＬＮＩＣＳ） １０３、シュプリン
ガー・フェアラーク（Ｓｐｒｉｎｇｅｒ Ｖｅｒｌａ
ｇ）、１９８７年）、第１９−３９頁）に記載されてい
る。ある文献においては、これらのアルゴリズムは”言
語閉じ込め”アルゴリズムと呼称されている。
【００２９】全てのタスクの解析が成功された場合に
は、ステータスライン２１がユーザに本発明にかかる反
復が完了したことを知らせる。その後、ユーザは次の反
復に進む。ユーザは（ブロック１０に対して）システム
の改善を供給し、当該改善されたシステムによって実行
さるべきタスクのより総合的な組及び当該新たなタスク
の組をテストする還元を規定する。
【００３０】既に記述されているように、図２に示され
た装置はテスト機能を実行し、テストを通った場合の最
終的な結果は、規定されたタスクの全てを実行するため
に、すなわち、目的とする全ての出力信号が種々の可能
な入力信号に対して生成され得るのに必要な程度まで詳
細になった、ブロック１５内のスペシフィケーションで
ある。この時点で、コード生成器３０が有限状態マシン
をインプリメントするための実際のコードを生成するこ
とになる。このコードは、当該有限状態マシンを実現す
るストアード・プログラム制御プロセッサへのインスト
ールを目的としたものであることも可能であり、特定目
的のハードウエアによる実現に対して必要とされる情報
を生成する段階への入力となるものである場合もある。
この種の情報は、例えば、集積回路実現における種々の
素子間の接続を規定する”ネットリスト”であり得る。
ネットリストは目的とするＦＳＭを生成するために直接
用いられ得るものであり、あるいは目的とするＦＳＭを
実現する集積回路を製造するために用いられる一つのあ
るいは複数個のマスクに変換され得る。
【００３１】ブロック１４、２５及び２６において実行
されるベリフィケーションに関する詳細な事項をさらに
追加する前に、前述されている原理に従った一般的な実
施例について考えることは意味があると思われる。
【００３２】図４は、そのデザインが本発明の原理に従
って形式的に開発されかつ確認されるコントローラのブ
ロック図である。当該ブロック図には、ＣＰＵ１００及
びパケットレイヤーコントローラ（ＰＬＣ）２００が含
まれている。ＣＰＵ１００は、バスマネージャ１１０、
インターフェースドライバ１２０及びアプリケーション
１３０を有している。ＰＬＣ２００は、ジェネラルマネ
ージャ２１０、管理ブロック２２０、タスクマネージャ
２３０、リスタートブロック２４０、レシーバ２５０、
センダ２６０、タイマ２７０、タスクキューブロック２
８０、及びＲＯＭマネージャ２９０を有している。さら
に、ＰＬＣには、入力及び出力キュー３１０−３７０及
びＲＯＭ３８０が接続されている。
【００３３】アプリケーションブロック１３０が実行さ
せる必要があるタスクの内の一つが”ｅｎｑｕｅ−ｍｓ
ｇ”タスクである。当該タスクにおいては、アプリケー
ションは”ｅｎｑｕｅ−ｍｓｇ”トークンを出力し、出
力メッセージキュー、すなわちキュー３３０、にメッセ
ージを出力する。”ｅｎｑｕｅ−ｍｓｇ”トークンはド
ライバ１２０によって翻訳され、コマンドキュー３７０
へ送られる。同時に、タスクマネージャ２７０は、コマ
ンドキューに翻訳されたトークンが挿入されたことを知
らされる。タスクマネージャはコマンドキューから当該
キューに挿入されたメッセージを読み出し、それをタス
クキュー２８０に移してさらにセンダ２６０に送る。セ
ンダは、ＲＯＭマネージャ２９０及びジェネラルマネー
ジャ２１０を介してＲＯＭ３８０内のプロトコルをアク
セスする。ジェネラルマネージャ２１０はＲＯＭ内及び
プロトコルに従って”ｅｎｑｕｅ−ｍｓｇ”タスクのプ
ロセシングを行なうシステムバス内のコンフリクト（衝
突）を制御する。ジェネラルマネージャは、最終的に
は、出力メッセージキューからデータをリンク上に移動
する。
【００３４】タスクを確認するために、図４に示された
システムの複雑さを還元することが必要である。なぜな
ら、当該システムは余りにも複雑だからである。すなわ
ち、当該システムが効率的な確認を可能にするために仮
定する状態が（計算に係る労力という観点からは）多す
ぎる、ということである。還元の目的は、前記システム
における、”ｅｎｑｕｅ−ｍｓｇ”タスクとの相互作用
を有さない部分を抽象化し、センダ及び他のコンポーネ
ントと相互作用しかつそれ以外では前記タスクに関して
はプロアクティブであるようなより単純なブロックの組
に前記部分を還元することである。それらの相互作用す
なわち干渉が少なくとも実際のコンポーネントと同程度
である場合には、”ｅｎｑｕｅ−ｍｓｇ”タスクが還元
されたシステムにおいて実行されるという証明は、当該
タスクが還元される以前のシステムにおいても実行され
ることを保証する。可能な還元の一例は、例えば、ブロ
ック３１０、３２０、３５０、３６０、２２０、２７
０、２４０、２５０、２９０を包含している。他方、こ
のような急激な還元でさえも充分に包含しているとは限
らない。
【００３５】用いられる解の一例は、”ｅｎｑｕｅ−ｍ
ｓｇ”タスクを３つのサブタスクに分解することであ
る。第一のサブタスクは、アプリケーションが”ｅｎｑ
ｕｅ−ｍｓｇ”を送出した際に”ｅｎｑｕｅ−ｍｓｇ”
トークンがコマンドキューに到達していることを確認す
る。第二のサブタスクは、”ｅｎｑｕｅ−ｍｓｇ”トー
クンがコマンドキューにあることを仮定して、タスクマ
ネージャが当該トークンを適切にセンダに渡すことを確
認する。第三のサブタスクは、”ｅｎｑｕｅ−ｍｓｇ”
がセンダにあることを仮定して、センダがリンクへのデ
ータ転送を適切に実行することを確認する。各々のサブ
タスクを確認するために、前記システムのより広い部分
が還元されたシステムに含まれる。その後、還元された
より簡潔なシステムが解析されてサブタスクがより容易
に確認される。もちろん、サブタスクを実行することが
元の”ｅｎｑｕｅ−ｍｓｇ”タスクを実行することと等
価であることを証明する、実行されなければならない付
加的な確認ステップも存在する。
【００３６】ブロック１４において実行されるベリフィ
ケーションに戻ると、既に記述されているように、ブロ
ック１５におけるシステムスペシフィケーションとブロ
ック１３におけるより改善されたシステムスペシフィケ
ーションとの関係はマッピング（ホモモルフィズム）に
よって規定される。改善されたより複雑なスペシフィケ
ーションがより複雑でないスペシフィケーションとコン
システントであることを確認するためには、選択ｘによ
って可能とされる前記より複雑なシステムにおける状態
ｖから状態ｗへの遷移が存在しかつ前記マッピングによ
ってｖがｖ’へ、ｗがｗ’へ、及びｘがｘ’へそれぞれ
マッピングされる場合には、ｖ’からｗ’への遷移が
ｘ’によって可能とされなければならない、ということ
をテストすることが必要である。
【００３７】前記ｓ／ｒモデルが前述の評価を行なうた
めに用いられる。簡潔に述べれば、ｓ／ｒモデルは、全
体の有限状態マシンを形成するように統合される個々の
有限状態マシンに係るグローバルな選択、グローバル状
態、及び多重度を考慮することによって説明される。こ
のモデルに係る各々の反復において、個々の有限状態マ
シンの各々はそれらの現時点での状態で可能な出力の内
からある出力を選択し、それによってグローバルな選択
に寄与する。そののち、当該グローバル選択を考慮し
て、全体の有限状態マシンが進むであろう状態へ移行す
る。この反復は、無限に続けられる。
【００３８】本発明に従って、前記ｓ／ｒモデルが所
謂”クランクマシン”における確認を目的としてインプ
リメントされる。当該マシンは、統合される個々の有限
状態マシンの多重度に対応する多重個のモジュール、及
び４つの段階を通じて反復する手段を有している。前述
されている選択段階及び状態へ解決する段階（これらは
クランクマシンの第２及び第３段階に相当する）の２つ
の段階に加えて、クランクマシンはレジスタから得られ
たグローバル状態を分割してそれらを個々の有限状態マ
シンに与える第１段階、及び、新たなグローバル状態を
生成してそれをレジスタにストアする第４段階を有して
いる。レジスタは個々の有限状態マシン間の通信インタ
ーフェースとして機能し、有限状態マシン間で必要とさ
れる相互作用を提供する。個々の有限状態マシンはグロ
ーバル状態に応答して、新たなグローバル状態の生成に
寄与する。
【００３９】もちろん、システムスペシフィケーション
の種々の状態間を循環する機能だけを有することは、シ
ステムスペシフィケーションをテストする目的には不充
分である。可能な状態及び選択の全ての間を実際に循環
する手段が与えられなければならない。ここで、システ
ムは、与えられた状態にある場合にいくつかの選択を有
しており、かつ、その逆に、各々の選択に対してはいく
つかの状態の内の一つへの解がある、ということに留意
されたい。
【００４０】システムスペシフィケーションをテストす
るために、前記実施例においては、図５に示されている
ように、境界キューメモリ６１、到達状態テーブル（Ｒ
ＳＴ）６２、及びクランクマシンコントローラ６３が用
いられる。境界キューは上部及び下部よりアクセスされ
得るスタックであり、ＲＳＴ内のシステムの状態を指し
示すグローバル状態ポインタを保持している。クランク
マシンコントローラ（ソフトウエア制御コントローラ）
は、境界キューの上部から状態をポップ（復帰）し、当
該状態を分解して個々の有限状態マシンを表わす種々の
モジュールに与える。そののち、当該コントローラは可
能な選択の全てを生成し、各々の選択に対してその次の
可能な状態を生成する。生成された次の状態の各々に関
して、クランクマシンは当該状態が既にＲＳＴ内に存在
するか否かを決定する。それがＲＳＴ内に存在しない場
合には、クランクマシンは当該状態をＲＳＴに追加し、
ＲＳＴ内に挿入された状態の位置を指し示すポインタを
境界キュー内に挿入する。ポインタは、受容基準の値に
基づいて、境界キューの上部あるいは境界キューの下部
に挿入される。より詳細に述べれば、ポインタは、前記
状態へのアクセスが”リカー（再帰）”エッジを横断す
るものであると決定された場合に前記スタックの上部に
挿入される。この概念は、アール・ピー・カーシャンに
よる前述のＬＮＩＣＳにおける論文において見いだされ
る。
【００４１】前述されているプロセスは、基本的には図
６に示された流れ図に従っている。ブロック５１におい
て、状態はバッファキューから分解される。ブロック５
２においては、未だになされていない選択がシステム中
に存在するか否かが決定される。その答えが肯定的であ
る場合には、ブロック５３において選択がなされ、制御
はブロック５５に移行する。その他の場合には、制御は
ブロック５１へ戻り、他のシステム状態がクランクマシ
ンによってポップされ、分解される。
【００４２】ブロック５４においては、それ以前に識別
されておらずかつ（なされた選択に基づいて）当該シス
テムが移行し得る状態が存在するか否かが決定される。
その答えが肯定的な場合は、ブロック５５は前記状態へ
還元し、ブロック５６が還元された状態をパックして境
界キュースタックへプッシュする。さらに還元される状
態がない場合は、制御はブロック５２へ戻って新たな選
択がなされる。
【００４３】図６におけるブロック５６は、前記パック
された状態を境界キュースタック６１の上部にプッシュ
するべきかあるいは下部にプッシュするべきかの決定を
行なうロジックが含んでいる。ブロック５２は、個々の
有限状態マシンによってなされた種々の選択を通じての
循環を行なうロジックが含んでいる。
【００４４】クランクマシンコントローラ内のモジュー
ルは、個々の有限状態マシンに対応している。本発明に
従って、これらのモジュールは前記Ｓ／Ｒ言語スペシフ
ィケーションをコンパイルすることによって生成され
る。本発明に係るコンパイラは、前記スペシフィケーシ
ョンを表１のＣライクなコードによってその概略が示さ
れているようなストラクチャを有するスイッチ動作ステ
ートメントの集合に変換する。表１はその概略のみを例
示したものであり、正確であることを意図したものでは
ない。表１０ー３４に表わされているコード”ｃｃｏｄ
ｅ．ｃ”を実行することにより、表１が表現している実
際のコードを開発するために必要なその詳細の全てが与
えられる。表１は、ブロック５２及び５４における結果
を全ての可能な選択とそれ以降のケースステートメント
に存在する全ての可能な状態とを通じて循環することに
関して記録しておくために設定された”セット状態ベク
トル”を含んでいる。表１は、さらに、各々の動作ステ
ートメントとともにそれらに対になるエラーステートメ
ントも有している。エラーステートメントエントリは、
希望するベリフィケーションを遂行するために実行され
るテストを表現している。この種のテストの一例が安定
性テストである。安定性をテストするためには、前記ス
ペシフィケーションが連続した時間非同期システム定義
とコンシステントであることを決定しなければならな
い。この安定性問題の理論的取扱いは、公表されること
になっている記事においてなされている。安定性テスト
を実行するためのコードはＶ（Ｖ）４表３５ー３６に与
えられている。ここで、表１は図２のブロック３０によ
って生成された、確認ブロック及び信号の組において用
いられるコードのストラクチャを示し、個々の有限状態
マシンの内の一つしか表わしておらず、以上に議論され
た状態及び選択はグローバル選択及びグローバル状態に
関連するものであることに留意されたい。
【００４５】以上に記述されたものは、種々の可能な状
態と種々の可能な選択とを通じての循環プロセスであ
る。ブロック１４のベリフィケーションを実行するため
に、前述のプロセスがブロック１３のスペシフィケーシ
ョンとブロック１５のスペシフィケーションの双方に対
して適応される。前記プロセスは双方のシステムに対し
て同時に適応され、各々のステップにおいて、ブロック
１３のシステムが選択ｘによって可能とされる状態ｖか
ら状態ｗへの遷移を経験し、ブロック１５のシステムが
選択ｘ’に従ってｖ’からｗ’への遷移を経験する際
に、ｖ’、ｗ’、及びｘ’がブロック１３のマッピング
によってｖ、ｗ、及びｘに関連していることを確認する
決定がなされる。
【００４６】上述されているように、ブロック２５に係
るベリフィケーションプロセスはブロック１４における
プロセスと同種のものであり、それゆえ、それについて
はここでは言及しない。
【００４７】コード生成器（ブロック３０）に関して
は、当該コード生成器は基本的にはブロック１４のベリ
フィケーションプロセスにおいて生成されたものと同一
のスイッチステートメントの集合を生成する。唯一の差
異は、全ての可能な状態を通じて循環するためのスイッ
チステートメントに含まれているテストサブモジュール
が、例えば、除去されていることである。もちろん、表
１に示された例における”エラーステートメント”エン
トリも除去されている。その結果、コード生成器は関数
やサブルーチンの呼び出しを含まないコードを生成す
る。全ての決定は、スイッチステートメントの一つの”
レベル”上でなされる。その結果、コード生成器によっ
て生成されたコードパッケージに対応する信号の組が目
的とするマシン（プロセッサ−メモリの組合せ）におい
てインストールされると、それによって得られる有限状
態マシンは非常に高速となる。コード生成器３０の信号
セットとともに生成される有限状態マシンと他の手段に
よって生成される有限状態マシンとの差異は、あるアル
ゴリズムに従って積を計算するプロセッサによって構成
されている乗算器とルック・アップ・テーブルを有して
いる乗算器との速度の差異に類似のものである（本発明
に係る有限状態マシンがルック・アップ・テーブル型乗
算器により類似している）。
【００４８】ブロック３０によって生成されたコードは
有限状態マシンの集合を形成する。本発明に従って、こ
この有限状態マシンの種々のサブセットを対応する単一
の有限状態マシンにマージすることにより、よりよいも
のが得られる。現実には、このことは、複数個のスイッ
チステートメントを単一のスイッチステートメントにま
とめることを意味する。この種のマージを行なうことは
困難ではない；すなわち、ソフトウエアにおけるメモリ
の消費が増加することで実行時間を減少させるという効
果を認識すればよいのである。
【００４９】マージングによるコード長の増加の効果は
ブロック３０において実行される他のステップ、すなわ
ち種々のマージされたマシンの各々に係る還元ステップ
によって改善される。この還元の概念は新しいものでは
ない。従来技術に係る有限状態マシン還元アルゴリズム
は、可能な入力値の全てを見てシステムがそれらの入力
に対して応答することを可能にするようシステムを還元
するものである。還元は前記可能な入力に係る制限によ
って生ずるものである。例えば、ジェイ・イー・ホップ
クロフト（Ｊ．Ｅ．Ｈｏｐｃｒｏｆｔ）による、”マシ
ン及び計算の理論”（コハビ（Ｋｏｈａｖｉ）、パズ
（Ｐａｚ）編、アカデミック・プレス（Ａｃａｄｅｍｉ
ｃ Ｐｒｅｓｓ））第１８９−１９６頁の”有限オート
マトンにおける状態の最小化に係るｎｌｏｇｎアルゴリ
ズム”という表題の記事を参照。本発明に係る還元は、
ＦＳＭの”種々の状態において”可能な入力を見る、と
いう点が改良されている。状態の全てにおいて全ての入
力が可能であるわけではないので、個々の状態を考慮す
ることによって到達し得る還元は従来技術によって可能
なものよりも実質的に大きいものである。
【００５０】まとめると、アナライザ／デベロッパスト
ラクチャが機能する方法は、ユーザが全体的なアーキテ
クチャ、個々の機能、及びタスクを規定することであ
る。その後、アナライザ／デベロッパはタスクが実行さ
れ得ることを確認し、ユーザがシステム定義及び当該改
善されたシステムにおいて実行されるタスクを反復して
改善することを可能にする。
【００５１】本発明に係るトップ・ダウン逐次改善法と
従来技術に係る方法との差異は、従来技術に係る方法
が、一度に一つ、その内部で完全な機能を有するモジュ
ールを生成する、ということである。新たなモジュール
が追加されると、システムに対して新たな振舞いが追加
される。他方、本発明に従って、システム全体が最初か
ら定義される；すなわち、最初は非常に抽象的なレベル
においてであり、後にはより詳細さを増したレベルにお
いてである。最も高次のレベルにおいてはシステムが非
常に抽象的であるため、データのシンタクスの修正のチ
ェックに付随するもの等の低レベルの問いは決定されず
に放置される。例えば、高レベルスペシフィケーション
においては、特定のメッセージは良好なシンタクスある
いは不良なシンタクスを決定されずに持ち得る。双方と
もが可能である。これが、システムのそれ以降のレベル
において改善され、シンタクスが決定されて特定のメッ
セージが良好なシンタクスあるいは不良なシンタクスの
いずれかのみを有するような条件が得られるかがチェッ
クされる。
【００５２】別な見方をすれば、本発明に従って振舞い
は追加されるのではなくむしろ除去される。この違いは
特に際だったものである。なぜなら、システムが開発さ
れている間に当該システムについて何か証明できると期
待するならば、システムの振舞いが追加される場合には
当該振舞いについての証明することは不可能であるから
である。その理由は、個々のシステムについて何らかの
証明がなされ、その後に振舞いが追加された場合、もは
やそれ以前に証明された命題が依然として成立するか否
かを知ることが不可能であるからである。他方、振舞い
が除去されかつ当該抽象的なシステムの全ての振舞いが
満足し得るものであることが証明されている場合には、
より少ない数の振舞いしか有さない改善されたシステム
に関しては当該事実は確実に真で有り続けるからであ
る。結果として、本発明に係る方式の重要な利点の一つ
は、ユーザが基本的な設計エラーを、個々のシステムの
全ての場合についての論拠付けが完了することを待つこ
となく、開発の非常に初期の段階において検出すること
が可能になることである。
【００５３】以上の説明は、本発明の一実施例に関する
もので，この技術分野の当業者であれば、本発明の種々
の変形例が考え得るが、それらはいずれも本発明の技術
的範囲に包含される。
【発明の効果】以上述べたごとく、本発明によれば、フ
ォーマルベリフィケーションに基づいて、制御指向シス
テムの有限状態マシンによるインプリメンテーションが
自動的に短時間の内になされる。
【表１】
【表２】
【表３】
【表４】
【表５】
【表６】
【表７】
【表８】
【表９】
【表１０】
【表１１】
【表１２】
【表１３】
【表１４】
【表１５】
【表１６】
【表１７】
【表１８】
【表１９】
【表２０】
【表２１】
【表２２】
【表２３】
【表２４】
【表２５】
【表２６】
【表２７】
【表２８】
【表２９】
【表３０】
【表３１】
【表３２】
【表３３】
【表３４】
【表３５】
【表３６】
【図面の簡単な説明】
【図１】本発明に係る分析／開発装置の全体を表わすブ
ロック図。
【図２】図１に示したブロック図の詳細を示す図。
【図３】本発明に係る分析／開発法において用いられた
同型概念（ホモモルフィズム・コンセプト）を示す図。
【図４】本発明に係るプロトコル装置及び適用されるタ
スク関連還元を示す図。
【図５】本発明に係る”クランクマシン”の実施例の全
体を表わすブロック図。
【図６】本発明に係る、選択及び状態を通じての循環を
表わす流れ図。

Claims (30)

    【特許請求の範囲】
  1. 【請求項１】 シーケンシャル回路を生成する方法にお
    いて、当該シーケンシャル回路に対するスペシフィケー
    ション及びタスクを受信する段階；前記シーケンシャル
    回路が前記スペシフィケーションに従う場合前記回路に
    おいて前記タスクが実行可能であるか否かをテストする
    段階；前記スペシフィケーションに係る詳細な情報を追
    加することによって改善されたスペシフィケーションを
    形成しかつ実行さるべき新たなタスクを決定する段階；
    前記改善されたスペシフィケーションが前記与えられた
    スペシフィケーションの振舞いを保存していることを形
    式的に確認する段階；この際、前記回路が前記改善され
    たスペシフィケーションに従う場合前記回路の入力信号
    に対する応答は、前記回路が前記与えられたスペシフィ
    ケーションに従う場合の同一の入力信号に対する応答と
    コンシステントである；前記タスクを前記新たなタスク
    と置換しかつ前記スペシフィケーションを前記改善され
    たスペシフィケーションと置換し、前記テスト段階へ戻
    る段階；及び、前記シーケンシャル回路を実現するため
    に、前記スペシフィケーションに基づいてストラクチャ
    情報を開発・伝達する段階；よりなることを特徴とする
    シーケンシャル回路生成方法。
  2. 【請求項２】 与えられたタスクを実行するシーケンシ
    ャル回路を生成する方法において、前記シーケンシャル
    回路のスペシフィケーションをアナライザに入力する段
    階；前記アナライザに対して前記スペシフィケーション
    に欠けていた詳細な情報を追加することによって改善さ
    れたスペシフィケーションを生成する段階；前記改善さ
    れたスペシフィケーションが前記スペシフィケーション
    の振舞いを保存していることを形式的に確認する段階；
    この際、前記回路が前記改善されたスペシフィケーショ
    ンに従う場合前記回路の入力信号に対する応答は、前記
    回路が前記スペシフィケーションに従う場合の同一の入
    力信号に対する応答とコンシステントである；前記スペ
    シフィケーションを前記改善されたスペシフィケーショ
    ンと置換し、前記生成段階へ戻る段階；及び、前記シー
    ケンシャル回路を実現するために、前記アナライザから
    前記スペシフィケーションに基づいてストラクチャ情報
    を開発・伝達する段階；よりなることを特徴とするシー
    ケンシャル回路生成方法。
  3. 【請求項３】 前記テスト段階が、改善されたスペシフ
    ィケーションの生成を終了するか否かを決定するために
    テストすることを含むことを特徴とする請求項１に記載
    の方法。
  4. 【請求項４】 さらに、前記ストラクチャ情報を集積回
    路の接続パターンに関して用いる段階を有することを特
    徴とする請求項２に記載の方法。
  5. 【請求項５】 さらに、前記ストラクチャ情報を集積回
    路のレイアウトに組み込む段階を有することを特徴とす
    る請求項２に記載の方法。
  6. 【請求項６】 前記ストラクチャ情報が、前記シーケン
    シャル回路を実現するプロセッサを制御する制御信号シ
    ーケンスを有することを特徴とする請求項２に記載の方
    法。
  7. 【請求項７】 前記制御信号が、ストアード・プログラ
    ム・プロセッサを制御するために適応されていることを
    特徴とする請求項６に記載の方法。
  8. 【請求項８】 前記制御信号が複数個のモジュールを形
    成し、各々のモジュールが前記ストアード・プログラム
    ・プロセッサの入力及び出力機能を制御するモジュール
    のみを参照して生成されたスイッチステートメントを形
    成することを特徴とする請求項７に記載の方法。
  9. 【請求項９】 与えられたスペシフィケーションに従っ
    て与えられたタスクを実行するシーケンシャル回路を生
    成する方法において、前記与えられた各々のタスクに対
    する還元されたスペシフィケーションを形成するために
    各々のタスクに対して与えられた前記スペシフィケーシ
    ョンの還元されたものを規定する段階；前記還元された
    各々のスペシフィケーションが前記タスクに関して前記
    与えられたスペシフィケーションを包摂しかつ対応する
    タスクを不変にしていることをテストする段階；各々の
    タスクをテストして当該テストされたタスクに対応する
    還元されたスペシフィケーションに従う回路において当
    該テストされたタスクが実行可能であることを決定する
    段階；前記シーケンシャル回路を実現するために、前記
    与えられたスペシフィケーションに基づいてストラクチ
    ャ情報を開発・伝達する段階；よりなることを特徴とす
    るシーケンシャル回路生成方法。
  10. 【請求項１０】 さらに、前記ストラクチャ情報を集積
    回路の接続パターンに関して用いる段階を有することを
    特徴とする請求項９に記載の方法。
  11. 【請求項１１】 さらに、前記ストラクチャ情報を集積
    回路のレイアウトに組み込む段階を有することを特徴と
    する請求項９に記載の方法。
  12. 【請求項１２】 前記ストラクチャ情報が、前記シーケ
    ンシャル回路を実現するプロセッサを制御する、前記与
    えられたスペシフィケーションに基づく制御信号シーケ
    ンスを有することを特徴とする請求項９に記載の方法。
  13. 【請求項１３】 前記制御信号が、ストアード・プログ
    ラム・プロセッサを制御するために適応されていること
    を特徴とする請求項１２に記載の方法。
  14. 【請求項１４】 前記制御信号が複数個のモジュールを
    形成し、各々のモジュールが前記ストアード・プログラ
    ム・プロセッサの入力及び出力機能を制御するモジュー
    ルのみを参照して生成されたスイッチステートメントを
    形成することを特徴とする請求項１３に記載の方法。
  15. 【請求項１５】 シーケンシャル回路を生成する方法に
    おいて、アナライザに回路スペシフィケーション及びタ
    スクを入力する段階；前記シーケンシャル回路が前記ス
    ペシフィケーションに従う場合前記シーケンシャル回路
    において前記タスクが実行可能であるか否かをテストす
    る段階；前記スペシフィケーションに係る詳細な情報を
    前記アナライザに追加することによって改善されたスペ
    シフィケーションを形成しかつ実行さるべき新たなタス
    クを決定する段階；前記改善されたスペシフィケーショ
    ンが前記スペシフィケーションの振舞いを保存している
    ことを形式的に確認する段階；この際、前記回路が前記
    改善されたスペシフィケーションに従う場合前記回路の
    入力信号に対する応答は、前記回路が前記スペシフィケ
    ーションに従う場合の同一の入力信号に対する応答とコ
    ンシステントである；前記タスクを前記新たなタスクと
    置換しかつ前記スペシフィケーションを前記改善された
    スペシフィケーションと置換し、前記テスト段階へ戻る
    段階；前記各々のタスクに対する還元されたスペシフィ
    ケーションを形成するために各々のタスクに対する前記
    スペシフィケーションの還元されたものを規定する段
    階；前記還元されたスペシフィケーションをテストして
    前記還元された各々のスペシフィケーションが前記タス
    クに関して前記与えられたスペシフィケーションを包摂
    しかつ対応するタスクを不変にしていることを決定する
    段階；各々のタスクをテストして当該テストされたタス
    クに対応する還元されたスペシフィケーションに従う回
    路において当該テストされたタスクが実行可能であるこ
    とを決定する段階；前記シーケンシャル回路を実現する
    ために、前記スペシフィケーションに基づいて前記アナ
    ライザからストラクチャ情報を開発・伝達する段階；よ
    りなることを特徴とするシーケンシャル回路生成方法。
  16. 【請求項１６】 与えられたスペシフィケーションに従
    うシーケンシャルマシンを生成する方法において、前記
    マシンがタスクを実行し、前記シーケンシャル回路のス
    ペシフィケーションの改善したものを開発して改善され
    たスペシフィケーション候補を形成し前記シーケンシャ
    ルマシンによって実行さるべきタスクを規定する段階；
    前記生成むされたスペシフィケーション候補が前記与え
    られたスペシフィケーションに包摂されている及び前記
    シーケンシャルマシンが前記改善されたスペシフィケー
    ション候補に従う場合に前記タスクが前記マシンによっ
    て実行可能である、という主張をテストする段階；前記
    テスト段階が前記主張を拒絶した場合に前記改善された
    スペシフィケーション候補及び前記タスクを修正する段
    階；前記テスト段階が前記主張を受容した場合に前記与
    えられたスペシフィケーションを前記改善されたスペシ
    フィケーション候補で置換し前記改善開発段階へ戻る段
    階；よりなることを特徴とするシーケンシャルマシン生
    成方法。
  17. 【請求項１７】 前記テスト及び修正段階が、前記改善
    が前記改善されたスペシフィケーション候補によって包
    摂されているという主張を確認するために前記改善をテ
    ストする段階；前記改善テスト段階が前記主張を拒絶し
    た場合に前記改善におけるエラーを修正する段階；前記
    タスクが前記改善によって実行されるという主張を確認
    するためにタスクをテストする段階；前記タスクテスト
    段階が前記主張を拒絶した場合に前記改善及び前記タス
    クにおけるエラーを修正する段階；よりなることを特徴
    とする請求項１６に記載の方法。
  18. 【請求項１８】 前記タスクが前記改善によって実行さ
    れるという主張をテストする前記段階が、前記タスクが
    前記スペシフィケーション候補に関する還元されたスペ
    シフィケーションによって実行されるという主張をテス
    トする段階よりなることを特徴とする請求項１７に記載
    の方法。
  19. 【請求項１９】 さらに、前記還元されたスペシフィケ
    ーションをテストして前記還元されたスペシフィケーシ
    ョンの振舞いが前記改善されたスペシフィケーション候
    補の振舞いを包摂していることを決定する段階を有する
    ことを特徴とする請求項１８に記載の方法。
  20. 【請求項２０】 前記改善を規定する段階が、与えられ
    た可能な入力信号及び目的とする出力信号の組に対し
    て、前記スペシフィケーション候補が前記入力信号を処
    理するのに充分なものでありかつ前記目的とする出力信
    号の全てを生成する場合に終了することを特徴とする請
    求項１６に記載の方法。
  21. 【請求項２１】 前記方法が、さらに、前記シーケンシ
    ャルマシンを実現する制御信号の組を生成する段階を有
    することを特徴とする請求項１６に記載の方法。
  22. 【請求項２２】 前記制御信号の組を生成する段階が、
    ストアード・プログラム・コントローラを制御するイン
    ストラクションシーケンスを生成する段階を有すること
    を特徴とする請求項２１に記載の方法。
  23. 【請求項２３】 前記方法が、さらに、前記インストラ
    クションをストアード・プログラム・コントローラに組
    み込む段階を有することを特徴とする請求項２２に記載
    の方法。
  24. 【請求項２４】 与えられたタスクを実行するシーケン
    シャル回路において、当該回路はストアード・プログラ
    ム・プロセッサ及びメモリを有し、前記与えられたタス
    クを実行するために本質的な部分を有する信号の組が前
    記メモリにストアされており、前記部分が複数個のモジ
    ュールよりなり、各々のモジュールが前記ストアード・
    プログラム・プロセッサの入出力機能を制御するモジュ
    ールのみを参照するようにして構築されたスイッチを形
    成していることを特徴とするシーケンシャル回路。
  25. 【請求項２５】 プロセッサと相互作用して有限状態マ
    シンを形成するコントローラにおいて、当該コントロー
    ラは入出力ポートを有しかつ前記入力ポートにおける入
    力信号及び前記有限状態マシンの状態に従って前記出力
    ポートに予め選択された応答を出力し、当該コントロー
    ラが、前記予め選択された応答を実現するための実行プ
    ログラム、及び前記実行プログラムをストアするメモリ
    を有し、前記実行プログラムの一部が前記選択された応
    答を実現するために本質的なものであり、前記実行プロ
    グラムがスイッチ構造を含み、前記スイッチ構造の全て
    のブランチが、前記入力ポート及び前記出力ポートと相
    互作用する以外の機能に対する呼び出しを排除する組か
    ら厳密に選択されたコマンドを有していること、を特徴
    とするコントローラ。
  26. 【請求項２６】 有限状態マシンを形成する装置におい
    て、当該装置は入出力ポートを有しかつ前記入力ポート
    における入力信号及び前記有限状態マシンの状態に従っ
    て前記出力ポートに予め選択された応答を出力し、当該
    装置が、前記予め選択された応答を実現するための実行
    プログラム、前記実行プログラムをストアするメモリ、
    及び前記メモリ及び前記入力ポート及び前記出力ポート
    に対して接続されたプロセッサを有し、前記実行プログ
    ラムの一部が前記選択された応答を実現するために本質
    的なものであり、前記実行プログラムがスイッチ構造を
    含み、前記スイッチ構造の全てのブランチが、前記入力
    ポート及び前記出力ポートと相互作用する以外の機能に
    対する呼び出しを排除する組から厳密に選択されたコマ
    ンドを有していること、を特徴とする有限状態マシン装
    置。
  27. 【請求項２７】 前記実行プログラムが、スイッチ構造
    連鎖を有し、各々のスイッチ構造が前記組から厳密に選
    択されたコマンドを有するブランチを有していることを
    特徴とする請求項２６に記載の装置。
  28. 【請求項２８】 複数個の相互作用する有限状態マシン
    から構成され入力ポート及び出力ポートを有するシーケ
    ンシャルマシンにおいて、当該マシンが、前記入力ポー
    トにおける入力信号に対する前記出力ポートにおける前
    記マシンの選択された応答を実現するための実行プログ
    ラム、前記実行プログラムをストアするメモリ、及び前
    記メモリ及び前記入力ポート及び前記出力ポートに対し
    て接続されたプロセッサを有し、前記実行プログラムが
    前記相互作用する有限状態マシンの各々に対するスイッ
    チ構造を含み、前記選択された応答を実現するために本
    質的な前記スイッチ構造の全てのブランチが、前記入力
    ポート及び前記出力ポートと相互作用する以外の機能に
    対する呼び出しを排除する組から厳密に選択されたコマ
    ンドを有していること、を特徴とするシーケンシャルマ
    シン。
  29. 【請求項２９】 前記スイッチ構造が連結されているこ
    とを特徴とする請求項２８に記載のマシン。
  30. 【請求項３０】 与えられたタスクを実行するシーケン
    シャル回路において、当該回路は協同するモジュールを
    有し、各々のモジュールのストラクチャが反復して適応
    される方法に従って構成されたスイッチ構造を形成して
    おり、前記方法が、与えられたスペシフィケーションを
    形成する回路スペシフィケーションを生成する段階；前
    記シーケンシャル回路が前記与えられたスペシフィケー
    ションに従う場合前記タスクが前記回路において実行可
    能であるか否か、及び改善されたスペシフィケーション
    を形成する段階へ進むか否か、をテストする段階；前記
    スペシフィケーションに係る詳細な情報を追加すること
    によって改善されたスペシフィケーションを形成しかつ
    実行さるべき新たなタスクを決定する段階；前記改善さ
    れたスペシフィケーションが前記与えられたスペシフィ
    ケーションの振舞いを保存していることを確認する段
    階；この際、前記回路が前記改善されたスペシフィケー
    ションに従う場合前記回路の入力信号に対する応答は、
    前記回路が前記与えられたスペシフィケーションに従う
    場合の同一の入力信号に対する応答と一致している；前
    記タスクを前記新たなタスクと置換しかつ前記スペシフ
    ィケーションを前記改善されたスペシフィケーションと
    置換し、前記テスト段階へ戻る段階；前記与えられたス
    ペシフィケーションから前記モジュールの組を生成する
    段階；よりなることを特徴とするシーケンシャル回路生
    成方法。
JP3062481A 1990-03-06 1991-03-05 シーケンシャル回路及びその生成方法、及びコントローラ及び有限状態マシン Expired - Fee Related JPH0760324B2 (ja)

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
US07/489,438 US5163016A (en) 1990-03-06 1990-03-06 Analytical development and verification of control-intensive systems
US489438 1990-03-06

Publications (2)

Publication Number Publication Date
JPH04219804A JPH04219804A (ja) 1992-08-10
JPH0760324B2 true JPH0760324B2 (ja) 1995-06-28

Family

ID=23943860

Family Applications (1)

Application Number Title Priority Date Filing Date
JP3062481A Expired - Fee Related JPH0760324B2 (ja) 1990-03-06 1991-03-05 シーケンシャル回路及びその生成方法、及びコントローラ及び有限状態マシン

Country Status (6)

Country Link
US (1) US5163016A (ja)
EP (1) EP0445942A3 (ja)
JP (1) JPH0760324B2 (ja)
KR (1) KR100237090B1 (ja)
CA (1) CA2035844C (ja)
IL (1) IL97177A (ja)

Families Citing this family (118)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
JPH02234274A (ja) * 1989-03-08 1990-09-17 Hitachi Ltd パイプライン制御論理の自動生成方法及び制御論理
US6185516B1 (en) * 1990-03-06 2001-02-06 Lucent Technologies Inc. Automata-theoretic verification of systems
US5483470A (en) * 1990-03-06 1996-01-09 At&T Corp. Timing verification by successive approximation
FR2679398B1 (fr) * 1991-07-16 1993-10-08 Alcatel Cit Procede d'aide au developpement d'un ensemble d'automates communicants.
US5910958A (en) * 1991-08-14 1999-06-08 Vlsi Technology, Inc. Automatic generation of test vectors for sequential circuits
US5305229A (en) * 1991-09-06 1994-04-19 Bell Communications Research, Inc. Switch-level timing simulation based on two-connected components
US5299206A (en) * 1991-10-24 1994-03-29 Digital Equipment Corporation System and method for analyzing complex sequences in trace arrays using multiple finite automata
FR2685838B1 (fr) * 1991-12-27 1994-02-25 Sgs Thomson Microelectronics Sa Procede pour verifier la conformite a une norme d'une cellule representative d'un circuit dedie a la gestion d'un protocole de communication, et systeme pour sa mise en óoeuvre.
US5491640A (en) * 1992-05-01 1996-02-13 Vlsi Technology, Inc. Method and apparatus for synthesizing datapaths for integrated circuit design and fabrication
US5710711A (en) * 1992-10-21 1998-01-20 Lucent Technologies Inc. Method and integrated circuit adapted for partial scan testability
US5477474A (en) * 1992-10-29 1995-12-19 Altera Corporation Computer logic simulation with dynamic modeling
WO1994017478A1 (en) * 1993-01-19 1994-08-04 City Of Hope Method for control of chaotic systems
JP2994926B2 (ja) * 1993-10-29 1999-12-27 松下電器産業株式会社 有限状態機械作成方法とパターン照合機械作成方法とこれらを変形する方法および駆動方法
US5446652A (en) * 1993-04-27 1995-08-29 Ventana Systems, Inc. Constraint knowledge in simulation modeling
US5465216A (en) * 1993-06-02 1995-11-07 Intel Corporation Automatic design verification
US5394347A (en) * 1993-07-29 1995-02-28 Digital Equipment Corporation Method and apparatus for generating tests for structures expressed as extended finite state machines
US5659555A (en) * 1993-08-19 1997-08-19 Lucent Technologies Inc. Method and apparatus for testing protocols
US5493505A (en) * 1993-10-28 1996-02-20 Nec Usa, Inc. Initializable asynchronous circuit design
US5623419A (en) * 1994-04-28 1997-04-22 Cadence Design Systems, Inc. Modeling of multi-disciplinary signals
US5513122A (en) * 1994-06-06 1996-04-30 At&T Corp. Method and apparatus for determining the reachable states in a hybrid model state machine
US5623499A (en) * 1994-06-27 1997-04-22 Lucent Technologies Inc. Method and apparatus for generating conformance test data sequences
US5600579A (en) * 1994-07-08 1997-02-04 Apple Computer, Inc. Hardware simulation and design verification system and method
WO1996024101A1 (en) * 1995-02-03 1996-08-08 A T & T Corp. An automata-theoretic verification of systems
US5535145A (en) * 1995-02-03 1996-07-09 International Business Machines Corporation Delay model abstraction
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
US5878407A (en) * 1995-04-18 1999-03-02 International Business Machines Corporation Storage of a graph
US5703798A (en) * 1995-04-25 1997-12-30 Mentor Graphics Corporation Switch level simulation employing dynamic short-circuit ratio
US5831853A (en) * 1995-06-07 1998-11-03 Xerox Corporation Automatic construction of digital controllers/device drivers for electro-mechanical systems using component models
US5848393A (en) * 1995-12-15 1998-12-08 Ncr Corporation "What if . . . " function for simulating operations within a task workflow management system
US5854929A (en) * 1996-03-08 1998-12-29 Interuniversitair Micro-Elektronica Centrum (Imec Vzw) Method of generating code for programmable processors, code generator and application thereof
US5905883A (en) * 1996-04-15 1999-05-18 Sun Microsystems, Inc. Verification system for circuit simulator
DE69626963T2 (de) * 1996-05-06 2003-11-13 Siemens Ag Verfahren zur Modellierung eines Prozessablaufs nach Zeitzwangsbedingungen
DE69626964T2 (de) * 1996-05-06 2003-11-06 Siemens Ag Verfahren zur Steuerung eines Prozessablaufs nach von einem Rechner spezifizierten Verhalten
US5754760A (en) * 1996-05-30 1998-05-19 Integrity Qa Software, Inc. Automatic software testing tool
US6178394B1 (en) * 1996-12-09 2001-01-23 Lucent Technologies Inc. Protocol checking for concurrent systems
IL119914A (en) 1996-12-25 2000-06-29 Emultek Ltd Device for implementing hierarchical state charts and methods and apparatus useful therefor
US6049662A (en) * 1997-01-27 2000-04-11 International Business Machines Corporation System and method for model size reduction of an integrated circuit utilizing net invariants
US6606588B1 (en) 1997-03-14 2003-08-12 Interuniversitair Micro-Elecktronica Centrum (Imec Vzw) Design apparatus and a method for generating an implementable description of a digital system
EP0867820A3 (en) * 1997-03-14 2000-08-16 Interuniversitair Micro-Elektronica Centrum Vzw A design environment and a method for generating an implementable description of a digital system
US6233540B1 (en) 1997-03-14 2001-05-15 Interuniversitair Micro-Elektronica Centrum Design environment and a method for generating an implementable description of a digital system
US5937181A (en) * 1997-03-31 1999-08-10 Lucent Technologies, Inc. Simulation of a process of a concurrent system
US5901073A (en) * 1997-06-06 1999-05-04 Lucent Technologies Inc. Method for detecting errors in models through restriction
US6138266A (en) 1997-06-16 2000-10-24 Tharas Systems Inc. Functional verification of integrated circuit designs
US6295515B1 (en) * 1997-11-03 2001-09-25 Lucent Technologies Inc. Static partial order reduction
US6059837A (en) * 1997-12-30 2000-05-09 Synopsys, Inc. Method and system for automata-based approach to state reachability of interacting extended finite state machines
US6324496B1 (en) * 1998-06-18 2001-11-27 Lucent Technologies Inc. Model checking of hierarchical state machines
US6099575A (en) * 1998-06-23 2000-08-08 Lucent Technologies Inc. Constraint validity checking
US6446241B1 (en) 1999-07-15 2002-09-03 Texas Instruments Incorporated Automated method for testing cache
US6625783B2 (en) * 2000-02-16 2003-09-23 Logic Research Co., Ltd. State machine, semiconductor device using state machine, and method of design thereof
US6606674B1 (en) * 2000-02-24 2003-08-12 Intel Corporation Method and apparatus for reducing circular list's thrashing by detecting the queues' status on a circular linked list
US6708143B1 (en) * 2000-05-22 2004-03-16 Lucent Technologies Inc. Verification coverage method
US6564354B1 (en) * 2000-06-01 2003-05-13 Hewlett Packard Development Company, L.P. Method for translating conditional expressions from a non-verilog hardware description language to verilog hardware description language while preserving structure suitable for logic synthesis
EP1168158B1 (en) * 2000-06-12 2007-10-10 Broadcom Corporation Context switch architecture and system
US20020032551A1 (en) * 2000-08-07 2002-03-14 Jabari Zakiya Systems and methods for implementing hash algorithms
EP1202141B1 (en) * 2000-10-30 2007-12-12 Siemens Aktiengesellschaft Method of reducing finite controlling automata and corresponding computer-readable medium
US7283945B2 (en) * 2000-11-03 2007-10-16 Fujitsu Limited High level verification of software and hardware descriptions by symbolic simulation using assume-guarantee relationships with linear arithmetic assumptions
US6625786B2 (en) 2000-12-14 2003-09-23 Tharas Systems, Inc. Run-time controller in a functional verification system
US6470480B2 (en) * 2000-12-14 2002-10-22 Tharas Systems, Inc. Tracing different states reached by a signal in a functional verification system
US6691287B2 (en) 2000-12-14 2004-02-10 Tharas Systems Inc. Functional verification system
US6629297B2 (en) 2000-12-14 2003-09-30 Tharas Systems Inc. Tracing the change of state of a signal in a functional verification system
US6957178B2 (en) * 2001-10-29 2005-10-18 Honeywell International Inc. Incremental automata verification
US6986117B1 (en) * 2002-06-04 2006-01-10 Cadence Design Systems, Inc. Method and apparatus for identifying a path between source and target states
US7231630B2 (en) * 2002-07-12 2007-06-12 Ensequence Inc. Method and system automatic control of graphical computer application appearance and execution
US7653520B2 (en) * 2002-07-19 2010-01-26 Sri International Method for combining decision procedures with satisfiability solvers
US6778943B2 (en) * 2002-08-13 2004-08-17 Xerox Corporation Systems and methods for distributed fault diagnosis using precompiled finite state automata
US7451143B2 (en) * 2002-08-28 2008-11-11 Cisco Technology, Inc. Programmable rule processing apparatus for conducting high speed contextual searches and characterizations of patterns in data
US7119577B2 (en) * 2002-08-28 2006-10-10 Cisco Systems, Inc. Method and apparatus for efficient implementation and evaluation of state machines and programmable finite state automata
US20040209676A1 (en) * 2002-11-18 2004-10-21 Takahiro Onishi Gaming machine
US7085918B2 (en) * 2003-01-09 2006-08-01 Cisco Systems, Inc. Methods and apparatuses for evaluation of regular expressions of arbitrary size
US7464254B2 (en) * 2003-01-09 2008-12-09 Cisco Technology, Inc. Programmable processor apparatus integrating dedicated search registers and dedicated state machine registers with associated execution hardware to support rapid application of rulesets to data
DE10325513B8 (de) * 2003-06-05 2006-08-03 Onespin Solutions Gmbh Verfahren und Vorrichtung zum Erstellen eines Verhaltensaspekts einer Schaltung zur formalen Verifikation
CN100461186C (zh) * 2003-10-31 2009-02-11 富士通微电子株式会社 验证支持装置、验证支持方法
US7543274B2 (en) 2003-12-22 2009-06-02 The United States Of America As Represented By The Administrator Of The National Aeronautics And Space Administration System and method for deriving a process-based specification
US7895552B1 (en) * 2004-03-26 2011-02-22 Jasper Design Automation, Inc. Extracting, visualizing, and acting on inconsistencies between a circuit design and its abstraction
JP4691374B2 (ja) * 2004-04-08 2011-06-01 日立オートモティブシステムズ株式会社 設計支援システム
US7581199B1 (en) * 2005-08-08 2009-08-25 National Semiconductor Corporation Use of state nodes for efficient simulation of large digital circuits at the transistor level
US7434183B2 (en) * 2005-08-17 2008-10-07 Cadence Design Systems, Inc. Method and system for validating a hierarchical simulation database
WO2007028226A1 (en) * 2005-09-09 2007-03-15 Ibm Canada Limited - Ibm Canada Limitee Method and system for state machine translation
JP4496205B2 (ja) * 2006-12-18 2010-07-07 日立オートモティブシステムズ株式会社 制御用マイクロコンピュータの検証装置および車載用制御装置
US9082104B2 (en) * 2007-02-02 2015-07-14 Alcatel Lucent Method and apparatus for managing system specifications
US20090093901A1 (en) * 2007-10-03 2009-04-09 International Business Machines Corporation Method and apparatus for using design specifications and measurements on manufactured products in conceptual design models
US9002899B2 (en) * 2008-07-07 2015-04-07 International Business Machines Corporation Method of merging and incremental construction of minimal finite state machines
US8885510B2 (en) 2012-10-09 2014-11-11 Netspeed Systems Heterogeneous channel capacities in an interconnect
US9009648B2 (en) * 2013-01-18 2015-04-14 Netspeed Systems Automatic deadlock detection and avoidance in a system interconnect by capturing internal dependencies of IP cores using high level specification
US9471726B2 (en) 2013-07-25 2016-10-18 Netspeed Systems System level simulation in network on chip architecture
US9473388B2 (en) 2013-08-07 2016-10-18 Netspeed Systems Supporting multicast in NOC interconnect
US9699079B2 (en) 2013-12-30 2017-07-04 Netspeed Systems Streaming bridge design with host interfaces and network on chip (NoC) layers
US9473415B2 (en) 2014-02-20 2016-10-18 Netspeed Systems QoS in a system with end-to-end flow control and QoS aware buffer allocation
GB2526052B (en) * 2014-03-31 2016-04-13 Imagination Tech Ltd Deadlock detection using assertions
US9742630B2 (en) 2014-09-22 2017-08-22 Netspeed Systems Configurable router for a network on chip (NoC)
US9571341B1 (en) 2014-10-01 2017-02-14 Netspeed Systems Clock gating for system-on-chip elements
US9660942B2 (en) 2015-02-03 2017-05-23 Netspeed Systems Automatic buffer sizing for optimal network-on-chip design
US9444702B1 (en) 2015-02-06 2016-09-13 Netspeed Systems System and method for visualization of NoC performance based on simulation output
US9928204B2 (en) 2015-02-12 2018-03-27 Netspeed Systems, Inc. Transaction expansion for NoC simulation and NoC design
US9568970B1 (en) 2015-02-12 2017-02-14 Netspeed Systems, Inc. Hardware and software enabled implementation of power profile management instructions in system on chip
US10050843B2 (en) 2015-02-18 2018-08-14 Netspeed Systems Generation of network-on-chip layout based on user specified topological constraints
US10348563B2 (en) 2015-02-18 2019-07-09 Netspeed Systems, Inc. System-on-chip (SoC) optimization through transformation and generation of a network-on-chip (NoC) topology
US9864728B2 (en) 2015-05-29 2018-01-09 Netspeed Systems, Inc. Automatic generation of physically aware aggregation/distribution networks
US9825809B2 (en) 2015-05-29 2017-11-21 Netspeed Systems Dynamically configuring store-and-forward channels and cut-through channels in a network-on-chip
US10218580B2 (en) 2015-06-18 2019-02-26 Netspeed Systems Generating physically aware network-on-chip design from a physical system-on-chip specification
US10452124B2 (en) 2016-09-12 2019-10-22 Netspeed Systems, Inc. Systems and methods for facilitating low power on a network-on-chip
US20180159786A1 (en) 2016-12-02 2018-06-07 Netspeed Systems, Inc. Interface virtualization and fast path for network on chip
US10313269B2 (en) 2016-12-26 2019-06-04 Netspeed Systems, Inc. System and method for network on chip construction through machine learning
US10063496B2 (en) 2017-01-10 2018-08-28 Netspeed Systems Inc. Buffer sizing of a NoC through machine learning
US10084725B2 (en) 2017-01-11 2018-09-25 Netspeed Systems, Inc. Extracting features from a NoC for machine learning construction
US10469337B2 (en) 2017-02-01 2019-11-05 Netspeed Systems, Inc. Cost management against requirements for the generation of a NoC
US10298485B2 (en) 2017-02-06 2019-05-21 Netspeed Systems, Inc. Systems and methods for NoC construction
US11144457B2 (en) 2018-02-22 2021-10-12 Netspeed Systems, Inc. Enhanced page locality in network-on-chip (NoC) architectures
US10547514B2 (en) 2018-02-22 2020-01-28 Netspeed Systems, Inc. Automatic crossbar generation and router connections for network-on-chip (NOC) topology generation
US10983910B2 (en) 2018-02-22 2021-04-20 Netspeed Systems, Inc. Bandwidth weighting mechanism based network-on-chip (NoC) configuration
US10896476B2 (en) 2018-02-22 2021-01-19 Netspeed Systems, Inc. Repository of integration description of hardware intellectual property for NoC construction and SoC integration
US11176302B2 (en) 2018-02-23 2021-11-16 Netspeed Systems, Inc. System on chip (SoC) builder
US11023377B2 (en) 2018-02-23 2021-06-01 Netspeed Systems, Inc. Application mapping on hardened network-on-chip (NoC) of field-programmable gate array (FPGA)
CN110383232B (zh) * 2019-05-05 2021-03-23 长江存储科技有限责任公司 具有序列处理单元的存储器控制系统
GB2588134B (en) * 2019-10-08 2021-12-01 Imagination Tech Ltd Verification of hardware design for data transformation component
US11669613B2 (en) * 2020-05-29 2023-06-06 EnSoft Corp. Method for analyzing and verifying software for safety and security
US11914993B1 (en) * 2021-06-30 2024-02-27 Amazon Technologies, Inc. Example-based synthesis of rules for detecting violations of software coding practices
US12353848B2 (en) * 2023-06-23 2025-07-08 Maplebear Inc. Validating code ownership of software components in a software development system

Family Cites Families (5)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US4587625A (en) * 1983-07-05 1986-05-06 Motorola Inc. Processor for simulating digital structures
US4694411A (en) * 1985-02-04 1987-09-15 Sanders Associates, Inc. Simulation apparatus and method
US4862347A (en) * 1986-04-22 1989-08-29 International Business Machine Corporation System for simulating memory arrays in a logic simulation machine
US4907180A (en) * 1987-05-04 1990-03-06 Hewlett-Packard Company Hardware switch level simulator for MOS circuits
US4965758A (en) * 1988-03-01 1990-10-23 Digital Equipment Corporation Aiding the design of an operation having timing interactions by operating a computer system

Also Published As

Publication number Publication date
IL97177A0 (en) 1992-05-25
JPH04219804A (ja) 1992-08-10
EP0445942A2 (en) 1991-09-11
EP0445942A3 (en) 1994-09-21
CA2035844C (en) 1995-05-16
US5163016A (en) 1992-11-10
IL97177A (en) 1995-12-31
KR910017301A (ko) 1991-11-05
KR100237090B1 (ko) 2000-01-15

Similar Documents

Publication Publication Date Title
JPH0760324B2 (ja) シーケンシャル回路及びその生成方法、及びコントローラ及び有限状態マシン
US5483470A (en) Timing verification by successive approximation
JP3835754B2 (ja) 集積回路の設計方法及びそれによって設計された集積回路
US20080270103A1 (en) Method for Functional Verification of an Integrated Circuit Model for constituting a Verification Platform, Equipment Emulator and Verification Platform
Jussila et al. Model checking dynamic and hierarchical UML state machines
US20060282807A1 (en) Software verification
US5960182A (en) Hardware-software co-simulation system, hardware-software co-simulation method, and computer-readable memory containing a hardware-software co-simulation program
JPH11513512A (ja) ディジタル信号プロセッサの製造方法
JP2001142937A (ja) 回路のスケジューリング正当性チェック方法及びスケジュール検証方法
JP4418591B2 (ja) 技術システムの予め設定された特性と第１の特性とを比較するための方法及び装置
van Beusekom et al. Formalising the Dezyne modelling language in mCRL2
US7124070B2 (en) Method of and apparatus for, and program for verifying equivalence between behavioral description and register transfer level description
Schmidt et al. A new formal verification approach for hardware-dependent embedded system software
JP2000207440A (ja) 半導体集積回路の設計検証装置、方法及び記憶媒体
US7257786B1 (en) Method and apparatus for solving constraints
Lavagno et al. Embedded system co-design: Synthesis and verification
JPH05101141A (ja) 高位合成装置
Kress-Gazit et al. The challenges in specifying and explaining synthesized implementations of reactive systems
CN116911219A (zh) 用于逻辑系统设计的仿真的方法、电子设备和存储介质
Borrione et al. HDL-based integration of formal methods and CAD tools in the PREVAIL environment
Schliecker Performance analysis of multiprocessor real-time systems with shared resources
Mooney et al. Synthesis from mixed specifications
Blaumenrohr et al. Performing high-level synthesis via program transformations within a theorem prover
EP0938045A1 (en) Method and apparatus for efficient verification using a generalised partial order analysis
Toeppe et al. Automatic code generation requirements for production automotive powertrain applications

Legal Events

Date Code Title Description
LAPS Cancellation because of no payment of annual fees