形式等価判定
レジスタ転送レベル(RTL)でのデジタルチップの振る舞いは通常、VerilogやVHDLといったハードウェア記述言語で記述される。この記述によりクロックサイクル毎にどの部分がどう動作するかが詳細に記された重要な参照モデルが作られる。レジスタ転送記述を設計者がシミュレーションなどで検証した後、その設計を論理合成ツールに入力してネットリストを生成する。等価性と機能の正当性とは異なる概念である。後者は機能検証によって検証されなければならない。
ネットリストはその後、最適化や Design For Test(DFT)構造の追加などの変換が行われ、物理レイアウトに置かれる論理要素の基盤として使われる。最近の物理設計ソフトウェアはネットリストにも大幅な変更を加えることがある。このような複雑な多段階の処理を経たとしても、当初の設計上の振る舞いは保持されなければならない。最終的なテープアウトからチップが作られたとき、各種EDAプログラムや手による編集でネットリストが変更されているだろう。
理論上、論理合成ツールは最初のネットリストがRTLソースコードと論理的に等価であることを保証している。その後の工程でのネットリスト更新に関わるプログラムも、理論上は、それらの更新が論理的に等価であることを保証している。