同期回路の等価性

ウィキペディア小見出し辞書

同期回路の等価性

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2014/03/16 22:54 UTC 版)

「形式等価判定」の記事における「同期回路の等価性」の解説

レジスタ転送レベル（RTL）でのデジタルチップの振る舞いは通常、VerilogやVHDLといったハードウェア記述言語で記述される。この記述によりクロックサイクル毎にどの部分がどう動作するかが詳細に記された重要な参照モデルが作られる。レジスタ転送記述を設計者がシミュレーションなどで検証した後、その設計を論理合成ツールに入力してネットリストを生成する。等価性と機能の正当性とは異なる概念である。後者は機能検証によって検証されなければならない。 ネットリストはその後、最適化や Design For Test(DFT)構造の追加などの変換が行われ、物理レイアウトに置かれる論理要素の基盤として使われる。最近の物理設計ソフトウェアはネットリストにも大幅な変更を加えることがある。このような複雑な多段階の処理を経たとしても、当初の設計上の振る舞いは保持されなければならない。最終的なテープアウトからチップが作られたとき、各種EDAプログラムや手による編集でネットリストが変更されているだろう。 理論上、論理合成ツールは最初のネットリストがRTLソースコードと論理的に等価であることを保証している。その後の工程でのネットリスト更新に関わるプログラムも、理論上は、それらの更新が論理的に等価であることを保証している。 実際にはプログラムにはバグがあり、RTLから最終テープアウトまでの工程で何の問題も発生していないと考えるのは危険である。また、設計者が自らの手でネットリストに修正を加えることも珍しいことではない。これをEngineering Change Order（ECO）と呼ぶが、これも主たるエラー発生要因となる。 従来から行われている等価判定は再シミュレーションである。最終ネットリストを使い、RTLの正当性検証用に作成されたテストケースを用いる。この工程をゲートレベルの論理シミュレーションと呼ぶ。しかし、この方法の問題点は判定の品質がテストケースの品質に左右される点である。また、ゲートレベルのシミュレーションは非常に時間がかかり、集積回路の大規模化にあたっての重大な問題となっている。 別の方法は、RTLコードとネットリストがあらゆる面で等価であることを形式的に証明するものである。これを形式等価判定と呼び、形式的検証の研究課題の1つとして研究が進められている。 形式等価判定は任意の2つの設計表現の間で行うことができる（RTLとネットリスト、ネットリストとネットリスト、RTLとRTLなど）。形式等価判定ツールは、2つの設計表現に差異を発見すると、一般に非常に正確に問題箇所を指摘することができる。