23 lines
970 B
Plaintext
23 lines
970 B
Plaintext
|
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.
|