tip

================================================================================ Overview

Tip is a SAT based model checker. The name stands for "Temporal Induction Prover" as it mainly uses inductive model checking techniques. Circuits and properties are parsed via the AIGER file format and Tip supports all current AIGER features (safety properties, liveness properties, constraints, multiple properties, etc).

================================================================================ Quick Install

• Install MiniSat and Mini Circuit Library. Below the location of MiniSat headers and library files is referred to as $MINC and $MLIB respectively, and similarly the header and library locations for MCL is referred to as $MCLINC and $MCLLIB. If installed in a system-wide default location these locations are not necessary to specify by the user, and the configuration step becomes simpler.

• Configure the library dependencies:

  [ the exact details here may be simplified in the future ]

  make config MINISAT_INCLUDE=-I$MINC make config MINISAT_LIB="-L$MLIB -lminisat" make config MCL_INCLUDE=-I$MCLINC make config MCL_LIB="-L$MCLINC -lmcl"

• Decide where to install the files . The simplest approach is to use GNU standard locations and just set a "prefix" for the root install directory (reffered to as $PREFIX below). More control can be achieved by overriding other of the GNU standard install locations (includedir, bindir, etc). Configuring with just a prefix:

  make config prefix=$PREFIX

• Compiling and installing:

  make install

================================================================================ Configuration

• Multiple configuration steps can be joined into one call to "make config" by appending multiple variable assignments on the same line.

• The configuration is stored in the file "config.mk". Look here if you want to know what the current configuration looks like.

• To reset from defaults simply remove the "config.mk" file or call "make distclean".

• Recompilation can be done without the configuration step.

  [ TODO: describe configartion possibilities for compile flags / modes ]

================================================================================ Building

[ TODO: describe seperate build modes ]

================================================================================ Install

[ TODO: ? ]