Grafo AND-inversor

Um grafo AND-inversor (GAI) (ou AIG, em inglês) é um grafo acíclico direcionado que representa uma implementação estrutural de um circuito ou rede. Um GAI consiste de vértices de duas entradas representando conjunções lógicas, vértices terminais contendo nomes de variáveis e possivelmente arestas contendo marcadores indicando negação lógica. Essa representação de uma função lógica não é estruturalmente eficiente para circuitos grandes, mas o é para manipulações de funções booleanas. Tipicamente, o grafo é representado como uma estrutura de dados.

Dois GAIs estruturalmente diferentes para a mesma função ternária f(x1, x2, x3) = x2 * ( x1 + x3 )

A conversão da rede de portas lógicas para GAIs é rápida e adaptável, e não leva a aumento imprevisível no uso de memória e tempo de execução, ela apenas requer que cada porta seja expressa em termos de portas AND e inversores. Isso faz do GAI uma eficiente representação em comparação com o diagrama de decisão binária (BDD) ou a "soma-de-produtos" (ΣoΠ),^{[carece de fontes]} isto é, a forma canônica na álgebra Booleana conhecida como forma normal disjuntiva (DNF). O BDD e a DNF podem também ser vistos como circuitos, mas eles envolvem restrições formais que priva-os de escalabilidade. Por exemplo, ΣoΠs são circuitos com no máximo dois níveis, enquanto BDDs são canônicos, isto é, eles exigem que as variáveis de entrada sejam avaliadas na mesma ordem em todos os caminhos.

Circuitos compostos de portas simples, incluindo GAIs, são um "antigo" tema de pesquisa. O interesse em GAIs começou no final da década de 1950 e continuou na década de 1970, quando várias transformações locais foram desenvolvidas. Essas transformações foram implementadas em diversos sistemas de síntese e de verificação lógica, tais como Darringer et al. e Smith et al., que otimizam circuitos para melhorar a área e o atraso durante a síntese, ou para acelerar a verificação formal de equivalência. Várias técnicas foram descobertas cedo, na IBM, tal como a combinação e a reutilização de multi-entrada de expressões lógicas e uma subexpressão, agora conhecida como hashing estrutural.

Recentemente, tem havido um interesse renovado em GAIs como uma representação funcional para uma variedade de tarefas de síntese e verificação. Isso porque as representações comuns na década de 1990 (como BDDs) atingiram os seus limites de escalabilidade em muitas de suas aplicações.^{[carece de fontes]} Outro desenvolvimento importante foi o surgimento recente de solucionadores do problema da satisfatibilidade (SAT) muito mais eficientes. Quando unidos com GAIs como o circuito de representação, eles levam a notáveis aumentos de velocidade na resolução de uma grande variedade de problemas booleanos.^{[carece de fontes]}

GAIs têm encontrado utilização bem sucedida em diversas aplicações EDA. Uma combinação otimizada de GAIs e satisfatibilidade causou um grande impacto na verificação formal, incluindo tanto o modelo de verificação de modelo (model checking) quanto o de verificação de equivalência. Outro trabalho recente mostra que técnicas eficientes de compressão de circuito podem ser desenvolvidas usando GAIs. Há uma crescente compreensão de que problemas de síntese lógicos e físicos podem ser resolvidos através do uso de simulação e da satisfatibilidade para calcular propriedades funcionais (tais como simetrias) e o flexibilidades (como o os termos don't care, resubstituições, e SPFDs). Mishchenko et al. mostra que GAIs são representações de unificação promissora, que pode abranger síntese lógica, a tecnologia de mapeamento, síntese física e verificação formal. Este é, em grande medida, pela simples e uniforme estrutura de GAIs, que permitem a reconfiguração, simulação, mapeamento, posicionamento e verificação para compartilhar a mesma estrutura de dados.

Além da lógica combinacional, GAIs têm sido aplicadas em lógica sequencial e transformações sequenciais. Especificamente, o método estrutural hash foi ampliado para trabalhar para GAIs com registradores (tais como flip-flops tipo D com um estado inicial, que, em geral, podem ser desconhecidos), resultando em uma estrutura de dados que é adaptada especificamente para aplicações relacionadas com a ressincronização.

A investigação em curso inclui a implementação de um moderno sistema de síntese lógica totalmente baseado em GAIs. O protótipo chamado ABC apresenta um pacote GAI, várias estruturas de síntese baseadas em GAIs e técnicas de verificação de equivalência lógica, bem como uma implementação experimental de síntese sequencial. Uma dessas técnicas combina a tecnologia de mapeamento e ressincronização em uma única etapa de otimização. Essas otimizações podem ser implementadas através de redes compostas de portas lógicas quaisquer, mas o uso de GAIs torna mais escalável e mais fácil de implementar.

Implementações

• Lógica de Síntese e Verificação do Sistema ABC
• Um conjunto de utilitários para AIGs AIGER
• OpenAccess Gear

Veja também

• Diagrama de decisão binária
• A conjunção lógica