Comparador AIG

Implementação de dois comparadores de AAG para verificar equivalência lógica.

A aplicação converte o arquivo AAG para uma estrutura AIG e depois converte para uso em um dos comparadores disponíveis.

Comparador desenvolvido para a disciplina INF01205 CAD para Sistemas Digitais.

Building

Make

Compila todos os módulos individuais, seguido pela aplicação principal.

Make aag

Compila o leitor de AAG para AIG.

Make (bdd || bdd-file || sat)

Compila o módulo do comparador escolhido (BDD ou SAT). O comparador BDD possuí duas versões: bdd e bdd-file. O primeiro recebe as duas expressões por argumentas, pela linha de comando. O segundo recebe as expressões por um arquivo, informado no primeiro argumento. Esse arquivo contém cada expressão separada por linha. Exemplo:

expressao1
expressao2

Make util

Compila o módulo com utilitários utilizados por outros módulos.

Make test

Efetua testes sobre cada um dos módulos, sendo que no documento todos testes estão definidos separadamente, permitindo apenas testes de cada módulo, individualmente.

Make clean

Remove arquivos temporários gerados.

Using

./dst/comparador examples/aag/C17.aag examples/aag/C17-v1.aag --bdd
./dst/comparador examples/aag/C17.aag examples/aag/C17-v1.aag --sat

Arquivo de entrada AAG

• 11 nodos
• 5 entradas
• 0 FFs
• 2 saidas
• 6 ANDs

Para efeitos do parsing, são lidos o arquivo na seguinte ordem:

• nodos de entradas
• nodos de saída
• nodos AND

No caso do exemplo abaixo, as entradas são 2, 4, 6, 8 e 10. As saidas são 19 e 23 (que são os nodos 18 e 22 negados, respectivamente). Em seguida, estão os 6 ANDs: nodo 12 é nodo 6 && nodo 2, 14 é 8 && 6 e assim em diante.

aag 11 5 0 2 6
2
4
6
8
10
19
23
12 6 2
14 8 6
16 15 4
18 17 13
20 15 10
22 21 17

Comparando utilizando BDDs

Para o comparador utilizando BDD, o AIG dos dois arquivos de entrada é convertido em duas expressões lógicas, salvas em um arquivo e lido pelo comparador bdd-cmp.

Comparando utilizando SAT

Para o comparador utilizando SAT, o mesmo processo de conversão para AIG dos dois arquivos de entrada é efetuada, mas a estrutura é convertida para o formato CNF e avaliada por um programa externo, o Limboole. Esse programa recebe as expressões e avalia a sua satisfiability.

Versioning

We use SemVer for versioning. For the versions available, see the tags on this repository.

Contributing

Please read CONTRIBUTING.md for details on our code of conduct, and the process for submitting pull requests to us.

Authors

Contributors	Contributions
Francisco Knebel	Contributions by FranciscoKnebel
Luciano Zancan	Contributions by lzancan
Rodrigo Dal Ri	Contributions by rodrigodalri

See also the full list of contributors who participated in this project.

License

This project is licensed under the Apache License 2.0 - see the LICENSE.md file for details.