設計検証（形式検証・等価性チェック・UVM）

なぜ「設計検証」が独立した巨大工程なのか

大規模チップ開発では、検証（バグを見つける作業）に投じる工数が設計そのものを上回ることが珍しくありません。理由は単純で、テープアウト後にバグが見つかると、マスク再作成と再製造で数か月と巨額の費用を失うからです。製造プロセスの正しさは/semiconductor/asic-design-flow/のサインオフ（DRC/LVS/STA）が担いますが、それらは「設計したものを正しく作れるか」を見るだけです。設計した機能そのものが仕様どおりかを保証するのは、別個の「設計検証（Design Verification）」の責任です。

検証の根本的な難しさは状態空間の爆発にあります。レジスタが100ビットあれば取りうる状態は2の100乗で、全パターンを流すシミュレーションは原理的に不可能です。だから現代の検証は、性質の異なる3つの武器を組み合わせて網羅性を作ります。

設計検証の3本柱（カバーする領域が異なる）:

  1. 論理等価性検証(LEC) : 変換前後で「同じ回路か」を全網羅で証明
  2. 形式プロパティ検証(FPV): 性質(アサーション)を全状態で証明 or 反例提示
  3. 制約付きランダム検証(UVM): 刺激を大量生成し機能カバレッジで網羅度を測る

論理等価性検証（LEC）── 変換が意味を変えていないか

設計フローは抽象度を下げる変換の連鎖です（/semiconductor/logic-synthesis/の論理合成、その後のスキャン挿入や手動最適化など）。各変換の絶対条件は、変換前後で論理的に等価であること、つまり全入力組み合わせで同じ出力を返すことです。これを証明するのが LEC（Logical Equivalence Check、論理等価性検証） です。

LECの肝は、2つの回路の出力XORが**恒偽（どんな入力でも0）**であることを証明する点にあります。これは充足可能性問題（SAT）に帰着でき、現代のSATソルバやBDD（二分決定図）で網羅的に判定できます。膨大な入力を1つずつ試すのではなく、等価でない入力が存在しないことを論理式として証明するため、シミュレーションと違い見落としがありません。

LECの基本原理:

  回路A(リファレンス) と 回路B(変換後) を用意
    → 対応する出力ごとに XOR をとった「マイター回路(miter)」を作る
    → マイター回路の出力が恒に 0 であることを SAT/BDD で証明
    → 1つでも 1 になる入力があれば、それが「等価でない反例」

LECは入力ベクトルを必要としない点で、機能の正しさを見ない/semiconductor/static-timing-analysis/（STA）と発想が似ています。STAがタイミングを全パス網羅で保証するのに対し、LECは論理の等価性を全入力網羅で保証する――どちらもシミュレーション不要の形式的サインオフです。

形式プロパティ検証（FPV）── 性質を証明し、反例を自動で出す

LECは「2つの回路が同じか」を問いますが、回路が満たすべき性質を直接証明したい場面も多くあります。たとえば「FIFOがオーバーフローしない」「2つのマスタが同時にバスを掴まない（相互排他）」といった性質です。これを担うのが 形式プロパティ検証（FPV, Formal Property Verification） で、中核技術はモデル検査（Model Checking） です。

設計者は性質をSVA（SystemVerilog Assertions）などでアサーションとして記述します。証明したい性質はsafety（安全性）とliveness（活性）の2種類に大別され、これに入力へ課す前提を表すassume（仮定）が加わります。

モデル検査は、有限状態機械の到達可能な全状態を探索し、アサーションを破る状態が到達可能かどうかを判定します。破る状態に到達できなければ「性質は全状態で成立する（証明）」、到達できればその状態へ至る入力系列＝反例（counterexample）を自動生成します。この反例は波形として再生でき、デバッグの出発点になります。

モデル検査の判定:

  到達可能状態の全集合を計算（BDD法や、BMC=有界モデル検査でSATを反復）
    → アサーション違反状態が到達可能集合に含まれるか？
        含まれない → 証明完了（proof）。深さ無制限で安全を保証
        含まれる   → 反例トレースを出力。設計バグ or 仮定不足

制約付きランダム検証とUVM ── 広く叩いて、覆えた範囲を測る

形式手法は強力ですが、CPUコア全体のように巨大なブロックでは状態爆発で手に負えません。そこで主力になるのがシミュレーションベースの制約付きランダム検証で、その業界標準方法論が UVM（Universal Verification Methodology） です。UVMはSystemVerilogのクラスライブラリとして提供され、再利用可能な検証環境（テストベンチ）の構造を標準化します。

UVMの発想は、人手で書いた個別テストではなく、制約付きランダム（constrained-random）な刺激を大量に生成して設計を広く叩くことです。完全な乱数ではなく、「アドレスは有効範囲内」「バースト長は1から16」のような制約を満たす範囲でランダム化し、人間が思いつかないコーナーケースを機械的に踏ませます。

UVMテストベンチの主要コンポーネント:

  sequencer → driver : 制約付きランダムなトランザクションを生成しDUTへ印加
  monitor            : DUTの入出力を観測しトランザクションへ復元
  scoreboard         : 期待値モデルと実応答を突き合わせ正否を判定
  coverage collector : 何が検証できたかを機能カバレッジとして集計
  (DUT = Design Under Test、検証対象設計)

ここで決定的なのが スコアボードと機能カバレッジです。ランダムに叩くだけでは、合格しても「たまたまバグを踏まなかった」のか「本当に正しい」のか区別できません。スコアボードが独立に計算した期待値と照合して正否を判定し、機能カバレッジが意図したシナリオを実際に踏めたかを定量化します。

カバレッジ駆動検証 ── 「いつ検証を止めてよいか」への答え

制約付きランダム検証の運用思想が カバレッジ駆動検証（CDV, Coverage-Driven Verification） です。検証の終了条件を「テストを書き切ったら」ではなく、機能カバレッジが目標（典型的には100%近く）に収束したらと定義します。

カバレッジ駆動のループ:

  カバレッジ目標(検証計画)を定義
    → ランダムシードを変えて回帰(regression)を大量実行
    → カバレッジを集計し、未到達(カバレッジホール)を特定
    → 制約を調整 / 専用テスト追加で穴を埋める
    → 目標に収束したら検証完了。バグ発見率の頭打ちも判断材料

この「未到達の穴を見つけて制約で狙い撃つ」ループにより、人間の直感に頼らず網羅度を測りながら検証を進められます。検証対象の規模は/semiconductor/process-variation-corners/のプロセスコーナーのような物理ばらつきとは別軸で、あくまで論理・機能の網羅を扱う点に注意してください。

実務では3手法を役割分担します。バスプロトコルやアービタのような制御集約ブロックはFPVで証明し、データパスを含む大規模ブロックはUVMで叩き、合成・最適化の各段はLECで等価性を担保する――この組み合わせで、シミュレーション単独では到達できない網羅性をテープアウト前に作り込みます。

まとめ

• 設計検証は製造前に機能の正しさを保証する独立工程で、状態空間の爆発のためシミュレーション単独では網羅できない。形式手法と制約付きランダム検証を組み合わせて網羅性を作る。
• LEC（論理等価性検証） は合成・最適化の前後で全入力一致をSAT/BDDで証明し、カットポイントで順序回路を組合せ回路の等価性へ分解する。
• FPV（形式プロパティ検証） はアサーションをモデル検査で全状態証明し、破れれば反例トレースを自動生成する。状態爆発で「証明不能」に終わることがある点が落とし穴。
• UVM は制約付きランダム刺激で広く叩き、スコアボードで正否を、機能カバレッジで網羅度を測る。コードカバレッジと機能カバレッジは別物で補完関係。
• カバレッジ駆動検証は機能カバレッジの収束を終了条件とし、未到達の穴を制約で狙い撃つ。制御集約はFPV、大規模はUVM、変換段はLECと役割分担するのが定石。