(57)【要約】【課題】C 言語などを用いた高抽象度でのシステム設計において、設計詳細化を経ても、満たすべきプロパティが確実に、かつ設計者に負担を強いずとも満たされることを可能とする。【解決手段】本発明の一態様としての設計装置は、複数の部品を含み、互いに通信する前記部品間をチャネルで接続した電子システムの設計を記述した設計記述と、各前記部品が守るべき制約を記述した部品制約記述と、各前記チャネルが守るべき制約を記述したチャネル制約記述と、から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出する接続制約記述算出部と、前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得る全体制約記述算出部と、を備える。【選択図】図１
2008242962.tif 000002
【特許請求の範囲】
【請求項１】
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出する接続制約記述算出部と、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得る全体制約記述算出部と、
を備えた設計装置。
【請求項２】
前記部品制約記述、前記チャネル制約記述、前記通信制約記述は時相論理を用いた論理式で記述されたことを特徴とする請求項２に記載の設計装置。
【請求項３】
通信制約記述を格納した第１データベースと、
通信部品または通信プロトコルを指定する指定手段と、
前記通信部品または通信プロトコルに対応する通信制約記述を前記第１データベースから取得する通信制約記述取得手段と、
を備えた請求項１または２に記載の設計装置。
【請求項４】
部品制約記述を格納した第２データベースと、
チャネル制約記述を格納した第３データベースと、
前記設計記述に記述された部品に対応する部品制約記述を前記第２データベースから取得する部品制約記述取得手段と、
前記設計記述に記述されたチャネルに対応するチャネル制約記述を前記第３データベースから取得するチャネル制約記述取得手段と、
を備えた請求項１〜３のいずれか一項に記載の設計装置。
【請求項５】
前記全体制約記述から特定の部品に関わる制約を抽出する部品制約抽出手段をさらに備えたことを特徴とする請求項１〜４のいずれか一項に記載の設計装置。
【請求項６】
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出し、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得る、
設計方法。
【請求項７】
前記部品制約記述、前記チャネル制約記述、前記通信制約記述は時相論理を用いた論理式で記述されたことを特徴とする請求項６に記載の設計方法。
【請求項８】
通信制約記述を格納した第１データベースを用意し、
通信部品または通信プロトコルを指定し、
前記通信部品または通信プロトコルに対応する通信制約記述を前記第１データベースから取得する、
ことを特徴とする請求項６または７に記載の設計方法。
【請求項９】
部品制約記述を格納した第２データベースと、チャネル制約記述を格納した第３データベースとを用意し、
前記設計記述に記述された部品に対応する部品制約記述を前記第２データベースから取得し、
前記設計記述に記述されたチャネルに対応するチャネル制約記述を前記第３データベースから取得する、
ことを特徴とする請求項６〜８のいずれか一項に記載の設計方法。
【請求項１０】
前記全体制約記述から特定の部品に関わる制約を抽出する部品制約抽出手段をさらに備えたことを特徴とする請求項６〜９のいずれか一項に記載の設計方法。
【請求項１１】
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出するステップと、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得るステップと、
をコンピュータに実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、LSI(Large-Scale Integration) 設計など電子回路を主とするシステムの設計を行うための設計装置、設計方法およびプログラムに関し、特に電子システムレベル（ESL:Electronic System Level）設計と呼ばれるような、C 言語などの抽象度の高い言語を使ってシステムを記述する技術分野に関する。
【背景技術】
【０００２】
近年、デジタル回路をベースとした設計において、C 言語やそれに類する、SystemCTM やSpecC 言語と言った、抽象度の高い言語を用いる事で、従来のハードウェア記述言語よりも生産性の高い設計をする試みがなされている。多くの電子システムはCPU、メモリといった機能モジュールと、それらの間の通信を受け持つ通信バス、といった構成をとる事が多いが、特にSystemCTM やSpecC 言語を用いた設計においては、電子システムをより高い抽象度で設計するため、機能モジュールと、それらの間をつなぐチャネルという概念を用いて設計されることがままある。機能モジュールとチャネルとで構成された設計は、その後、人手によって通信バスを用いた構成に置き換える「設計詳細化」と呼ばれる作業が必要であった。米国カリフォルニア大学アーバイン校において開発されたSCE （System-on-Chip Environment）と呼ばれる開発環境などは、この作業を半自動的に行うものであった（参考：同大学組み込みコンピュータシステムセンター技術報告：TR03-45）。
【０００３】
しかし、人手においてもツールによる自動的な変換においても、詳細化後の設計記述が元々の仕様を保証する事は容易ではなかった。その上、詳細化後に設計記述を修正してしまうと、設計詳細化の前後で設計の同一性がなくなってしまい、元の仕様を詳細化後の設計が満たすかどうか、確認する事は尚更困難であった。
【０００４】
一方、LSI 設計などで、特にハードウェア記述言語を使った設計において、時相論理や正規表現をベースとしたプロパティ記述言語を使ってプロパティ（対象の設計が守るべき制約）を記述し、設計記述の検証に用いる方法が盛んに用いられている。ここでいうプロパティ記述言語として、“Property Specificaton Language” (IEEE 1076, 1364, 1800) などがある。
【０００５】
また、Goguen とBurstall、あるいはFiadeiro らは、下記非特許文献１、２などで、並行ソフトウェアを記述する仕様記述言語を代数的に定義し、その言語の上で、複数の並行に動くソフトウェアの仕様を合成する数学的な枠組みを与えた。
【非特許文献１】Joseph A. Goguen and Rod M. Burstall. Institutions: abstract model theory for specification and programming. J. ACM, 39(1):95.146, 1992.
【非特許文献２】Jos´e Luiz Fiadeiro and Tom Maibaum. Categorical semantics of parallel program design. Sci. Comput. Program., 28(2-3):111.138, 1997.
【発明の開示】
【発明が解決しようとする課題】
【０００６】
本発明は、C 言語などを用いた高抽象度でのシステム設計において、設計詳細化を経ても、満たすべきプロパティが確実に、かつ設計者に負担を強いずとも満たされることを可能とした設計装置、設計方法およびプログラムを提供する。
【課題を解決するための手段】
【０００７】
本発明の一態様としての設計装置は、
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出する接続制約記述算出部と、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得る全体制約記述算出部と、
を備える。
【０００８】
本発明の一態様としての設計方法は、
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出し、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得る。
【０００９】
本発明の一態様としてのプログラムは、
複数の部品を含み、互いに通信する前記部品間をチャネルで接続したシステムの設計を記述した設計記述と、
各前記部品が守るべき制約を記述した部品制約記述と、
各前記チャネルが守るべき制約を記述したチャネル制約記述と、
から、前記チャネルで接続された部品間で守られるべき制約を記述した接続制約記述を算出するステップと、
前記接続制約記述と、通信に用いられる通信部品または通信プロトコルに関わる制約を記述した通信制約記述とから、各前記部品間全体で守られるべき制約を記述した全体制約記述を得るステップと、
をコンピュータに実行させる。
【発明の効果】
【００１０】
本発明により、C 言語などを用いた高抽象度でのシステム設計において、設計詳細化を経ても、満たすべきプロパティが確実に、かつ設計者に負担を強いずとも満たされることが可能となる。
【発明を実施するための最良の形態】
【００１１】
図1 は、本発明の一実施形態としての設計装置の全体構成を示すブロック図である。また、図2 は、図1の設計装置による処理の流れを示すフローチャートである。図2のフローチャートに示される各段階の処理を実行するための命令を記述したコンピュータプログラムをコンピュータに実行させることによって図1の設計装置の各要素の機能が実現されてもよい。このコンピュータプログラムはハードディスク、CD-ROMなどの記録媒体に格納されてコンピュータによって読み出され実行されてもよい。以下図1および図2に沿って、本処理の流れを概説する。
【００１２】
まず本装置は、設計者からの入力１０１に基づき、設計記述１０３を受け取る（図2 の２０１）。ここには、例えば図4 のような、複数の部品がチャネルで接続されたような態様で電子システムの設計が記述されている。
【００１３】
利用部品選択部１０４は、設計記述１０３に記述されている利用部品の識別の処理２０２を行い、利用されている部品の各々が、部品DB（DataBase：データベース）１０５ に蓄積されている標準部品であるかどうかの判断２０３を行い、YES であれば、部品DB１０５ から該部品（標準部品）に対応する部品プロパティの取得２０４を行い、NO であれば、該部品（ユーザが自ら設計したカスタム部品）に対応する部品プロパティを、設計記述１０３から直接読み取る（２０５）。ここで部品プロパティは、部品が守るべき制約の記述であり、部品制約記述に相当する。部品DB１０５は第２データベースに相当し、利用部品選択部１０４は部品制約記述取得手段を含んでいる。以上２０３から２０５の処理を、識別された部品全てに対して行う。
【００１４】
次に接続情報抽出部１０６は、設計記述１０３から、部品間の接続関係を読み取り、その接続に使われているチャネルの識別２０６を行う。そして、識別されたチャネルの各々に対応するチャネルプロパティ１１１を、チャネルDB １０２から取得する（２０７）。  チャネルプロパティ１１１はチャネルが守るべき制約の記述であり、チャネル制約記述に相当する。チャネルDB１０２は第３データベースに相当し、接続情報抽出部１０６はチャネル制約記述取得手段を含んでいる。接続情報抽出手段１０６は、処理２０６で識別されたチャネルと、利用部品選択部１０４で識別された部品との接続関係を処理２０８にて識別し、接続情報１１０を得る。
【００１５】
そして接続プロパティ算出部１１２は、接続プロパティの算出処理２０９を行うことにより接続プロパティ１１４を得る。接続プロパティは、同じチャネルで接続された部品同士間で守られるべき制約の記述であり、接続制約記述に相当する。
【００１６】
２０９の処理後、あるいはそれとは別途、設計者は通信部品（たとえばある種類のバス）の選択１０９を行う（２１０）。通信部品の選択１０９は、設計者により指定手段を用いて通信部品または通信プロトコルの指定を行う操作に相当する。
【００１７】
通信プロパティ選択部１１３は、設計者によって選択された通信部品に対応する通信プロパティ１１７を、通信部品DB１０８から取得する（２１１）。通信プロパティは、部品間の通信に用いられる通信部品または通信プロトコルに関わる制約の記述であり、通信制約記述に相当する。通信プロパティ選択部１１３は通信制約記述取得手段に相当し、通信部品DB１０８は第１データベースに相当する。
【００１８】
そして、合成プロパティ算出部１１５は、接続プロパティ１１４と通信プロパティ１１７から、合成プロパティの算出２１２を行って合成プロパティ１１６を取得し、本装置から出力する。合成プロパティは、通信部品または通信プロトコルを介して通信する各部品間全体で守られるべき制約の記述であり、全体制約記述に相当する。合成プロパティ算出部１１５は全体制約記述取得手段に相当する。
【００１９】
ここで例として、図3 のような、2 つのCPU と2 つのメモリが一本のバスを介して通信しあうような電子システムを最終的に設計する事を考え、この例に従って本装置の処理の流れを解説する。
【００２０】
本装置の入力として、設計者は図4 のような、CPU とメモリが1 対ずつ、それぞれチャネルを通じて通信しあうような設計記述を与える。CPU1 は、Store 信号をチャネル送信側に接続し、メモリ1 はRead 信号をチャネル受信側に接続している。このことで、CPU1 はStore 信号を発行すると、チャネルを介してメモリ1 に伝達される。CPU2 とメモリ2 にもまったく同様の想定がなされている。つまり、CPU1 はメモリ1 と、CPU2 はメモリ2 としか通信せず、それぞれが並行に動作しうる設計となっている。
【００２１】
なお、CPU はユーザがカスタム部品として用意し、メモリはDB に標準部品として与えられているものとする。ここではCPU、メモリ、チャネルは2 つとも同一で、1 種類しかない想定となっているが、当然複数の種類のチャネルがあってもかまわない。
【００２２】
DBに格納されている各プロパティ（部品プロパティ、チャネルプロパティ、通信プロパティ）は、時相論理を用いた論理式で記述されている。一般的な古典論理の記号である∧（論理積）、∨（論理和）、→（含意）, ¬（否定）のほか、時相を表すオペレータF, X, G を用いる事が可能であるとする。ここで、FA は「いつかA が成り立つ」、XA は「次の時刻にA が成り立つ」、GA は「常にA が成り立つ」という意味を示している。これらのオペレータは、別の記号を用いる事はあるが、時相論理として一般的なものである。
【００２３】
また、X を重ねて記述するための略記法として、[n] (n は自然数) を用いる事もできるとする。例えば、[3]A はXXXA と同義である。
【００２４】
以降、「次の時刻に」を「1 サイクル後に」と読み替える事にする。[n]A は、「n サイクル後にA が成り立つ」となる。また、A を電子システムにおける信号とみなせば、「A が成り立つ」は「信号Aが1 になる」あるいは「信号Aが発行される」と読み替える事ができる。逆に「A が成り立たない」は「信号A が0 になる」あるいは「信号A が発行されない（されなくなる）」と読み替える事ができる。
【００２５】
また、DB に格納されている各プロパティは、図5の要領で与えられるメタ制約に従って記述されている。以下、メタ制約の役割と利用方法について解説する。図5 の例では、
・チャネルの、送信側の端点を表す信号Start 
・チャネルの、受信側の端点を表す信号End 
・チャネルへの送信ができるかどうかの状態を表す信号Grant
・計算の開始を表す、擬似的な信号Init 
・計算の終了を表す、擬似的な信号Term 
の各記号から構成されている。
【００２６】
メタ制約は、通信プロパティ、接続プロパティのそれぞれで共通して利用される信号（通信の単位となる記号）を示している。チャネルプロパティは上記の通りメタ制約に記述した信号を用いた論理式で記述されるが、部品プロパティに関しては、メタ制約に記述した信号以外の信号名を用いる事もできる。通信プロパティは、メタ制約とは別途定義される通信制約と、その通信制約に記述された信号を用いた論理式と、通信制約に記述された信号と接続プロパティ内で使用されている信号の名前とを関係付ける合成射と、の3 つから構成される。例えば図23 のような図式を複数個集めたもので定義される。
【００２７】
ここで設計者は、図6 にあるようなプロパティをCPU に与えたとする。簡単のため、このCPU はStore 命令のみを保持しているとし、命令を1 つの信号とみなして、その最も素朴な制約を与えている。
【００２８】
ここで示された1 行目の論理式は、「計算が開始し、その時点でチャネルへ送信が可能な状態ならば、次のサイクルでStore 信号を発行する」を意味する制約であり、2 行目の論理式は、「Store 信号が0 になったら、計算が終了する」を意味する。
【００２９】
そして本装置は、メモリのプロパティとして図7 を部品DB １０５に格納し、またチャネルのプロパティとして図8 をチャネルDB１０２に格納しているとする。図7 の論理式は、「Read 信号が1 になったら、2サイクル後にRead 信号が0 になる」という意味である。また、図8 のうち1 行目は「Start 信号が1 になったら、いつかEnd 信号が1 になる」、2 行目は「End 信号が0 になったら、いつかStart 信号が0 になる」という意味である。
【００３０】
本装置は、図4 のような設計記述の入力を受け取ると、CPU、メモリ、チャネルの各プロパティを、然るべきDB または設計記述から取得する。そして、CPU とチャネルがStart の部分で接続されており、メモリとチャネルがEnd の部分で接続されている事を解析する。そして、接続プロパティ算出部１１２において接続プロパティを算出する。
【００３１】
接続プロパティおよび後述する合成プロパティの算出処理は、実際には、数学の圏論で言うcolimitを計算する処理である。接続プロパティの算出処理を解説するためにまず、colimit の定義を、横内寛文著『プログラム意味論』（ISBN:4-320-02657-8）の定義５．３．７から引用する。
【００３２】
カテゴリC とその図式D が与えられているとする。C の対象X と、D の各頂点i についてCの射: μi : D → X (Di は頂点i に割り当てられたC の射) が定められていて、D 中の任意の射f : Di → Dj について、図28の図式が可換であるとする。このとき、対象X とD の頂点の集合V によって添数づけられたC の射の族μ=(μi : Di→X)i∈Vの組をD からのcone と呼び（あるいはcocone と呼ぶ事もある）、μ : D→Xと表す。
【００３３】
さらに、D からの任意のcone ν : D→Y について、ある射p : X→Y が存在して、D の各頂点i について、図29の図式が可換になり、しかもこのような射ｐが正確に１つ存在するとする。このときμをDのcolimitと呼ぶ。
【００３４】
尚、「射」は圏論における術語であり、集合論における準同型写像に相当する。また、上述の定義で図式Ｄに相当するものを、「基底」と呼ぶ。「頂点」とは、基底の中で、矢印の先になっている箇所の事である。
【００３５】
上述のGoguenとBurstallは、仕様記述における各仕様の合成は各仕様から構成されるカテゴリと、それぞれの仕様間に定められた射から定義されるcolimitによって求められる事を示しており、この理論を本装置での接続プロパティ、合成プロパティの算出処理にも用いている。要は、基底を適切に設定することで、上述の定義に従って求められるcolimit (に含まれる対象X) を求めることが、接続プロパティ算出部１１２、合成プロパティ算出部１１５における処理である。その意味で、この2つの算出部は共通化することも可能であるが、本明細書では特に区別して記述している。
【００３６】
図10は接続プロパティの算出処理を説明するフローチャートである。
【００３７】
まず、該当する部品プロパティとチャネルプロパティを図式にあてはめる処理１００１をおこなう。図5のメタ制約に従った接続プロパティを求める上で、基底に相当する図式は、図12となる。M およびS は部品プロパティ、Ch はチャネルプロパティを示す。この図の意図するところは、チャネルの送信側（Start 側）に接続されている部品がM というプロパティを持ち、チャネルの受信側(End 側) に接続されている部品がS というプロパティを持つ、という事である。例えば、CPU1とメモリ１との間の接続プロパティを求める際は、ＭにCPU１が、Sにメモリ１が割り当てられ、Chがその間のチャネルとなる。
【００３８】
次に、接続関係に従い、部品プロパティに使われている信号名を置き換える処理１００２を行う。この置き換えは、先述の図式中の矢印（接続射）に、該当する接続関係を割り当てることに相当する。例えば図式における射sm, sc, ec, esは、接続情報抽出部１０６によって解析した接続情報から、図13のように定義づけられる。つまり、図12 中のsm,sc,ec,es に対して、図13 のような割り当て関係を、接続情報から導き出す。具体的には、CPU1 のStore 信号がチャネルの送信側に接続されている事から、Store 信号がStart 信号と同一である、とみなす（Start 信号をStore 信号に割り当てる）。これが射sm の意味である。同様に、メモリのRead 信号がチャネルの受信側に接続されている事から、End 信号をRead 信号に割り当てる、という、射es が決定する。sc、ec は解析情報を必要とすることなく、チャネルのStart 信号をStart 信号とみなし、End 信号をEnd 信号とみなす恒等射（恒等写像）と定義する。このような割り当て関係に従って部品プロパティに使われている信号名を置き換える。
【００３９】
置き換えた信号は、１００３の処理に従い、置換情報として書き換え前の信号と、書き換え後の信号の割り当て関係を記述しておく。
【００４０】
そして、信号名を置き換えた後の、全ての部品プロパティ、チャネルプロパティの論理式を一様に列挙して集める処理１００４を行うことにより接続プロパティを得る。接続プロパティの計算は図14のようにConnectを求めることであり、Connectが求めるべきcolimitとなる。
【００４１】
更に、ここからは必須ではないが、例えば図27 のような、論理式の変換ルールが定められている場合は、１００４で列挙された論理式のいくつかに対し、変換ルールが適用できるかできないかの判断１００５を行う。図27においてルールAnd1は、A→FBとA→XBとの２つをA→XBの１つに置換できることを規定し、And2は、A→FBとA→Bとの２つをA→Bの１つに置換できることを規定している。判断１００５においてYES の場合は、変換処理１００６を行って、適用できると判断された複数の論理式の論理式に、該当する変換ルールを適用して、古い論理式を消去して新しい論理式を生成し、再度１００５の判断を行う。１００５の判断がNO の場合は、処理を終了する。なお、１００５〜１００６の処理が不要である場合は、ルールを定めなければ良い。
【００４２】
この事例において算出された接続プロパティを図15に示す。なおこの時点では、CPU1とメモリ1、CPU2とメモリ2とはまったく独立に、同じプロパティが算出される。図15はその片側のみを示したものである。尚、ここで元の部品プロパティで使われていた信号名は、接続プロパティ上では図16 のように置き換えられている。このような情報（接続プロパティ置換信号情報）を接続プロパティ算出部１１２が同時に出力し、後の合成プロパティ算出の結果に反映させる事もできる。
【００４３】
この時点の結果で、設計者はバスなどのシステム全体の通信に関わる制約を入れない段階での、個々のモジュール間のやりとりに関わる制約を取得する事もできる。
【００４４】
次に、設計者は、上述の結果を参照するなどして、通信バスなど、システム全体の通信に関わる部品の選択を行い、その情報を本装置に対して入力する。ここでは、図9、図23、図24および図25に示されるような通信プロパティを持つバス部品が選択されたとする。
【００４５】
本装置における通信プロパティ選択部１１３は、設計者により選択された通信部品に関わる通信プロパティを通信部品DB１０８から取得し、合成プロパティ算出部１１５が通信プロパティと接続プロパティとから合成プロパティを算出する。
【００４６】
図11は合成プロパティの算出処理の流れを示すフローチャートである。
【００４７】
まず、入力となるn 個の接続プロパティの全てに1 からn までの番号を振る処理１１０１を行う。そして、通信プロパティに含まれる図式の1 つに対して、接続プロパティを当てはめる処理１１０３を行う。
【００４８】
ここで、通信プロパティのうちの1 つの図式は一般に、図17 のような図式となる。この図式において、MC は通信制約であり、Comm は通信制約を用いて記述された論理式の集合であり、Connect1…Connectn は、ここまでの処理で求められた複数個（n 個）の接続プロパティである。また、MC からComm, Connect1, ... Connectn への射c, c1…cn （合成射）は、通信制約に定められた信号の、メタ制約に定められた信号、すなわち接続プロパティに使われている信号への割り当てを行う射である。この事例では、通信プロパティは図9、図23、図24、図25 の組から成る図式1 つとする。ここで図23は図式の全体であり、図24がそのうちの通信制約MCであり、図9はその通信制約を使って記述された論理式Commであり、図25は合成射c1…cnの定義である。図23のcolimit 、すなわち図18 に示すCompositeが、求めるべき合成プロパティである。
【００４９】
本処理１１０３では、n 個の接続プロパティを、上述のConnect1 からConnectn のそれぞれに、１１０１で割り振られた番号に従って当てはめていく。この事例では、接続プロパティは2 つ存在し、それぞれを、Connect1 とConnect2 に当てはめる。この事例では、これら2 つに含まれる論理式の内容は全く同一である。
【００５０】
そして、１つ１つの接続プロパティに対して、繰り返し処理１１０４に従って処理をおこなう。まず、接続プロパティに、特別な信号Idle を追加する処理１１０５を行う。これは各接続プロパティの論理式では使われていない信号である事を意味する。これは後の処理１１０７において利用される。
【００５１】
そして、接続プロパティ中の信号名に、１１０１で割り振られた番号を振る処理１１０６を行う。例えば、接続プロパティに“1” が割り振られているとき、その中のStart という信号を、Start1 と変換する。これは、他の接続プロパティで同名の信号が使われている場合、信号名の衝突が起こるのを回避するための処理である。
【００５２】
そして、通信プロパティ中に定められた合成射に従って、信号名を通信制約に定められたものに置き換える処理１１０７を行う。ここで、通信制約は例えば図24 のように与えられ、合成射は図25のように与えられている。図25 において、左に示されているci が合成射の名称で、コロンで区切られた右に列挙されている、『→』で示された式のそれぞれが、通信制約にある信号名から、接続プロパティ中の信号名（既に、１１０６の処理で信号名が変更されているのを前提としているもの）への割り当てを示している。『→』の左辺が通信制約の、右辺が接続プロパティの信号名を示している。
【００５３】
i 番目の接続プロパティConnecti に対して、合成射ci を適用すれば、接続プロパティの信号名を通信制約のそれに置き換える事ができる。ただし、合成射で定義されている割り当てに含まれない接続プロパティ中の信号名は置き換わらない。また、合成射ci においてIdlei への割り当てが行われている場合は、実際の割り当ては起こらない。これは、通信制約には定められている信号であって、他の接続プロパティでは置き換えられるが、当該の接続プロパティには置き換えが発生しない場合に利用される処理である。
【００５４】
そして、１１０７で置き換えられた信号の前後での変更を、例えば図26 のような置換情報（合成プロパティ置換信号情報）として保存する処理１１０８を行う。
【００５５】
以上の処理を全ての接続プロパティに対して行った後、信号Idle、及びそれに相当する記号Idle1 , …, Idlenが残っていた場合は、それを削除する処理１１０９を行う。
【００５６】
そして、全ての接続プロパティ、および通信プロパティに定められた論理式を列挙し、1 つに集める処理１１１０を行う。
【００５７】
ここでもし、図27 のような変換ルール（And1, And2）が定められていた場合は、それらの変換ルールが、１１１０で集められたうちの複数の論理式に適用できるかどうかの判断１１１１を行い、その判断がYES であった場合は、適用できると判断した複数の論理式に対して、変換ルールを適用して、適用前の論理式を削除し、新しい論理式を生成する処理１１１２を行って、その後再び１１１１の判断を行う。
【００５８】
１１１１でNO と判断されれば、処理１１１３を行い、１１０８で保存した置換情報を元に、各論理式で使われている信号名を、１１０７での置き換え前の信号名に復元する。
【００５９】
以上の処理を、通信プロパティに含まれる全ての図式に対して繰り返し処理を行う（ループ１１０２）。すなわち通信プロパティの図式が複数個存在する場合は、処理１１１０〜１１１２による算出結果に対して合成プロパティの算出処理を適用し、新たな算出結果を計算する。この処理を、全ての通信プロパティの図式に対して繰り返して起用する。全ての図式の適用が終了すれば、処理を終了する。
【００６０】
この事例では、処理１１１０〜１１１２によって、図19に示す、当該電子システム全体の設計制約を示す合成プロパティが得られる。そして、処理１１１３において、接続プロパティ算出時の図16 の割り当て結果から、部品プロパティで使われていたStore, Read の信号を使って（ただし、Start とEnd はそれぞれStart1, Start2 とEnd1 とEnd2 の2 つの接続プロパティで同じ信号名を使っているため、それぞれStore1 とStore2、Read1とRead2 として）図19の合成プロパティを表現すると、図20 のようになる。
【００６１】
こうして得られた合成プロパティを使って、設計者は当該システムの設計に対する設計を検証したり、様々な情報を得る事ができる。ここではその一応用例として、CPU1 のStore 命令に対する制約を算出してみる。
【００６２】
図20に対して、一方のCPU であるCPU1 に関連する論理式を抽出する。すなわち本装置は、合成プロパティ（全体制約記述）から特定の部品に関する制約を抽出する部品制約抽出手段（図示せず）を備えている。抽出したCPU1 に関連する論理式に対して図21 に示されるルールを複数回適用して、時系列の始点と終点を示す記号Init1 からTerm1 に至るまでの論理式に簡約化する。ただし、ルールTransOp の『*』には、任意の時相オペレータが当てはまる。
【００６３】
その結果は図22 となる。この論理式から、下記のような制約条件が読み取れる。
・Store 命令が発行されて計算が終了するには、Grant信号が真でなければならない。しかし、このGrant信号はもう一方のCPUに対するGrant信号と共には発行されない。すなわち、CPU1のStore命令とCPU2のStore命令は排他的に発行されなければならない。
・Store 命令が発行されてから終了するまでに、5 サイクルかかる。
【００６４】
これはあくまで人間による解釈であるが、例えばこのプロパティを、CPU とその上で実行されるソフトウェアのための検証装置にかけて利用することで、ソフトウェアの命令単位での検証を行う事ができる。
【００６５】
一方、本発明で意図している実施形態はLSI などの電子システムの設計が主であるが、例えばネットワークを介して複数の計算機が通信しあうような分散システムを設計する場合にも役立てる事ができる。各計算機（分散システムの構成部品）が個別に守るべき制約を、部品プロパティや設計者の手によるカスタムのプロパティで与え、個別の通信相手との通信に関わる制約をチャネルプロパティで与える。その上で、通信プロトコル（ネットワークのトポロジーを含んでも良い）などを、システム全体の通信プロパティとして与える。
【００６６】
このようにすれば、各計算機と、各計算機のそれぞれに個別に与えられた通信に関する仕様と、通信プロトコルの選択を入力として、本装置によりシステム全体の制約仕様を導出する事ができる。
【００６７】
以上のように、本発明の実施形態によれば、設計部品とともに、該当部品に対応するプロパティも部品化・再利用し、設計詳細化の過程でプロパティの合成を自動的に行う事により、設計者はより少ない作業量で効率よく、設計詳細化を行った後のシステム全体のプロパティ（合成プロパティ）を得る事ができる。設計者は、この合成プロパティを利用する事で、詳細化された設計記述が実際に制約を満たしているかどうか、容易に検証できる。
【００６８】
また、設計者は、システム全体の設計を、
・個別のモジュールとその間の個別通信
・システム全体に関わる通信の選択
に分離して扱える事により、システム全体の通信制約に設計当初からわずらわされる事なく、より抽象的に、簡易にシステムの制約を得る事ができる。
【００６９】
さらに本提案の方式はプロパティの再利用性をより高め、効率的な再利用を行うことができる上に、個々の部品単位ではチェックできないような特性も、部品同士の接続関係や通信プロパティとの組み合わせからチェックすることができる。
【図面の簡単な説明】
【００７０】
【図１】本発明の一実施形態としての設計装置の全体構成を示すブロック図。
【図２】図1の設計装置による処理の流れを示すフローチャート。
【図３】本実施形態により設計しようとする電子システムの例を示す図。
【図４】設計記述の一例を示す図。
【図５】メタ制約の例を示す図。
【図６】部品（カスタム部品）プロパティの一例を示す図。
【図７】部品（標準部品）プロパティの一例を示す図。
【図８】チャネルプロパティの一例を示す図。
【図９】通信プロパティ（バス）の論理式の一例を示す図。
【図１０】接続プロパティの算出処理の流れを示すフローチャート。
【図１１】合成プロパティの算出処理の流れを示すフローチャート。
【図１２】接続プロパティの算出に関わる図式の例を示す図。
【図１３】接続射の割り当ての例を示す図。
【図１４】接続プロパティの算出例を示す図。
【図１５】接続プロパティの例を示す図。
【図１６】接続プロパティ置換信号情報の一例を示す図。
【図１７】合成プロパティの算出に関わる図式の例を示す図。
【図１８】合成プロパティの算出例を示す図。
【図１９】合成プロパティの一例（置換前）を示す図。
【図２０】合成プロパティの一例（置換後）を示す図。
【図２１】最適化ルールの例を示す図。
【図２２】図２０の合成プロパティからCPU1について得た制約の例を示す図。
【図２３】通信プロパティの図式の例を示す図。
【図２４】通信制約の例を示す図。
【図２５】通信プロパティの合成射の例を示す図。
【図２６】合成プロパティ置換信号情報の例を示す図。
【図２７】最適化ルールの例を示す図。
【図２８】colimitの定義を説明するための図。
【図２９】colimitの定義を説明するための図。
【符号の説明】
【００７１】
１０２：チャネルDB（第３データベース）
１０３：設計記述
１０４：利用部品選択部（部品制約記述取得手段）
１０５：部品DB（第２データベース）
１０６：接続情報抽出部（チャネル制約記述取得手段）
１０７：部品プロパティ（部品制約記述）
１０８：通信部品DB（第１データベース）
１１０：接続情報
１１１：チャネルプロパティ（チャネル制約記述）
１１２：接続プロパティ算出部（接続制約記述算出部）
１１３：通信プロパティ選択部（通信制約記述取得部）
１１４：接続プロパティ（接続制約記述）
１１５：合成プロパティ算出部（全体制約記述算出部）
１１６：合成プロパティ（全体制約記述）
１１７：通信プロパティ（通信制約記述）
【図１】
2008242962.tif 000003
【図２】
2008242962.tif 000004
【図３】
2008242962.tif 000005
【図４】
2008242962.tif 000006
【図５】
2008242962.tif 000007
【図６】
2008242962.tif 000008
【図７】
2008242962.tif 000009
【図８】
2008242962.tif 000010
【図９】
2008242962.tif 000011
【図１０】
2008242962.tif 000012
【図１１】
2008242962.tif 000013
【図１２】
2008242962.tif 000014
【図１３】
2008242962.tif 000015
【図１４】
2008242962.tif 000016
【図１５】
2008242962.tif 000017
【図１６】
2008242962.tif 000018
【図１７】
2008242962.tif 000019
【図１８】
2008242962.tif 000020
【図１９】
2008242962.tif 000021
【図２０】
2008242962.tif 000022
【図２１】
2008242962.tif 000023
【図２２】
2008242962.tif 000024
【図２３】
2008242962.tif 000025
【図２４】
2008242962.tif 000026
【図２５】
2008242962.tif 000027
【図２６】
2008242962.tif 000028
【図２７】
2008242962.tif 000029
【図２８】
2008242962.tif 000030
【図２９】
2008242962.tif 000031