博 士（情 報科学 ）吉川浩

学 位 論 文 題 名宣言的仕様に対する正当なデジタル回路および協調計算システムの自動生成に関する研究
学位論文内容の要旨
本研究は「宣言 的仕様」からデジタル回路 を自動生成する高位合成の研究，および宣言的仕様からソフトウェアと ハードウェアの協調計算シ ステムを自動生成する協調設計(Co‑Design)に関する研究である．本書 が扱う宣言的仕様とは問題 の性質と解く範囲を「確定節」と呼ばれる一階述語論理によって記述したものであり，一般的誼意味の「仕様」より狭い意味で用いられる．宣言的仕様が記述できる問題には求解問題や制約充足問題をどがあり，本研究の目的は，このよう誼問題を効率よく解くためのデジ タル回路やデジタル回路と ソフトウェアによる協調計算システムを自動生成する基礎を与えることである，本研究では，回路をプログラム変換によって生成する手法を開発しており，
ま た協 調計算の実験 を容易にするための柔軟社協調計算システムの開発も行 っている．
宣言的仕様は 問題の性質と問題の範囲を 宣言的に記述したものであり問題を解くアルゴリズムやプロシージャは 宣言的仕様に含まれをい． そのため宣言的仕様からアルゴリズムを生成する必要がある，本研究では，このアルゴリズムを「等価変換理論」と呼ばれる既存の研究によって宣言的仕様から自動生成さ れ与えられているものと仮 定している，生成されるアルゴリズムは書き換え規則に
よ っ て 記 述 さ れ ， こ の 書 き 換 え 規 則の 記述 を入 カと して デジ タル 回路 を生 成す る．
デジタル回路は，論理ゲートから橡る「組み合わせ回路」と記憶素子である「フリップフロップ」から構成されて いる．このようをデジタル 回路は「アドレス参照型メモ リ」を利用できをいためヒープやスタックをどが使えない．そのため，デジタル回路に変換可能を書き換え規則のクラスは限られている．本 研究ではまずヒープやスタ ックを必要としをい書き換え規則のクラスに対して宣言的仕様に対する正当性を保存したまま回路化する研究を行った．具体的には，末尾再帰の書き換え規則でデータに可 変長リストを含まをいもの を対象としている．このクラスの書き換え規則は有限状態マシンで計算 でき，そのよう顔有限状態 マシンを生成する方法として全ての書き換え規則をーつにマージする手法を開発した，
本研究が採用 している回路および協調計 算システム生成の特徴は，書き換え規則の集合をプログラム変換し顔が らデジタル回路，あるいは 協調計算システムのプログラムヘ変換させていることである．この生成過程では，書き換え規則のプログラム変換を何度も繰り返しをがら宣言的仕様に対する正当性を保持 したままデジタル回路へ変 換する方法を採用している．その中には書き換え規則の書き換え対象を変換することや，複数の書き換え規則をマ←ジする方法が合まれる，さらに書き換え規則を有限状態 マシンとして実現する際に は，使用するレジスタの数を減らし回路をコンパクトにすることも重要 であり，そのためにメタ計 算によって計算過程で出現する状態数を調べ上げることも必要である．そしてこのようを変換の流れを数学的に考察してゆくことによって，書き換え規貝l亅をー 864ー

プログラム変換す ることが「代数系の変換」によって実現されていることを明らかにしている，代数系の変換の正当性は，変換前の代数系（プログラム）と変換後の代数系（プログラム）との間に，ある条件を満たす写 像が存在することによって保証される，この写像を見つけることで様々なプログラム変換が可能とをり，一般性を持った変換の体系を作ることができた．その結果，回路生成の方法を広げ，さらにソフトウェアの生成にも応用できる方法が得られた．
上記で得られた 代数系の変換の体系によってハードとソフトの両方を生成する基礎を与えることができる．本研究では，この結果と既存の等価変換理論に関する研究との組み合わせによって，宣言的仕様から正しい デジタル回路および協調計算システムを自動生成する枠組みを提案している．問
題を計算する上で ヒープやスタックを必要とするようを処理や複雑教条件判定を含む処理をソフトウェア(CPU)に任せ ，単純で並列計算可能を部 分をデジタル回路で実行すれば計算のスピードを上げることができる，この枠組みは，宣言的仕様に対する正当橡デジタル回路や協調計算システムを自動生成する数学的を基礎を与えるものである，この枠組みによって，制約充足問題等を解く協調計算システムを安全に容易かつ短期間に開発できることが期待できる．
本 研 究の 中で は， 実際 に ソフ トウェア とハードウェアの協調計算を 簡単に実験できるようにFPGAを 利用し た「協調計算システム」を開 発している.FPGAは動的にデ ジタル回路を再構成できるLSIであり，PC上 のプログラムから任意にデ ジタル回路を構成し利用できるようにをっている，
この協調計算シス テムの性能を示す例題として「お絵かきロジック」と呼ばれるパズルゲームを解
く時間を計測し，ソフトウェア単体での計算時間との比較を行った．簡単な問題に対しては通信時間のオーバーヘッド により優位性はわずかであったが，計算量の多い複雑を問題に対しては協調計算の圧倒的な優位性 を示すことができ，協調計算システムが複雑を問題に対して有効であることを実験的に示した，

ー 865ー

学位論 文審査の要旨
主査 教 授 小野 哲雄
副査 教 授 古川 正志
副査 教 授 栗原 正仁
副査 教 授 鈴木 恵二
副査 准教授 山本雅人

学 位 論 文 題 名宣 言的仕様 に対す る正当な デジタ ル回路および
協 調計算 システム の自動生 成に関する研究
本研 究は形 式仕様 の記述 から自 動的に正しいデジタル回路やプログラムを生成する高位合成の研究である，高位合成は古くから研究されているが実用化されるに至っていをい．本研究では，ひとつ の形式 仕様に 対して 正当か つ様々 をアルゴ リズム を生成 できる「等価変換理論(EquivalentTransformation Theory： ET理論）」を利用する.ET理論では形式仕様を論理式（確定節）によって宣言的に記述する．この宣言的仕様は求解問題や制約充足問題をどを確定節によって定義したものである．さらにET理論によって問題を解く手続きを自動生成する基礎が与えられている．この生成され た 手 続 き を 記 述 す る 言 語 が 「 ETル ー ル 」 と 呼 ば れ る 書 き 換 え 規 則 で あ る ．
第1章から第 3章は本 研究を 理解す るため に必要 を前提 知識の説明である．第1章は研究の概要とデ ジタル 回路に ついて の基礎 的を説 明である ．デジ タル回 路の構造や現在主流のHDLによる設計 方 法の ほ か ， デジ タ ル 回 路や 協 調 計 算シス テムの 設計に おける 困難につ いて述 べてい る．
第2章は宣言 的仕様についての説明である．宣言的仕様の記述に用いられる確定節について説明
した 後，従 来の論 理プロ グラミ ングとET理論のそれぞれについて宣言的意味と正当性の保証の仕方を述べている．
第3章 はET理 論お よ び ETル ー ル に つい ての 説明で ある.ETル ールの シンタ ックス ，ETルー ルのセマンティクスの説明とET理論の特徴について述べている，
第4章から第 7章にか けて著 者の研 究成果 が述べ られて いる，第4章は，ETルールからデジタル回路 を生成 する基 礎的を 手法を 論じて いる.ETル ールに よる計算が状態遷移モデルとして捉えられることに着目し，ETルールと等価な計算を行う有限状態マシンを生成すればよいことを示し，そのよ うを有 限状態 マシン を生成 する方 法として ，全て のETルー ルをマ ージし て等価 をーつのET
ルー ルを生 成する 手法を 考案し ている．マージされたETルールのへッドアトムおよびポディアト
ムを それぞ れ「現 在の状 態」お よび「次の状態」とみをすとE
Tルールの実行部が遷移関数の働きをし ている ことを 述ベ， 実際に 例題を 用いてETルール がマージ されて ゆく過 程を示 している．
第5章は，第4章の変換過程を理論的に考察し，汎用的を回路生成手法ヘ発展させている，まず回― 866ー

路の状態遷移をET計算モデルの節の書き換えに対応させて正当性を論じている．その後，より抽象的を議論のために回路のドメイン（レジスタ）とET計算モデルのドメイン（確定節）の間の写像を導入し，この写像により異をる代数系（ドメインと演算の組）の間で計算の等価性を議論できることを 論じている．この議論により第4章で不透明であった「同じ終了状態ヘループするプログラム」の正当性に問題が極いことを示している．さらに後半では，代数系変換理論を基礎としてプログラム変換の可能性を広げている．メタ計算によって計算ドメインを有限を範囲ヘ絞り込んで回路レジスタの数を最適化する方法や，「並列的」「シーケンシャル」「排他的」の3種類のルールマージ方法についてのアイデアを論じている．
第 6章は， 第5章の 成果で ある代 数系変 換を応用 して様 々をタ ーゲッ トデバイスに応じたETプ
ロ グラム 変換を可 能にす る「ETルール変換フレームワーク」を提案している．この提案フレームワークは，ターゲット上への実装方法を決める「ポリシー」と，ETルールをどのようを手順で変換するのかを決める「ストラテジー」が大切であることを述べている．
第 7章は．ETプログラムとデジタル回路の協調計算の実験を容易にするために作成した，再構成
可 能を柔 軟誼協調 計算シ ステムを紹介している．前半ではETルールと協調計算システムの親和性について論じ，このシステムの構成の説明をおこをっている．後半では「お絵かきロジック」と呼ばれるパズルゲームを用いてシステムの性能の実験をしている．この実験の結果，複雑を制約充足問題に対して協調計算システムが非常に有効であることが示されている，
第 8章は 結諭で ある， 本研究 の成果 のまと めと， 今後の課 題や発 展性に ついて 述べて いる．
以上を要するに、本論文では宣言的仕様からデジタル回路を自動生成する高位合成の方法、および宣言的仕様からソフトウェアとハードウェアの協調計算システムを自動生成する協調設計の方法を提案しており、実際にデジタル回路をプログラム変換により生成し、さらに協調計算システムの開発を行い、研究の優位性を示している。よって、著者は博士（情報科学）の学位を授与されるに値するものと認める。

― 867―