| AIGER is a format for And-Inverter Graphs (AIGs). | |
| See http://fmv.jku.at/aiger/ for details. | |
| AIGER is used in the Hardware Model Checking Competition (HWMCC), | |
| therefore all solvers competing in the competition have to support | |
| the format. | |
| The example in this directory is using super_prove as solver. Check | |
| http://downloads.bvsrc.org/super_prove/ for the lates release. (See | |
| https://bitbucket.org/sterin/super_prove_build for sources.) | |
| The "demo.sh" script in this directory expects a "super_prove" executable | |
| in the PATH. E.g. extract the release to /usr/local/libexec/super_prove | |
| and then create a /usr/local/bin/super_prove file with the following | |
| contents (and "chmod +x" that file): | |
| #!/bin/bash | |
| exec /usr/local/libexec/super_prove/bin/super_prove.sh "$@" | |
| The "demo.sh" script also expects the "z3" SMT2 solver in the PATH for | |
| converting the witness file generated by super_prove to VCD using | |
| yosys-smtbmc. See https://github.com/Z3Prover/z3 for install notes. |