中国科学院研究員蔡少偉：SATソルバーEDA基本エンジン

[[441194]]

この記事はLeiphone.comから転載したものです。転載する場合は、Leiphone.com公式サイトにアクセスして許可を申請してください。

2021年12月9日から12月11日まで、2021年第6回世界人工知能会議（GAIR 2021）が深センで正式に開催されました。 5年を経て、いくつかの潮流の変化を目の当たりにし、現在までに広東・香港・マカオ大湾区の人工知能分野における学術、産業、投資の各分野における最大かつ最高レベルの国境を越えたイベントとなった。

会議2日目に開催された「集積回路サミットフォーラム：国産ハイエンドチップへの道」では、学界、産業界、投資界の著名人15名が一堂に会し、国産ハイエンドチップの強みやRISC-Vが中国製チップにもたらすチャンスについて議論した。

EDAは中国のチップ産業の発展にとってボトルネック技術であり、ソルバーはEDAの基本的なエンジンです。基本的な技術課題を解決することによってのみ、業界全体の急速な発展を支えることができます。これを踏まえて、中国科学院ソフトウェア研究所の研究員である蔡少偉氏は、主に自身の研究の観点からEDAの発展について語りました。

Cai Shaowei 氏の講演は主に 3 つの側面を取り上げました。1 つ目は、EDA と SAT ソルバーの関係、2 つ目は、EDA における SAT ソルバーの応用例、3 つ目は、彼のチームの SAT ソルバーの進捗状況の共有です。

Cai Shaowei 氏は、EDA 集積回路設計自動化ソフトウェアは単なる単一のソフトウェアではなく、非常に長いチェーンであると述べました。 EDA ソフトウェアでは、最下層にいくつかの計算エンジンが必要であり、主な計算エンジンは SAT ソルバーです。

SAT ソルバーは、論理合成、物理実装、中間検証、シミュレーション テストなど、EDA のあらゆる段階で使用されます。

現在、蔡少偉氏のチームの SAT ソルバーは集積回路の検証の実際のシナリオで使用されており、約 2 億個の節規模の例を 1 時間以内に解決できます。

以下はGAIR 2021における蔡少偉氏のスピーチの内容です。Leifeng.com（公式アカウント：Leifeng.com）が原文の意味を変えずに編集してまとめました。

本日のレポートは 3 つの部分に分かれています。1 つ目は EDA と SAT ソルバーの関係、2 つ目は EDA における SAT ソルバーの応用を示すためにいくつかの例を挙げること、3 つ目は SAT ソルバーにおけるチームの進捗状況を紹介することです。

EDA の正式名称は Electronic Design Automation で、集積回路の設計自動化ソフトウェアを指します。このようなソフトウェアを使用して集積回路を自動的に設計することを一般に EDA (チップの母) と呼びます。これは半導体業界全体の上流であり、チップ、さらには情報産業全体を支える共通の基礎技術です。

EDA 集積回路設計自動化ソフトウェアは単一のソフトウェアではなく、全体のチェーンは非常に長いです。EDA ソフトウェアをハードウェア コンパイラと見なし、チップ要件をハードウェア記述言語で記述することができます。EDA ソフトウェアは、チップ集積回路のレイアウトを自動的に設計するのに役立ちます。

EDA ソフトウェアでは、最下層にいくつかのコンピューティング エンジンが必要であり、主なコンピューティング エンジンは SAT ソルバーです。SA​​T ソルバーは、論理合成、物理実装、中間検証、シミュレーション テストなど、EDA のあらゆるリンクで実際に使用されます。

たとえば、論理合成を例にとると、SAT ソルバーは論理合成の歴史において常に非常に重要な役割を果たしてきました。特に、最適化と表現が SAT ソルバーに大きく依存する論理合成の開発の最終段階では重要な役割を果たしてきました。

回路の形式検証に関しては、モデル検査ツールと等価性検証ツールという 2 つの主な種類の形式検証ツールがあります。モデル検査は主に回路が特定の特性を満たしているかどうかを証明するために使用されますが、等価性検証は 2 つの回路が同等であるかどうかを証明するために使用されます。

モデル検査技術の発展を例にとると、この歴史的発展段階において、2000 年以降のモデル検査技術は基本的に SAT ソルバーをベースに開発されました。

一般的に、コンピュータが問題を解決するときには 2 つの考え方があります。1 つは、問題を数学的な言語で明確に記述し、それを解決するためのアルゴリズムを設計することです。これが制約解決の考え方です。典型的なシナリオには、定理の証明などがあります。 2 つ目は機械学習で、ユーザーが例を提供し、コンピューターが問題を解決します。たとえば、さまざまなパターン認識タスクは機械学習に適しています。厳密な証明が必要なシナリオでは、制約の解決が必要です。

SAT の正式名称はブール充足可能性問題です。この問題の説明は非常に単純で、ブール式または命題論理式、つまり AND や NOT などの論理接続子で接続された式が与えられた場合、式内の変数に値を割り当てて式を真にできるかどうかを判断します。そのような割り当てが存在する場合、式は満足可能であると言われ、そうでない場合は満足不可能であると言われます。

SAT に含まれる基本概念には、変数、リテラル、節 (節はリテラルの論理和)、連言標準形 (略して CNF、節の論理積、つまり節のセット) などがあります。 SAT は一般に連言正規形入力を使用して解決されますが、回路に対する SAT 問題もあります。

EDA における SAT の一般的な応用に関しては、SAT を使用して回路内の問題を解決するには、まず回路を SAT が受け入れ可能な入力形式に変換する必要があります。その中で、回路を CNF に変換する方法は、比較的単純なエンコード方式で、時間とスケールが線形であり、比較的便利です。

表の左側には回路の論理ゲートがあり、右側には対応する SAT 式があります。このようにして、回路は連言形式に変換され、SAT の入力形式になります。

今理解した回路は SAT 式に変換できます。では、ほとんどの EDA シナリオで SAT ソルバーをどのように使用できるでしょうか?いくつか例を挙げてみましょう。

まずはモデル検査ツールについて見てみましょう。モデル検査ツールは、「レジスタは絶対に競合しない」など、回路が特定のプロパティを満たしているかどうかを検出するために使用されます。回路の動作を特徴付けるにはオートマトン モデルを使用する必要があり、検証されたプロパティは順次ロジックに関連する式を使用して表現されます。このモデルに属性を含めることができるかどうか、つまりこのモデルの属性が有効かどうかを証明することをモデル テストと呼びます。このタスクの中核では、SAT ソルバーを呼び出す必要があります。

これはカウンターの例です。ハードウェア記述ソース Verilog モジュールを取得し、最初のビットから 2 番目と 3 番目のビットにジャンプしてから再起動します。 Verilog モジュールをコンパイルして、レジスタ、ネットゲートの論理ゲート接続を含むネットリストを取得し、最終的にこのネットリストに対応する状態遷移モデル、つまりオートマトン モデルを取得します。

このモデルを取得したら、検証属性に対応する数式も取得する必要があります。境界モデル検査は、K ステップ (K は指定) 内にパスが存在するかどうかを確認します。前述のように、K ステップを完了した後に指定されたプロパティに違反するパスはありますか?そのため、プロパティを論理式に変換する必要があります。

私たちが気にするのは 2 種類の属性です。1 つは Safety 属性で、悪いことが決して起こらないことを意味します。これはグローバル時間項 Gp で表されます。ここで p は満たされるべき属性です。まず、式を書き出して自然言語で理解します。初期状態から特定の状態へのパスがあり、この状態によって p が真でなくなる場合、反例が見つかります。そのようなパスが存在しない場合は、Gp が k ステップ内で確実に有効であることを意味します。

もう 1 つは Liveness プロパティです。これは、最終的には良いことが起こることを意味し、Fp で表されます。同様に、その逆を考えます。この式が成り立たない場合、サイクルが続くパスが存在し、このパス上のどの状態でも p は成立しないため、このプロパティは満たされません。

これまで述べてきたことと組み合わせると、これを SAT 式に変換できます。この式が SAT ソルバーによって判定され、満足できる場合、反例が存在し、それに応じてこの反例を構築できることを意味します。式が満たされない場合、つまり反例がない場合、プロパティが満たされていることが検証されます。

形式検証の 2 番目のタイプは同等性検証です。 2 つの回路は、どの入力に対しても出力が同じであり、機能的に同等である場合に同等です。では、SAT を使ってこれをどのように行うのでしょうか?

まず、単一の出力を考え、2 つの回路 N1 と N2 の出力を XOR ゲートで接続します。XOR ゲートの出力が 1 になる入力セットが見つかった場合、2 つの回路 N1 と N2 の出力は異なる、つまり同等ではないことを意味します。そのような入力が見つからない場合は、それらは同等であることを意味します。

出力回路が複数ある場合も同様です。各対応する出力N1とN2の出力をXORし、最後にORゲートで接続します。最終ゲート出力を 1 にするということは、これらの出力のペアが等しくなく、等しくないことを意味します。

このプロセスは SAT ソルバーを使用して実行でき、ハイブリッド回路を構築すると、SAT の入力形式である CNF 式になります。この式の解、つまり反例を見つけることができれば、それらは同等ではないということになります。逆に、対応する式が満たされないことが証明できれば、2つの回路は等価であることを意味します。これが等価性検証の現在の技術です。

形式検証に加えて、回路構造の最適化、置換するサブ構造の検索、置換が正しいことを確認しながら 2 つの構造を置換できるかどうかを照会する SAT の実行など、論理合成における多くの用途があります。

回路テストでは、設計プロセスは比較的正確ですが、実際にはチップの製造と設計は必ずしも一致していません。製造プロセスには、不純物汚染によって特定の経路または回路で短絡または断線が発生するなど、いくつかの不確実性があり、チップが元の設計と異なるものになります。回路テストで必要なのは、欠陥モデルを可能な限りカバーし、同様のエラーが発生しないようにすることです。私たちが行う必要があるのは、テストの欠陥をカバーする入力ベクトルのセットを生成することです。

一般的な欠陥はスタックアット障害と呼ばれ、経路が短絡しているか壊れているかに重点が置かれています。遅延欠陥モデルもあります。

知らないうちに回線が切れていたら、テストで見つけなければなりません。回線が切れた後の出力が回線が切れていないときと異なる場合にのみ、異常を発見できます。回路のスタック故障をテストする場合、カバーする欠陥の数は回路ラインの数の 2 倍になります。

たとえば、これは 3 桁の乗算と 2 桁の乗算で、対応する回路には 50 行あります。100 個の潜在的なスタック フォールトを検出するには、すべての可能な入力と実際の出力を、設計された回路の予想される出力と比較して、同じかどうかを確認するという非常に単純なアプローチがあります。異なる場合は、何らかのエラーが見つかります。 100% のカバレッジを達成できますが、効率が悪すぎるため、現時点では業界が同様の列挙を行うことは不可能です。

ATPG は SAT ソルバーを使用して、できるだけ少ない入力でできるだけ多くのエラーをカバーします。一般的に、最初のステップは、注意を払う必要があるエラーの大部分をカバーするために、いくつかの入力ベクトルをランダムに生成することです。残りのエラーはランダムにカバーするのが難しいため、対応する SAT ソルバーを使用して、対応するエラーをカバーできる入力ベクトルを見つけ、最後に圧縮して Bachmark を生成する必要があります。

図に示すように、線 d が破断して 0 になっているとします。開回路を検出するには、通常の設計での出力が反対側の出力と異なる入力を見つける必要があります。

したがって、2 つの条件を満たすテスト ベクトルを生成する必要があります。1 つはエラーのアクティブ化、もう 1 つはエラーが伝播される必要があることです。この 2 つの条件は CNF 式にエンコードされており、これは実際には SAT 解決問題です。

SAT ソルバーは EDA において非常に重要ですが、現在どのようになっているのでしょうか?

SAT は論理的な問題であり、還元原理などの論理的推論方法を使用して考えるのは簡単です。しかし、探索空間内で割り当てを見つけて、それが合法的な解決策を持つかどうかを判断するものと考えると、探索方法も実行可能です。

SAT の解決方法は、完全なアルゴリズムと不完全なアルゴリズムの 2 つのカテゴリに分けられます。完全なアルゴリズムとは、アルゴリズムに十分な時間が与えられれば、必ず正しい答え (はい、またはいいえ) が生成されることを意味しますが、この時間は理論的には保証されません。不完全なアルゴリズムは、可能な限り短い時間で解決策を見つけようとするアルゴリズムです。

SAT ソルバーは非常に重要です。多くの科学者が歴史を通じて研究してきました。完全なアルゴリズムは 1960 年から利用可能で、不完全なアルゴリズムは 1992 年から利用可能です。その中でも最も重要なのは、画期的な出来事となった1996年のCDCLでした。

歴史的には、1997 年にバート・セルマンが命題論理推論の 10 の課題を提案しました。その 7 番目は、命題論理推論を組み合わせてより強力な方法を生み出すことができるかどうかというものでした。これが私たちの最近の研究の方向性です。

これまでの方法は、システム検索とローカル検索に重点を置いていました。これら 2 つの方法の解決能力は補完的です。ユニオンを使用しても、実際には業界は改善されません。元の方法では問題を解決できず、ユニオン方法でも問題を解決できません。

最近、私たちは、サンプリングツールとして不完全なランダム探索法を使用して、完全探索に基づく問題を解決しています。サンプリングされた情報は、情報相互作用の深い協力に基づいて、完全なアルゴリズムが問題を解決するのに役立ちます。過去数年間の競争の産業例では、この方法で生成されたハイブリッドアルゴリズムは、元の2つのアルゴリズムが解決できないケースの12％を解決でき、産業例で大幅な改善を達成し、初めてこの課題に答えました。

同時に、この方法は実際のシナリオでの集積回路の検証にも直接使用され、1 時間で約 2 億個のサブセットを解決できます。

今年のEDAコンテストでは世界第2位を獲得しました。これは、優れたSATソルバーがEDAにとって非常に重要であることを示しています。関連する手法はSAT 2021に掲載され、最優秀論文賞を受賞しました。

概要: SAT ソルバーは、EDA の主要エンジンとして重要な役割を果たします。この点で重要な進歩は、ハイブリッド解決方法のブレークスルーです。皆様ありがとうございました。