| 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. |
