Skip to content

niklasso/tip

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

================================================================================
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: ? ]

About

A model checker based on SAT solving and induction

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published