[博士学位論文] [信州大学], March,1997.
また, 人工衛星や航空機,原子力発電所等の制御には, 一過性または縮退性の 故障が発生したとしても, 障害が外界に波及しないようシステムを構成する方 策としての, フォールトトレラント性の考慮が必要である. これらの制御シ ステムを構成するディジタル回路には, 回路が高速で作動するための設計方法, 回路設計の仕様自体の検証方法, 耐故障性を有しており信頼性の高い回路の構 成方法, 仕様通りに正しく動作することを検証する方法等, 様々な回路設計手 法が必要不可欠である．
ここの主要問題は, 次の2点に絞られる.
(1) 信頼性が高く, かつ高速に作動するディジタル回路を,いかに効率 良く設計するか.
(2) 仕様通りに回路設計がなされており, かつ正しく作動することを, どの様に検証・証明するか.
高速ディジタル回路が仕様通り正しく作動しない, という点で問題となった社 会的な事例としては, 1995年に発表された改良型Pentiumプロセッサ（インテ ル製）の設計誤りが記憶に新しい. これは, プロセッサと共に内蔵されたパイ プライン型浮動小数点演算回路（FPU）の設計誤りにより,一定の条件の下, あ る演算結果の信頼性が損なわれたものである．プロセッサ自体の信頼性が低い ことは, コンピュータシステム全体の信頼性の低下に直結する．結局, 当該演 算部分をソフトウェアのパッチ（継ぎ剥ぎ）で修正する様々な試みが行われた が, 上記の設計誤りを修正した版が行き通るまで, 世界的な混乱を免れること はできなかった.
ディジタル回路システムの信頼性は, トランジスタの出現以降, 素子レベルで は飛躍的に改良向上された. 一方で, 上記のマイクロプロセッサの例のごとく, ハードウェアの規模が増大した結果, 設計時の誤りをいかに防ぐか, その方策 を探る必要性が高まった.
コンピュータ同士が通信回線で接続され, 情報化社会が進展した結果, 実時間 （リアルタイム）処理システムが, 社会生活のあらゆる分野に利用されるよう になった．このような通信システムの故障の影響を, 直接受けてしまう社会的 システムの脆弱性が問題視されることが多くなってきた. システムは一瞬の 停止も許されなくなってきているにも関わらず, 大抵の場合, 冗長系構成で解 決しようと試みる. 結果, 信頼性向上や設計検証のためのコスト配分や技術が 不十分なため, 航空機, 原子力発電所等での重大事故の発生をみてしまう例が, 近年増加している. ソフトウェアとヒューマンインターフェースに関する技 術不足が関係している事例もある. しかしながら, 中枢を担うべきディジタ ル回路を実装・稼働する以前に, その設計で（たとえ誤操作によるエラーが発 生したとしても）仕様通りに正しく動作を行うことを論理的に検証すべきであ り, 制御に必要な演算回路の, 高速動作の正当性や安定性を証明すべきである. これらの方策の結果, 回路レベルからボトムアップ的に信頼性が確保され, シ ステム全体の信頼性向上に多大な影響を及ぼすことが期待できる.
以上の状況に鑑み, 本論文では, 高速に作動するディジタル回路の論理的設計 手法に関する研究と，その通信・画像処理・演算回路への応用について述べる． ディジタル回路においては，高速性，信頼性，設計と動作の正しさ等の検証が 必要である．これらの各要求に関して, 第1章では通信システムの信頼性向上, 第2章ではシステム設計仕様の検証, 第3章では高速パイプライン型回路の設計 手法について論じ,第4章では演算回路の動作の正しさを数学的に証明する.
通信制御装置などに使用されるバッファには，通信系の同期確立を行うために 内部に格納されているデータの数を外部へ通知したり，信頼性を確保するため にメモリ内部の一時的な障害に対して自己回復する機能が必要である．しかし， 既存のバッファはこれらの機能を持たないという問題点がある．ここでは, セ ルオートマトンの概念を導入して，通信バッファとしての条件を満たすFIFO型 メモリのモデル化を提案する．このモデルは基本的な動作を行なうセルを直列 にいくつかつなぎ合わせたものである．各セルは自己と近傍の状態によって有 効な先頭データを保持しているか否かを認識できる．更に，提案するモデルは， その内部に一時的な障害が起きた場合に必ず正常な状態に戻る，自己回復能力 をもつ. これらの能力を有する通信バッファを用いることにより，既存の構成 方法によるメモリに比較して高い通信系の信頼性を確保できる．次に, 各セル を順序回路で構成し，実際にゲートアレイ上で試作し，従来の構成方法による メモリと性能の比較を行い，提案するバッファの有効性を確かめる．
回路システムを設計する際に特に考慮しなければならないものに，(1)設計し たシステムが安定して動作するか，(2)システムが目的とする速度で作動する か，の2点がある．
このうち (1)システムの安定性に関しては，従来よりペトリネットを用いるこ とで，デッドロックやトラップ状態の有無が検証できることが知られている. 一般の実システムでは，入力データの値に応じて出力を変化させる場合が多い. このため, 従来のペトリネットを用いて実システムを設計しようとすると，入 力条件に応じて別々のプレースを用意せねばならずネット規模が大きくなり過 ぎてしまい, 記述は困難である．この問題を解決するため，実並列システムを 容易に記述できるようペトリネットの要素を拡張する．拡張されたネット （LC-Petri net）をそのままハードウェアに変換することは回路が複雑になり 過ぎて困難であるから,マークネット（Boolean Marking Net, BMN）への変換 方法を与える．BMNはハードウェアへの変換に適したペトリネットである. LC-Petri netは等価な動作を行うBMNへ変換した後, 更に回路への変換を行う.
一方, (2)システムの動作速度については，現在, 広帯域ネットワーク等,高速 で作動をさせたいディジタル回路の需要は極めて大きく，回路の高速化につい ての検討は重要になっている．この回路の高速化も，設計元になるペトリネッ ト上で議論できる．回路を高速化するには，複数のトランジション発火評価を 同時に並行して行えばよい．そこで，ペトリネット上で同時に発火評価しても 元の発火評価順序の場合と等価な動作をするトランジションを探す必要がある． システムをペトリネットで表現するとトランジションの発火評価に自然な順番 が入ることが多いが，従来のネットではこの概念がないため，発火評価順序と いう概念を LC-Petri netへ導入する．BMNではトランジション発火系列の等価 性や交換可能性といった性質について既に検討が行われている.
本論文では，更に，LC-Petri net を実際のパイプライン構成された画像処理 装置を制御するシーケンサ設計に適用し，その記述能力について確かめる.
復号処理を高速に行う試みは, G4ファクシミリ用高速復号LSIの試作をはじめ, 様々な研究がある. 復号処理の高速化は,画像処理以外の分野でも必要であり, 様々な研究がある. 例えばハードディスクの記録符号の復号処理において,高 速転送の要求を満たす復号方式とそれを実現するLSIの開発に関する研究等が ある.
ここでは,逐次, かつリアルタイムで復号可能な2値画像の符号化方式として, 2進桁圧縮符号(BPC符号)と,その復号ハードウェアの構成方法を提案する. こ の符号は,既存のbit分割符号と同様に, Run長を一旦2進数へ変換し,各桁に対 応した可変長符号を対応付ける. BPC符号は逐次リアルタイム復号が可能な他, 圧縮率はMH,bit分割符号化方式と同程度,復号処理が簡単でハードウェア実装 が容易で規模も小さい,等の特徴を有している.
復号処理性能を向上するために,新しいパイプライン型の復号処理方式を提案 する. 復号処理をパイプライン化し, 1クロック毎に1bitの速度で定常的に復 号した画素を出力するために, 圧縮データを数bit分先読みするバッファを設 ける等,逐次リアルタイム復号に適したパイプライン構成法を考える. BPC符号 を用いることで, 上記の高速復号処理が可能なハードウェアは容易に実現可能 であり, 有効であることを本論文は示している. 更に, この高速復号ハード ウェアを,実際にゲートアレイ上へ実装し試作した. 復号ハードウェアを,逐 次リアルタイムで復号処理が必要な画像処理装置に組み込んで評価試験を行っ たところ, 提案方式の有効性が確認された.
ディジタル回路を設計する際, 最も重要となる点は, 「ロジック」と「タイミ ング」の問題である. 回路の設計検証における従来の研究では, この2つの問 題を同時に議論しようとする場合が多かった. これらを同時に解析的に検討す るとき, 実回路では問題が複雑になりすぎ, 回路の範囲を限定した上での小規 模回路での議論に留まっている.
上記の問題点を解決するためには, 「ロジック」と「タイミング」の問題を分 けて検討することが有効と考えられる. このうち, 「タイミング」の問題に 関しては, 信号伝搬を「タイミングベルト」という概念によってモデル化し, それを用いた回路のタイミング検証手法が既に提案されている.
本論文では, 「ロジック」の問題に関して, 演算回路の数学的定義を行い，そ の動作の正しさの証明について述べる. 回路を定義していくための数学的概念 は, 回路の構造として, 回路内の全信号点を表す状態空間, 入出力信号間の写 像で定義される演算子, 演算に必要な入力信号点を表す演算子から信号点への 写像,及び演算結果を表す演算子から出力信号点への写像, といった4つの空間 と写像の対として定義する. これは, 従来のシミュレーション手法などで用い ている,狭い条件下での演算子,信号線,遅延情報の組とは異なり, 信号点の状 態空間を0/1の値だけをとり得る2値空間だけでなく, ハイインピーダンス状態 や連続空間など,様々な空間で回路を定義できることを示している. この構造 を基に, 入力信号により出力信号が一意に決定できる演算子を一つだけ持つよ うな演算回路を定義する．この結果, 演算子が当該回路の入出力信号点の間を 写像する関数として正当か, 結果が一意に定まる関数が存在するか, 入力信号 点の状態が変化した場合, 演算結果が安定となるか, などの重要な性質が数学 的に証明可能であることを示す. 次に, 演算回路の合成について定義する. 合 成後の回路は, 上述の構造における各空間・写像の和をとったものであり, こ の合成回路に関しても, 結果が一意に定まるか, 演算結果が安定となるか, な どの性質が証明可能であることを示す.
本稿では演算回路の具体例として 2の補数演算回路を取り挙げ, その回路構造 の定義,演算結果の一意性や存在性に関する諸定理, ならびに演算動作の正し さの証明を行い, 設計の正しさを数学的に検証することが目的である. 証明 は以下のステップで進める. まず,2の補数演算回路は, 1ビット分の2の補数 器を$n$ビット接続して構成する. 1ビット分の演算回路は, 2の補数器と桁上 がり演算器の2つを合成した構造で定義する. 各々の演算器は, 双方とも演算 子を一つだけ持つような回路で定義できるので,その定義を基に, 回路の入出 力信号に関する定理を導く. 最後に, 入力信号点の状態が決まれば, 演算結果 が必ず安定することを証明する. これらの定義・定理および証明を, Warsaw 大学で開発された MIZAR proof checking system を利用し, 検証している.