デバイスの記事

第4回

フォーマル・ベリフィケーションの基本原理（3）――2 分決定グラフの変数順序を決める
藤田昌宏

今回は，論理関数の正規表現である2 分決定グラフの変数順序順の一つである「x 1，x 2，x 3，x 4，x 5，x 6」の場合，ノードの決めかたについて解説する．同じ論理関数を表現した2 分決数は変数の数に比例します．一方，最悪変数順の一つであ定グラフであっても，変数順が変わるとノード数が大きく変化る「x 1，x 3，x 5，x 2，x 4，x 6」の場合，ノード数は変数の数する．コンピュータ上で高速に処理するためには，ノード数がの指数に比例します．

少なくなる（つまり，計算量やメモリ使用量が減る）変数順序をこのように，2分決定グラフを利用する立場からすると，見つける必要がある．ただし，乗算器のように，変数順をどう変数順の決めかたはきわめて重要な問題となります．この変えても，2 分決定グラフのサイズが爆発するタイプの回路も変数順は，EDAツール（フォーマル・ベリフィケーショある．

ン・ツールなど）によって自動的に決められることが多い（編集部）のですが，場合によってはユーザが手を加えることもでき前回まで，フォーマル・ベリフィケーション（形式的検るようです．

証）を支える基礎技術として，計算機上で使われる論理関LSIの回路において，論理関数全体の値を決めるとき，数のコンパクトな表現法である「2分決定グラフ（BDD：一般に，制御部の変数の値はデータパス部の変数の値よりbinary decision diagram）」について説明してきました．今影響力が大きいと考えられます（制御部のほうが，データ回は，2分決定グラフを利用するうえで重要な「変数順の決パス部より結線の数が多く，回路構成が複雑になるケース定・最適化手法」について説明します．前回も述べたように，2分決定グラフの大きさは変数順によって大きく変化が，加算器を表す論理関数や制御回路の論理など，LSIのいと思います．

x3x5x3x5x5x5x1x2

ことが少なくありません．今回は，2分決定グラフのための変数順決定法や変数順の逐次改善手法について説明した最悪順

最良順

ない（変数順最適化の効果があまりない）ものも多いのです

実設計で利用される論理関数については変数順に依存する

x1x 1x 2＋ x 3x 4＋ x 5x 6するのが普通です．論理関数の中には変数順の影響を受け

x2x2x2x2x3x4x4x4x5x6x6●よく考えられた回路図の変数順はBDD を小さくする
2分決定グラフの大きさは，使用する変数順に大きく依存します．前回も示しましたが，例えば図 1 の論理関数
x 1 x 2 ＋x 3 x 4 ＋x 5 x 6 に対する2分決定グラフを作成するとき，変数順が「x1，x2，x3，x4，x5，x6」か「x1，x 3，x 5，x 2，x 4，x 6」かによって，必要なノード数が異なります．最良変数

0

10

1

〔図1〕変数順による2 分決定グラフの大きさの変化
2分決定グラフの大きさは，変数順に大きく依存する．同じ論理回路の出力に対する2分決定グラフでも，最良の変数順と最悪の変数順ではノード数が大きく異なる．この例では，最良変数順の場合は回路の入力数に比例するノード数になるが，最悪順の場合は回路の入力数の指数に比例するノード数になってしまう．

Design Wave Magazine 2003 October 149

が多いため）．そのため，2分決定グラフの変数順を決める

変数順決定手法の典型的な例を説明し，その後で動的な変ときに，最初に制御部の変数を並べて，その後にデータパ数順改善手法を説明します．

ス部の変数を並べるという方法がよく用いられます．ある

実はこれ以外にもさまざまな手法が提案されています．

いは，後に述べるように，「同じゲートに接続されている「最適な変数順決定問題」は NP 完全問題（NP-complete

信号間の変数順は近いほうがよい」という規則に基づいてproblem；入力のデータ量に対して，指数関数的な処理時決めることも考えられます．

間がかかってしまう問題）であることが証明されているの人手で変数順を決める場合の一つの方法は，回路図上ので，すべての解をしらみつぶしに探索するようなことを行

変数順をそのまま2分決定グラフの変数順として採用する

わない限り，最適な変数順を見つけることはできません．

ことです．よく考えて作成された回路図の場合，同じゲー

そこで，計算時間が少なくてすむ各種のヒューリスティットに接続される信号は近くに集められています．また，見ク（最適解ではないが，比較的良い解が得られる経験的手やすくするため，できるだけ信号線の交差が少なくなるよ法）が提案されているわけです．ヒューリスティックであうに描かれています．このように「よく考えて作成されたるため，うまくいく場合もあれば，うまくいかない場合も回路図」が存在する場合には，回路図上に現れる変数順をあるわけですが，実際の設計に出てくる論理関数についてそのまま2分決定グラフの変数順にすると，比較的良い結は，比較的うまくいくケースが多いようです．

果が得られることが経験的にわかっています．
現在のLSI設計では論理合成ツールなどを利用すること●静的手法：出力から入力の方向へ深さ優先でたどるが多く，最近では設計者が回路図を作成することはまれで静的な変数順を決定するうえで，何が重要かを考えてみす．そのため，実際にはこの方法が使えないかもしれませましょう．まず，図1の最適変数順がどういう順番になっんが，知っておいても損はないでしょう．ているかを考えてみます．図1の論理関数は x 1 x 2 ＋x 3 x 4 ＋x 5 x 6 ですが，これを回路図で書くと図2のようになります．

●静的な決定手法と動的な改善手法がある

このようにきれいな回路図が描ける場合には，前述のよう実際のLSI設計では，設計者自身が2分決定グラフの変に，回路図に出てくる変数を上から（あるいは下から）順に数順を指定することはめんどうであり，かつ手間や時間も並べたものを変数順とすれば，結果的に良い2分決定グラかかるため，ほとんどの場合，変数順はツール側で自動的フが得られます．に決定されています．2分決定グラフの変数順を決める方

さて，この回路（あるいはネットリスト）から，良い変数法には，2分決定グラフを作成する前に決定する「静的な変順を自動的に得るにはどうすればよいのでしょうか？ 一つ

数順決定手法」と，いったん2分決定グラフを生成してから言えることは，同じゲートにつながっている信号は，変数（あるいは生成する途中で）変数順を改善する「動的な変数順として，隣り合っているほうがよいということです．こ順改善手法」の2種類があります．ここでは，まず，静的なれをいちばん簡単に満足する方法は，回路のネットリストを出力から入力の方向へ深さ優先でたどっていき，現れた外部入力の順番を2分決定グラフの変数順とすることです．

x1x2x 1x 2＋ x 3x 4＋ x 5x 6x3x4x5x6〔図2〕回路を出力から入力へ向かって深さ優先でたどる木構造となっている回路，つまり，すべてのゲートの出力が一つのゲートにしかつながっていない回路（再収れんのない回路）の場合には，回路のネットリストを出力から入力の方向へ深さ優先でたどっていき，現れた外部入力の順番を2分決定グラフの変数順とすることで，最適な変数順が得られる．これは単純な深さ優先なので，2段目のNANDゲートの入力をどの順にたどるかは自由であり，その意味で，いろいろな変数順が得られる．例えば，「x 1，x 2，x 3，x 4，x 5，x 6」や「x 3，x 4，x 1，x 2，x 5，x 6」，「x 5，x 6，x 3，x 4，x 1，x 2」なども最適な変数順となっている．

150 Design Wave Magazine 2003 October

この過程を図2に示します．これは単純な深さ優先なので，2段目のNANDゲートの入力をどの順にたどるかは自由であり，その意味で，いろいろな変数順が得られます．例えば，「x 1，x 2，x 3，x 4，x 5，x 6」や「x 3，x 4，x 1，x 2，x 5，x 6」，「x 5，x 6，x 3，x 4，x 1，x 2」などが考えられます．ここで注意
してもらいたいのは，これらのどれもが「最小の2分決定グラフ」を与える変数順だということです．
実用的な回路の多くは，図2に示すような木構造の回路ではなく，一つのゲートの出力が複数のゲートの入力になり，それらの出力が回路の後のほうで再度同じゲートの入