And-inverter graph とは

インバータグラフ(AIG)は、回路またはネットワークの論理機能の構造的な実装を表す有向非循環グラフです。 AIGは、論理結合を表す2入力ノードと、変数名でラベル付けされた端末ノードと、論理否定を示すマーカを任意に含むエッジとからなる。論理関数のこの表現は、大規模な回路では構造的に効率的であることはめったにありませんが、ブール関数の操作のための効率的な表現です。通常、抽象的なグラフは、ソフトウェアのデータ構造として表されます。
論理ゲートのネットワークからAIGへの変換は高速かつスケーラブルです。すべてのゲートをANDゲートとインバータで表現することだけが必要です。この変換によって、メモリ使用量と実行時間が予期せず増加することはありません。これにより、バイナリ決定図(BDD)または積和(ΣoΠ)形式、すなわち論理和形式(DNF)として知られているブール代数の正規形式と比較して、AIGが効率的に表現されます。 。 BDDとDNFは回線と見なすこともできますが、スケーラビリティを奪う正式な制約があります。たとえば、ΣoΠsは最大で2つのレベルの回路ですが、BDDは標準的です。つまり、入力変数をすべてのパスで同じ順序で評価する必要があります。
AIGを含む単純なゲートで構成される回路は、「古代」の研究課題です。 AIGの関心は、Alan Turingの1948年のニューラルネットワークに関する論文から始まりました。この論文では、無作為化された訓練可能なNANDゲートネットワークを記述しました。利子は1950年代後半まで続いており、1970年代にはさまざまな地域の変革が進んだ。これらの変換は、Darringer et al。のようないくつかの論理合成と検証システムで実装されました。および合成中の面積および遅延を改善するための回路を削減する、または正式な等価性検査を高速化するSmith等が挙げられる。構造ハッシュと呼ばれる複数の入力論理式と部分式を結合して再利用するなど、IBMの早い段階でいくつかの重要な技術が発見されました。
最近、合成および検証における様々なタスクの機能的表現として、AIGに新たな関心が寄せられています。これは、1990年代に人気のある表現(BDDなど)が、多くのアプリケーションでスケーラビリティの限界に達していたためです。もう一つの重要な発展は最近のはるかに効率的なブール充足可能性(SAT)ソルバの出現です。 AIGを回路表現として結合すると、さまざまな論理的な問題を解決する際の速度が飛躍的に向上します。
AIGは、多様なEDAアプリケーションでの使用が成功していることを発見しました。 AIGとブールの充足可能性のうまく調整された組み合わせは、モデル検査と等価性検査の両方を含む形式検証に影響を与えました。最近の別の研究は、AIGを使用して効率的な回路圧縮技術を開発できることを示しています。論理と物理的合成の問題は、シミュレーションやブールの充足可能性を使って解決でき、機能特性(対称性など)やノードの柔軟性(ドントケア・ターム、再置換、SPFDなど)を計算することができます。 Mishchenko et al。 AIGは、論理合成、技術マッピング、物理合成、および正式な検証を橋渡しすることができる、有望な統合表現であることを示しています。これは、AIGの単純で均一な構造のために、大規模なものであり、書き換え、シミュレーション、マッピング、配置、および検証が同じデータ構造を共有することを可能にする。
組合せ論理に加えて、AIGは順次論理および順次変換にも適用されています。具体的には、構造ハッシュ法は、メモリ要素(一般に未知である初期状態のD型フリップフロップなど)を備えたAIGに対して機能するように拡張され、アプリケーションに特化したデータ構造となったリタイミングに関連する。
進行中の研究には、AIGに完全に基づいた最新の論理合成システムを実装することが含まれます。 ABCと呼ばれるプロトタイプは、AIGパッケージ、いくつかのAIGベースの合成および等価性検査技術、ならびに順次合成の実験的な実装を特徴とする。 1つのそのような技術は、単一の最適化ステップにおいて、技術マッピングとリタイミングを組み合わせる。これらの最適化は、任意のゲートで構成されたネットワークを使用して実装できますが、AIGを使用することにより、スケーラビリティと実装が容易になります。