yosys/examples/aiger

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.