Installation Guide

Home / Documentation / Installation Guide

System Requirements

Being developed in Java, MicroTESK can be used on Windows, Linux, OS X, and other systems with the following software installed:

  • JDK 1.7+;
  • Apache Ant 1.8+.

Installation Steps

  • Download the package (.tar.gz) and unpack it to some directory.
    This directory will be referred to as <installation dir>.
  • Install constraint solvers, if required, to <installation dir>/tools (see Installing Constraint Solvers).
  • Define the MICROTESK_HOME environment variable (see Setting Environment Variables).
  • Add <installation dir>/bin to the PATH environment variable.

Now you can run the following scripts:

compile.sh (compile.bat) Creates an ISA model from specifications
generate.sh (generate.bat) Processes a test templates and generates a test program

Setting Environment Variables

Windows

  • Open the System Properties window.
  • Switch to the Advanced tab.
  • Click Environment Variables.
  • Click New... under System Variables.
  • In the New System Variable dialog, type MICROTESK_HOME as a variable name and <installation dir> as its value.
  • Click OK on all open windows.
  • Reopen the command prompt window.

Linux and OS X

Add the command below to ~.bash_profile (Linux) or ~/.profile (OS X):

export MICROTESK_HOME=<installation dir>

To start editing the file, type vi ~/.bash_profile (Linux) or vi ~/.profile (OS X). Changes will be applied after restarting the terminal or reboot.

Installing Constraint Solvers

To generate test data based on constraints, MicroTESK requires external constraint solvers. The current version supports the Z3 and CVC4 solvers. Constraint solver executables should be downloaded and placed to <installation dir>/tools.

Installing Z3

  • Windows users should download Z3 from http://z3.codeplex.com/releases and unpack it to <installation dir>/tools/z3/windows. Note: the executable file path is <windows>/z3/bin/z3.exe.

Installing CVC4

  • OS X users should download the CVC4 distribution package from http://cvc4.cs.nyu.edu/builds/macos/ and install it. The CVC4 binary should be copied to <installation dir>/tools/cvc4/osx/cvc4 or linked to this path via a symbolic link.

Installation Directory Structure

The installation directory contains the following subdirectories:

arch Sample ISA specifications and test templates
bin Scripts for model compilation and test generation
doc Documentation
etc Configuration files
gen Compiled ISA models
lib Library JAR files and Ruby scripts
src Source code

Running MicroTESK

To generate an ISA model from its nML specification, one needs to run compile.sh (Linux or OS X) or compile.bat (Windows).

The command below generates a model for miniMIPS:

sh bin/compile.sh arch/minimips/model/minimips.nml

Note: sample ISA models are already built and included in the MicroTESK package. Thus, one can start working with MicroTESK from generating test programs for these models.

To generate a test program, one needs to run generate.sh (Linux or OS X) or generate.bat (Windows). The scripts require the following parameters:

  • model name;
  • test template file name.

The command below processes the euclid.rb test template for the miniMIPS model and generates a test program. The output file name is based on the --code-file-prefix and --code-file-extension options.

sh bin/generate.sh minimips arch/minimips/templates/euclid.rb

To specify whether Z3 or CVC4 should be used to solve constraints, one needs to specify the -s or --solver option as z3 or cvc4 respectively. By default, Z3 is used.

Here is an example:

sh bin/generate.sh -s cvc4 minimips arch/minimips/templates/constraint.rb

More information on the command-line options can be found on the Command-Line Options page.