RTL2GDS: 論理等価性チェック、LEC

RTLがテープアウトされるまで、本当に多くのEDAツールを経ます。この過程でバグが一度も発生しないでしょうか？ ツールがバグでインバータを1つ追加してしまったらどうなるでしょうか？

形式検証、中でも論理等価性チェック（LEC）は、現代のASIC設計フローにおいて不可欠な方法論です。

LECはシミュレーションとは異なり、テストベクトルを使用しません。 代わりに、二つの設計表現が数学的・論理的に全てのケースにおいて同一の動作を実行することを静的解析する手法である。

LECの主な目的は、設計変換プロセスにおける完全性の確認である。RTL（レジスタ転送レベル）コードがロジック合成を経てゲートレベルネットリストに変換される際、 あるいはP&Rツールがタイミング最適化のためにロジックを修正するとき、そしてDFT(Design for Testability)プロセスでスキャンチェーンが挿入される際に、元の設計者の意図(Golden Design)が変更された設計(Revised Design)においても完全に保持されていることを確認するものである。

上記の図表からわかるように、 LECは、RTL対合成ネットリスト(RTL vs Netlist)、合成ネットリスト対DFTネットリスト(Netlist vs Netlist)、そして最終レイアウトネットリスト検証など、様々な段階で繰り返し実施される。

これは、各段階で発生し得るツールのバグやユーザーのミスによる論理的欠陥を即座に捕捉し、高額な再設計コストを防止する安全装置としての役割を果たす。

2. 形式検証の数学的およびアルゴリズム的基礎

LECが「数学的に証明する」という言葉の意味を理解するためには、その基盤となるアルゴリズム的原理を検討する必要がある。LECツールは主にBinary Decision Diagrams, (BDD）とBoolean Satisfiability, (SAT)という二つの核心技術を基盤として動作する。

2.1 Miter回路構成と反証ベース検証

LECの基本原理は、二つの回路（ReferenceとTest）を比較し、出力が異なるケースが「一つでも」存在するかどうかを検出することである。このため、ツールは仮想的なMiter回路を構成する。 マイター回路は、2つの回路の同一入力ポートを互いに結び、対応する出力ポートをXORゲートで接続した構造である。

論理的にXORゲートは、二つの入力が異なる場合にのみ「1」を出力する。したがって、LECツールの目標は「XORゲートが出力1となる入力の組み合わせが存在するのか？」という問いに答えることに帰着する。

• もしそのような入力の組み合わせ（反例、Counter-example）が存在するならば、二つの回路は非等価である。
• もし全ての可能な入力に対してXOR出力が常に'0'であるならば、二つの回路は等価である。

このアプローチは、「同一性を証明する」よりも「相違点を見つけること」がアルゴリズム的に効率的である可能性を示す反証法的な思考に基づいている。

2.2 バイナリ決定ダイアグラム（BDD） BDD

初期のLECツールの基盤となったBDDは、ブール値をDAG形式で表現するデータ構造である。BDDの最も強力な特徴は、標準形（Canonical Form）であるという点だ。

Canonical Formとは、論理関数を入力組み合わせ基準で完全に展開した標準表現である。 その意味は、特定の論理関数について変数順序が固定されている場合、その関数を表現するBDDグラフの形状は唯一であるということを意味する。これは検証プロセスを画期的に簡素化する。

ゴールデン回路と改訂回路のBDDをそれぞれ生成した後、両グラフがメモリ上で同一構造を持つか（すなわち、ルートノードからターミナルノードまでの経路が一致するか）をポインタ比較のみで確認できるためである。

しかしBDDには致命的な弱点がある。それはメモリ爆発問題だ。乗算器のような特定の算術演算回路や入力変数が多い複雑なロジックの場合、BDDのノード数が指数関数的に増加し、物理メモリの限界を超えることになる。 このため、BDD ベースの検証は、大規模 SoC 設計全体を処理するには限界があった。

2.3 満足可能性 (SAT) ソルバー

BDD の限界を克服するために導入された技術が SAT ソルバーである。 SAT は、与えられたブール式（主に CNF、Conjunctive Normal Form）を真にする 変数割り当てが存在するかを探索するアルゴリズムである。

LECの観点から、SATソルバーはMiter回路の出力(XOR)が'1'となるようにする入力条件を探す。SATはBDDのように全体の真理値表を圧縮して保存しようとせず、 深さ優先探索 (DFS)とバックトラッキング、そして学習技法を用いて解を見つける。

• 長所: BDDに比べてメモリ使用量がはるかに少なく、大規模回路でも効率的に動作する。特に反例を見つける速度が非常に速い。
• 短所:特定の問題では探索空間が膨大すぎて解を見つけるのに非常に長い時間がかかる可能性がある（NP完全問題）。したがって現代のLECツールはBDDとSATを混合して使用するか、回路構造に応じて適切なエンジンを自動選択するハイブリッド方式を採用する。

2.4 Logic Cone 分割

チップ全体を単一の巨大なブール方程式として扱うことは不可能である。したがってLECツールは設計をLogic Coneという小さな単位に分割して検証する。

• 比較ポイント (Key Points): 検証の基準点となる要素である。主にPrimary Output、Flip-Flopの入力(D-pin)、Black Boxの入力ピンなどが該当する。
• Logic Coneの形成: 各比較ポイントを頂点とし、その点に影響を与える全ての主要入力、フリップフロップ出力(Qピン)、ブラックボックス出力ピンなどを基底とする組み合わせ論理領域を定義する。

LECはこのLogic Cone単位でGoldenとRevisedデザインを1:1マッピングした後、各ペアが等価であるかを独立して検証する。これにより全体の問題の複雑度を'分割統治法'方式で解決する。

3. LEC検証プロセスの詳細ステップ

実際の産業現場でSynopsys FormalityやCadence Conformal LECといったツールを運用する際、検証プロセスは一般的にSetup、 マッピング、比較、デバッグの4段階の循環構造に従う。各段階は検証の信頼性を確保するために必須の詳細作業を含む。

3.1 ステップ1: 設計モデリング、セットアップ - 検証環境の構築

設定ステップは、比較対象となる2つの設計（リファレンス/ゴールデンおよび実装/改訂）をツールにロードし、正しい検証環境を構成するプロセスである。このステップでの些細なミスが後々多大なデバッグコストを招くため、最も注意が必要である。

1. ライブラリロード (Library Loading): スタンダードセル(Standard Cell)ライブラリ、I/Oパッドライブラリ、およびメモリやアナログIPなどのブラックボックスモデルをロードする。
   • Synopsys Formalityは主に.db (Synopsys Liberty Binary)形式を使用する。
   • Cadence Conformalは.lib (Liberty)またはシミュレーション用Verilogモデル(.v)の両方をサポートする。 重要な点は、両方のデザインが同一の機能的定義を持つライブラリを参照しなければならないということである。
2. デザイン読み込み (Read Design):
   • ゴールデンデザイン: 検証の基準となる設計である。主にRTL (Verilog、VHDL、SystemVerilog) コードとなる。 RTL を読み込む際には、elaborate プロセスを通じてパラメータを確定し、階層構造を生成する。
   • Revised Design: 比較対象となる設計である。Synthesis 後に生成された Netlist または P&R 後の Netlist である。
3. 制約設定: LEC ツールがデザインを正しく解釈するためのガイドラインである。
   • 定数の設定: ネットリストにはテスト用のスキャンチェーンロジックが含まれており、RTLとは構造的に異なる。したがって、Scan Enable信号を0（または非アクティブ値）に固定し、ツールがスキャンパスではなく機能パス(Functional Path)のみを検証するよう強制する必要がある。
   • 未駆動信号の処理: 入力が接続されていないポート(Floating inputs)を'0'、'1'、'Z'(High-Z)、または'X'(Don't Care)のいずれとして解釈するかを定義する。これを誤って設定すると、不要な不一致が発生する可能性がある。

3.2 ステップ2: デザインマッピング - 比較対象の関連付け

マッピングとは、Goldenデザインの比較キーポイントとRevisedデザインの比較ポイントを1:1で対応させるプロセスである。Synopsysツールチェーンの場合、SVFというファイルがこれを支援する。

• Name-based Mapping: レジスタやポートの名前が同一、または規則的なパターンを持つ場合に使用する。ツールは基本的に名前一致を最優先で試みる。
• Function-based Mapping: 名前が変更された場合（例：合成ツールが最適化過程で任意に名前を変更した場合、またはデータバスとして構成されたフリップフロップがマルチビットフリップフロップでバンキングまたはデバンキングされた場合）、当該ポートを駆動する論理的機能（Logic Cone）が類似していることを分析してマッピングを試みる。これは計算コストが高いが、名前規則が破られたネットリスト検証では必須である。
• Renaming Rules: ユーザーが直接マッピング規則を定義できる。 例えば、RTLのregがネットリストでreg_0_に変更された場合、ツールに_を``に置換してマッピングするよう指示できる。
• Unmapped Points分析: マッピングされていないポイントは比較対象から除外される。 これが意図的なもの（例：未使用ロジックの削除）か、エラー（例：名前変更ルールの欠落）かを必ず確認する必要がある。

ここで Unmatch list が発生する。LEC Fail だけでなく、Umatch list も検証者の分析が必要である。

3.3 ステップ3: デザイン比較

マッピングされたポイントのペアに対してLEC検証を実行する。ツールは効率性を最大化するため、多段階戦略を使用する。

• ランダムパターンシミュレーション: まず数千のランダム入力パターンを注入し、迅速に出力値を比較する。この段階で不一致が発生した場合、即座に非等価と判断し、コストの高いソルバーリソースを節約する。
• 構造解析および形式検証： ランダムパターンを通過したポイントについて、SAT または BDD ソルバー を起動し、形式的証明 を試みる。

結果は、以下の 4 つに分類されます。

1. Equivalent: すべての入力の組み合わせに対して出力が同じである（検証成功）。
2. Non-Equivalent: 特定の入力に対して出力が異なる（Setup Issue または Functional Bug）。
3. Inverted-Equivalent: 出力が正反対である （例：QとQbarのマッピング）。これは機能的には等価である可能性がある（位相反転を許容する場合）、注意深く確認する必要がある。
4. 中止 / Inconclusive: ツールが与えられた時間またはメモリ制限内で証明を完了できなかった。これは主に巨大な乗算器などの算術論理演算や、非常に深い論理深度を持つ回路で発生する。

3.4 ステップ4: デバッグ - 根本原因分析および修正

Compare ResultがNon-EquivalentまたはAbortとなった場合、Debugステップに進む。 これはLECエンジニアの能力が最も求められる段階である。一言で言えば、LECで失敗すると、デバッグが本当に難しい。

• 診断: 不一致を引き起こす反例を生成し、ロジックコーン内でどのゲートがエラー候補であるかstrong>であるかをBacktraceする。
• Pattern Analysis: ツールが提供するWaveform ViewerやSchematic Viewerを通じて、Mismatch Pointまで信号がどのように伝播するかを視覚的に分析する。 ユーザーは、RTL ソースコード と ネットリスト回路図 を並べて比較し、ロジック の相違点を見つけ出します。

4. 合成最適化と構造変換の処理

LEC検証の最大の難関は、RTLとネットリストが構造的に大きく異なる点である。 論理合成ツール（Design Compiler、Genusなど）は、Area、Power、Timingを最適化するために、RTLの論理構造を大幅に変化させる。こうした構造的変換をLECツールが理解できない場合、機能が同一であるにもかかわらず、不一致（False Negative）と判断してしまう。

4.1 組み合わせ論理最適化

最も基本的な最適化は、ブール代数の法則を用いたロジックの簡略化である。

• 定数伝播 (Constant Propagation): 特定の入力が定数で固定されている場合、関連するロジックを削除または簡略化する。LECツールも、同じ定数制約条件を知らないと、これをエラーと認識する可能性がある。
• ロジック複製およびマージ (Logic Replication & Merging): タイミング解決のためにファンアウト (Fan-out) の大きいゲートを複製したり、逆に面積を削減するために同一のロジックをマージする。LEC ツールは、このような多対一 (N:1) または一対多(1:N) マッピングを処理できる必要がある。

4.2 逐次論理最適化 (Sequential Logic Optimization)

組み合わせ論理だけでなく、レジスタ（フリップフロップ）自体を変形する最適化は、検証をさらに困難にする。

• リタイミング (Retiming): リタイミングはクリティカルパスの遅延時間を削減するため、レジスタを組み合わせ論理の反対側に物理的に移動させる技術である。この場合、RTLのレジスタ位置とネットリストのレジスタ位置が異なり、1:1マッピングが不可能となる。
  • 解決策:合成ツールが生成したSVF（Setup Verification File）やガイドファイルが必須である。このファイルには「RTLのレジスタAがネットリストのレジスタBに移動した」ことを説明する情報が含まれており、LECツールがこれを参照して比較点を再設定できるようにする。
  • 詳細はFormality® Automated Setup File (SVF) Manualに記載されています。
  • ただし、SVFにもバグが存在するケースがあり、SVFを使用すると失敗が発生し、SVFを使用しない場合は成功する事例もあります。
• パイプラインレジスタの最適化
• FSM再エンコーディング

4.3 階層構造の変更

設計の階層構造も最適化の対象となります。

• Ungrouping (グループ解除): 合成ツールは最適化効率を高めるため、下位モジュールの境界を取り払い(Ungroup)、上位モジュールと統合して平坦化(Flatten)する場合が多い。
  • 問題点: モジュール境界が消失すると階層的（Hierarchical）比較が不可能になり、全体設計を平坦化して比較する必要があるため検証時間が急増する。またsubmodule/regがsubmodule_regのように名称変更されマッピング失敗を誘発する。
  • 解決策: 自動名前マッピング機能を活用するか、重要なモジュールについては合成時にset_ungroup false属性を付与し、階層構造を保持するよう誘導すべきである。
• 境界最適化 (Boundary Optimization): モジュール境界を越えてロジックを移動させる（例：インバータをモジュール外に押し出す）、または入力ポートの定数を内部に伝播させる技術である。これも階層比較時に境界ピンでの不一致を引き起こすため、LEC設定でset flatten model -boundary_optimizationなどのオプションを有効化する必要がある。

5.低消費電力設計のためのLECとUPF

現代のモバイルおよびIoTチップ設計において、低消費電力技術の適用は必須である。マルチ電圧ドメインとパワーゲーティング技術の導入は、LEC検証に新たな複雑性を加える。

5.1 UPF/CPFとPower Intent

RTLコード自体にはPower Networkに関する情報はない。Powerドメイン、アイソレーション、レベルシフターなどの情報は、別ファイルであるUPF(Unified Power Format)やCPF(Common Power Format)に定義される。

LEC検証時には、このUPF/CPFファイルを一緒にロードする必要がある。ツールはこの情報に基づき、仮想的なPower LogicをRTLモデルに挿入し、実際の電力デバイスを含むネットリストと比較可能な状態にする。

5.2 低消費電力セル検証の課題

• アイソレーションセル: 電源がオフのドメインからオンのドメインへ信号が移行する際に、信号を特定の値（0または1）に固定（クランプ）するセルである。LECツールはUPFに定義されたアイソレーションルール(Isolation Strategy)がネットリストに正確に実装されているかを確認する。もしアイソレーションセルが欠落していたり、制御信号の接続が間違っていると不一致が発生する。
• レベルシフター: 異なる電圧レベルを持つドメイン間の信号伝達を担当する。機能的にはバッファ(Buffer)と同じだが、LECでは電圧レベルルールの遵守を確認する必要がある。
• State Retention Cell: 電源がオフになってもデータを保持する特殊レジスタである。LECは一般レジスタとリテンションレジスタ間のマッピングを処理する必要があり、そのためにはライブラリモデルが正確にロードされなければならない。

6. ECO（エンジニアリング変更指示）とLEC

チップ設計の後半、特にP&Rやマスク製作直前にバグが発見された場合、全体の合成をやり直す代わりに最小限のゲートのみを修正するFECO(Functional Engineering Change Order)を実行する。LECツールはECOプロセスにおいても核心的な役割を果たす。

• Functional ECO: RTLを修正した後、既存のネットリストに最小限のパッチのみを適用し、RTLと同一にするプロセスである。Conformal ECOのようなツールは、修正されたRTLと既存のネットリストを比較し、差異を解消するために必要なパッチロジックを自動生成する。
• Spare ECO Cellの活用:テープアウトが既に完了しており、FEOLプロセスまで完了している場合、チップ内部に予め配置された予備のゲート（Spare Cells）を使用し、BEOLメタル層を修正してバグを修正する必要がある。LECツールは利用可能なSpare Cellリストを入力として受け取り、これを利用した最適なパッチネットリストを生成できる。