-1-
高速ディジタル回路の
論理的設計手法について
和﨑 克己
高速動作する
ディジタル回路の需要
-3-
• 情報通信,コンピュータシステム,移動体通信
• 人工衛星や航空機,原子力発電所の制御

ディジタル回路設計手法
– 回路が高速に動作できるための設計方法
– 回路設計の仕様自体の検証方法
– 耐故障性を有しており信頼性の高い回路の構成
方法
– 仕様通りに正しく動作することを検証する方法,
等々…
-4-
高速ディジタル回路が
仕様通り正しく動作しない…
 (例)初期型Pentiumプロセッサ
– 浮動小数点演算回路の設計誤り
– プロセッサ自体の信頼性が低い
– システム全体の信頼性の低下に直結
 ディジタル回路システムの信頼性
– トランジスタ素子レベルでは飛躍的に改良向上
– ハードウェア規模が増大 → 設計時の誤りを如
何に防ぐか,その方策を探ることは急務である
-6-
何を為すべきか?
 その設計で,“誤操作によるエラーが発生
しても”,仕様通りに正しく動作を行うことを
論理的に検証すべき
 制御に必要な演算回路の,動作の正当性
や安定性を証明すべき
 回路からボトムアップ的な信頼性確保
 システム全体の信頼性向上に多大な貢献
-7-
論文の構成

高速動作するディジタル回路の論理的設
計手法に関する研究

通信・画像処理・演算回路への応用

「高速性,信頼性,設計と動作の正しさ等
の検証が必要である」という立場で展開
-10-
通信用バッファに必要な条件
 通信系の同期確立
– 内部に格納されているデータの数を外部へ通知
 信頼性を確保
– メモリ内部の一時的な障害に対して自己回復す
る機能
 (例)LANを用いた音声伝送システム
図1.1 LAN上のノードにFIFO型メモリを用いた音声伝送の例
-OHP-
(a) 多段ラッチ構成
(b) リングバッファ構成
図1.2 多段ラッチ・リングバッファ構成をとるFIFOメモリ
-OHP-
-14-
セルオートマトン概念を用いた
通信バッファ
 基本的な動作を行うオートマトン(セル)を
定義
 各セルをメモリ深さ分だけ直列に接続
 前後のセルを近傍系とする
– 自己の状態と近傍セルの状態
– 先頭データ保持の有無を認識できる
(a) i番目のセル Celli の近傍系
(b) セルの遷移図
図1.3 セル近傍系とステートマシン
-OHP-
Read Operation
Write Operation
(a) FIFOメモリの機能ブロック図
(b) 書き込み/読み出し時のフラグ推移
図1.4 機能ブロックとフラグの推移
-OHP-
-17-
自己回復性 (耐故障性)
 メモリ深さ
n , 待ち行列先頭 Celli
障害発生フラグ Flagk のとき…
CASE-1 : クリアからセット状態に誤る場合

– (1) 読みだし操作
1回で回復
– (2) 書込み操作 (n-k+1)回で回復
CASE-2 : セットからクリア状態に誤る場合
– (1) 読みだし操作
– (2) 書込み操作
(i-k)回で回復
(n-k)回で回復
Read Operation
Read Operation
Write Operation
Write Operation
CASE-1 : クリアからセット状態に誤る場合
CASE-2 : セットからクリア状態に誤る場合
図1.5 自己回復過程のフラグ推移
-OHP-
既存メモリ構成方法との
性能比較
 有効データ数の通知機能
 障害回復性
 動作速度
 メモリ容量に対する回路規模
 バッファのゲートアレイ
(FPGA)実装
-19-
トランジション
プレース
アーク
図2.1 簡単な機械工場のペトリネットモデル
-OHP-
-22-
既存ペトリネットの低記述性
 ペトリネット
(Petri net)
– 並列性をもつシステムモデル設計に適する
– ネット解析 → 設計・動作の正しさの検証
– 視覚的にシステム状態の推移を観測できる
 既存ペトリネット
– プレーストランジションネット,カラーペトリネット
– ネット動作が一意に固定
– 実システムの記述には分岐処理等,ネット規模
が増大
(例)次のような条件で連続的に整数演算を行うシステム
図2.2 演算器の LC-Petri net モデル
-OHP-
-24-
論理カラーペトリネット
(Logical Coloured-Petri net)
 発火条件の拡張
– 入力プレース内トークンの有無,データ値によ
る任意の論理式で与える
 発火後のトークン移動条件の拡張
– 入力プレース内トークンのデータ値による関数
で自由に設定できる
 処理分岐用のネット要素追加が不要
– 実システムが“現実的な規模”で設計可能
-25-
LC-Petri netの解析方法
 LC-Petri
net への発火評価順序の導入
 LC-Petri net から Boolean Marking Net
(BMN)へ変換
– 厳密解析,ハードウェア化,クロック配分…
Tree)による探索
 Petri net Design System Tool による,シ
ミュレーション解析
 可達木(Reachability
制御用シーケンサの
LC-Petri netモデル
 画像処理装置の制御用シーケンサを
LC-Petri net により設計
 パイプライン構成された処理装置
– 並列度=3 の並行処理が要求された
 検査画像の取り込み
 基準画像の展開
 マッチング処理
-26-
(a) 機器構成図
(b) 処理装置の内部パイプライン構造
図2.3 画像処理システム
-OHP-
図2.4 画像処理のための LC-Petri net 図
-OHP-
-29-
ネット解析とその評価
 初期マーキングの設定
 可達木によるトランジション発火系列の探索
 システム異常状態の検出
– 設計の不備がネット解析により判明
 試験用コンピュータへの実装
– Petri net Design System Tool を使用
– 各シーケンスを視覚的に確認
試験用コンピュータの様子
図2.5 LC-Petri net図から生成した可達木(一部分)
-OHP-
-32-
逐次リアルタイム復号
S, アクティブ時間 A
 シーケンシャル性, 実行時間予測性
 リアルタイム復号
 セットアップ時間
– セットアップ時間SでM画素を一定の時間間隔
で次々と復号可能
 逐次リアルタイム復号
– シーケンシャル性とリアルタイム復号の両方
の性質を持つ
-33-
高速画像処理の要件
 セットアップ時間Sが小さい
 逐次リアルタイム復号である
 画素出力時間の間隔が小さい
図3.1 セットアップ・アクティブ時間を含んだ復号時タイミング
図3.2 パターンマッチングを行う画像処理アプリケーション
-OHP-
-36-
2進桁圧縮(BPC)方式
 符号器
(BPC encoder)
– Run-length計算
– 2進桁対応
 前段のRun-length計算の結果を入力としブロック
長を2進数に変換する
Lengthn  a0 2 0  a1 21    a K 1 2 K 1
ak ( k  0,1,, K1) は 0 ま たは 1
– 符号テーブルによる量子化
図3.3 BPC方式の基本システムとコード表
-OHP-
-38-
符号化の例
 入力bitストリーム
Length1  0000012 ; Length2  0000102
Length3  0001002 ; Length 4  0110002
 得られたBPC符号
[000][101][010][111011110][0111111111]
-39-
リアルタイム復号ハードウェア
 復号器
(BPC real-time decoder)
– 3bit先読みレジスタ
 常に圧縮データの先頭3bitを同時に参照
– 符号探索ステートマシン
 符号の展開が完全に終る前に出力を開始
– Bit出力カウンタ
 復号器のゲートアレイ
(FPGA)実装
– セットアップ時間S=85x3[nsec]
– 出力間隔85[nsec]
図3.4 先読みレジスタ・符号探索ステートマシン
-OHP-
図3.5 FPGA実装・復号タイミングチャート
-OHP-
-43-
演算回路の数学的定義
 回路の構造
– Many Sorted Signature
 演算回路,入力p,演算子f
– 1GateCircStr(p,f)
 回路の入出力信号
– InputVertices, InnerVertices
 演算回路の合成
 動作後の回路の状態
– Following(s) is stable.
 Mizar
proof checking system を使用
して証明の正しさを検証済み
図4.1 回路の構造 Many Sorted Signature
-45-
論理演算子の定義
 論理演算子
– Boolean Operator の概念
 演算回路の論理演算結果
– “1GateCircuit(p,f) は Boolean である”
 2入力型論理演算子
– and2*, nand2*, or2*, nor2*, xor2*
 3入力型論理演算子
– and3*, nand3*, or3*, nor3*, xor3*
2の補数回路
-46-
~動作の正しさの証明~
 演算回路
– 1bit分の 2の補数回路を n-bit接続 → 実現
 2の補数器,桁上がり演算器を定義
– 回路の入出力に関する諸定理を導出
 1bit分の演算回路
– 「2の補数器」 と 「桁上がり演算器」を合成
 動作の正しさの証明
– 入力信号点の状態が決まれば演算結果が必
ず安定することを示す
図4.2 2の補数回路の構造 BitCompStr(p,f)
-48-
結論
~何を明らかにしたのか~
 ディジタル回路においては,「高速性」,
「信頼性」,「設計と動作の正当性」等の検
証が必要である.これらの各要求に関し,
–
–
–
–
1.通信システムの信頼性向上
2.システム設計仕様の検証
3.高速パイプライン型回路の設計手法
4.演算回路の動作の正しさを数学証明
 以上の方策について明らかにした
-49-
今後の応用研究
 2次元セルオートマトン
– シストリックアレイ演算器
– 設計検証,耐故障性
 LC-Petri
net デザイン
– ゲートアレイ設計へ直結,回路の自動生成
 複雑な演算回路
– 固定・浮動小数点演算器(加減算,乗除算,
等々)の設計検証への応用
ダウンロード

公聴会PPT