形式等価判定

出典: フリー百科事典『ウィキペディア（Wikipedia）』

形式等価判定（けいしきとうかはんてい、Formal Equivalence Checking）は EDAの一部であり、デジタル集積回路の開発過程において、ある回路設計についての2つの表現が同じ振る舞いを表していることを形式的に証明するために用いられる手法。

[編集] 等価判定と抽象化レベル

一般に、抽象化レベルの異なる（タイミングの詳細さも異なる）ものの機能的等価性の定義は様々である。

最も典型的な手法は、2つの同期設計仕様に任意の同じ入力信号を与えたときにクロック毎に全く同じ出力信号列を生成することをもって、それらのマシンが等価であるとする。
マイクロプロセッサ設計では、レジスタ転送レベル（RTL）実装での命令セットアーキテクチャ(ISA)仕様の機能の等価性を比較し、両方のモデルで同じプログラムを実行したときに主記憶の内容更新が等しいことを確認する。
システム設計フローでは TLM（Transaction Level Model）での比較を必要とする。例えば、SystemCで書かれたものとそれに対応するRTL仕様を比較する。SoC（System-on-a-Chip）設計ではこのような判定が重要性を増している。

[編集] 同期回路の等価性

レジスタ転送レベル（RTL）でのデジタルチップの振る舞いは通常、VerilogやVHDLといったハードウェア記述言語で記述される。この記述によりクロックサイクル毎にどの部分がどう動作するかが詳細に記された重要な参照モデルが作られる。レジスタ転送記述を設計者がシミュレーションなどで検証した後、その設計を論理合成ツールに入力してネットリストを生成する。等価性と機能の正当性とは異なる概念である。後者は機能検証によって検証されなければならない。

ネットリストはその後、最適化や Design For Test(DFT)構造の追加などの変換が行われ、物理レイアウトに置かれる論理要素の基盤として使われる。最近の物理設計ソフトウェアはネットリストにも大幅な変更を加えることがある。このような複雑な多段階の処理を経たとしても、当初の設計上の振る舞いは保持されなければならない。最終的なテープアウトからチップが作られたとき、各種EDAプログラムや手による編集でネットリストが変更されているだろう。

理論上、論理合成ツールは最初のネットリストがRTLソースコードと論理的に等価であることを保証している。その後の工程でのネットリスト更新に関わるプログラムも、理論上は、それらの更新が論理的に等価であることを保証している。

実際にはプログラムにはバグがあり、RTLから最終テープアウトまでの工程で何の問題も発生していないと考えるのは危険である。また、設計者が自らの手でネットリストに修正を加えることも珍しいことではない。これをEngineering Change Order（ECO）と呼ぶが、これも主たるエラー発生要因となる。従って全くミスがないと想定するよりも最新のネットリストと本来の設計の等価性を判定するための検証工程を設けるのが賢明である。

従来から行われている等価判定は再シミュレーションである。最終ネットリストを使い、RTLの正当性検証用に作成されたテストケースを用いる。この工程をゲートレベルの論理シミュレーションと呼ぶ。しかし、この方法の問題点は判定の品質がテストケースの品質に左右される点である。また、ゲートレベルのシミュレーションは非常に時間がかかり、集積回路の大規模化にあたっての重大な問題となっている。

別の方法は、RTLコードとネットリストがあらゆる面で等価であることを形式的に証明するものである。これを形式等価判定と呼び、形式的検証の研究課題の1つとして研究が進められている。

形式等価判定は任意の2つの設計表現の間で行うことができる（RTLとネットリスト、ネットリストとネットリスト、RTLとRTLなど）。形式等価判定ツールは、2つの設計表現に差異を発見すると、一般に非常に正確に問題箇所を指摘することができる。

[編集] 手法

等価判定プログラムでのブール推論に使われる技術には以下の2つがある:

二分決定図(BDD): ブール関数についての推論をサポートするよう設計された特別なデータ構造。効率性と汎用性の高さから、BDD は非常に一般的に使われるようになった。
乗法標準形充足可能性: SATソルバーにより、その論理式を満足する変数の組み合わせがあるかどうかを検証する。ブール推論問題は総じてSAT問題で表現できる。

[編集] 等価判定の商用製品

EDAでの主な論理等価判定（LED）製品としては以下のようなものがある:

Conformal（ケイデンス・デザイン・システムズ）
Formality（シノプシス）
SLEC（Calypto）

[編集] 一般化

リタイム回路の等価判定: 論理回路をレジスタの一方から他方へ移す必要が生じることがあり、これが判定問題を複雑化させる。
逐次等価判定: 組み合わせレベルでは全く異なる2つのマシンが、同じ入力に対して同じ出力を返す場合がある。この場合、組み合わせ問題に縮減させることはできず、より汎用的な手法を必要とする。
ソフトウェアプログラムの等価性: つまり、N入力でM出力の正しく定義されたプログラムの等価判定である。概念的にはソフトウェアを状態機械に変換することができる（コンパイラと実際のコンピュータが行っているのは、プログラムの状態機械への変換である）。そして理論的には各種特性を判定することで同じ出力を生成するかどうかを確認できる。これは出力生成タイミングが異なる可能性もあるため、逐次等価判定よりも難しい。しかし、判定は可能であり、研究が進められている。

[編集] 参考文献

Electronic Design Automation For Integrated Circuits Handbook, by Lavagno, Martin, and Scheffer, ISBN 0-8493-3096-3 A survey of the field. This article was derived, with permission, from Volume 2, Chapter 4, Equivalence Checking, by Fabio Somenzi and Andreas Kuehlmann.
R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers., C-35, pp. 677–691, 1986. The original reference on BDDs.