About Aardvark

Aardvark is a mutual vacuity detection tool for LTL properties. Given a model and a property, the tool detects a maximal number of atomic formulae that can be replaced by TRUE/FALSE without changing the model checking outcome. Input Model Format: Verilog, Blif-MV Input Property Format: LTL Supported Platform: Linux X-86

Documentation

• Installation:

  Please download Aardvark and VIS executables provided on this page. Aardvark uses the model checker VIS. We made a few modifications to the VIS source code to serve our purpose. You must download the VIS executable available on the Aardvark page. If the models are described in Verilog, you also need to download and install the tool vl2mv from the VIS home-page.

  Before you can use Aardvark, set the PATH variable to include the path where you have downloaded VIS and Aardvark, and if needed, installed vl2mv.

• How to Use Aardvark:

  The following is the command to run Aardvark:

  aardvark -m model_file_name -p property_file_name -s use_binary -c use_ce.

  If use_binary = 1, Aardvark uses binary search to detect mutual vacuity. Otherwise, Aardvark uses exhaustive search. Likewise, use_ce can be used to enable or disable the use of counterexamples.

The following paper includes a detailed description of the various algorithms used in Aardvark:

• Strengthening Properties using Abstraction refinement.

Contact

• Mitra Purandare: E-mail: mitra.purandare[at]inf.ethz.ch