Installation Guide » History » Revision 83

Revision 82 (Andrei Tatarnikov, 05/23/2015 09:21 AM) → Revision 83/95 (Andrei Tatarnikov, 05/23/2015 09:23 AM)

h1. Installation Guide


h3. System Requirements

MicroTESK is a set of Java-based utilities that are run from the command line. It can be used on *_Windows_*, *_Linux_* and *_OS X_* machines that have *_JDK 1.7 or later_* installed. To build MicroTESK from source code or to build generated Java models, *_Apache Ant version 1.8_ or later* is required. To generate test data based on constraints, MicroTESK needs *_Microsoft Research Z3_* that can work under the corresponding operating system.

h3. Installation Steps

# Download from and unpack the MicroTESK installation package (the @.tar.gz@ file, latest release) to your computer. The folder to which it was unpacked will be further referred to as the installation directory (@<installation dir>@).
# [Not required for MicroTESK 2.1 beta] Download and install constraint solver tools to the @<installation dir>/tools@ directory (see the *Installing Constraint Solvers* section).
# Declare the *MICROTESK_HOME* environment variable and set its value to the path to the installation directory (see the *Setting Environment Variables* section).
# Set the @<installation dir>/bin@ as the working directory (add the path to the @PATH@ environment variable) to be able to run MicroTESK utilities from any path.
# Now you can run the (or @.bat@) script to create a microprocessor model and the (or @.bat@) script to generate test for this model.

h3. Setting Environment Variables

h4. _Windows_

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

h4. _Linux and OS X_

Add the command below to the @~.bash_profile@ file (Linux) or the @~/.profile@ file (OS X):
<pre>export MICROTESK_HOME=<installation dir></pre> To start editing the file, type @vi ~/.bash_profile@ (or @vi ~/.profile@). Changes will be applied after restarting the command-line terminal or reboot. You can also execute the command in your command-line terminal to make temporary changes.

h3. Installing Constraint Solvers

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

*_Installing Z3_*

* Windows users should download Z3 (32 or 64-bit version) from the following page: and unpack the archive to the @<installation dir>/tools/z3/windows@ directory. Note: the executable file path is @<windows>/z3/bin/z3.exe@.

* UNIX and Linux users should use one of the links below and and unpack the archive to the @<installation dir>/tools/z3/unix@ directory. Note: the executable file path is @<unix>/z3/bin/z3@.
| Debian x64 | |
| Ubuntu x86 | |
| Ubuntu x64 | |
| FreeBSD x64 | |

* OS X users should download Z3 from and unpack the archive to the @<installation dir>/z3/osx@ directory. Note: the executable file path is @<osx>/z3/bin/z3@.

*_Installing CVC4_*

* Windows users should download the latest version of CVC4 binary from and save it to the @<installation dir>/tools/cvc4/windows@ directory as @cvc4.exe@.

* Linux users download the latest version of CVC4 binary from (32-bit version) or (64-bit version) and save it to the @<installation dir>/tools/cvc4/unix@ directory as @cvc4@.

* OS X users should download the latest version of CVC4 distribution package from and install it.
The CVC4 binary should be copied to @<installation dir>/tools/cvc4/osx@ as @cvc4@ or linked to this file name via a symbolic link.

h3. Installation Directory Structure

The MicroTESK installation directory contains the following subdirectories:

| @arch@ | Examples of microprocessor specifications and test templates for the described designs |
| @bin@ | Scripts to run features of MicroTESK (modelling and test generation) |
| @doc@ | Documentation on MicroTESK |
| @etc@ | MicroTESK configuration files |
| @gen@ | Generated Java models of the specified microprocessor designs |
| @lib@ | JAR files and Ruby scripts to perform modelling and test generation tasks |
| @src@ | Source code of MicroTESK |

h3. Running MicroTESK

To generate a Java model of a microprocessor from its nML specification, a user needs to run the script (Unix, Linux, OS X) or the compile.bat script (Windows). For example, the following command generates a model for the miniMIPS specification:

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

_NOTE: Models for all demo specifications are already built and included in the MicroTESK distribution package. So a user can start working with MicroTESK from generating test programs for these models._

To generate a test program, a user needs to use the script (Unix, Linux, OS X) or the generate.bat script (Windows). The scripts require the following parameters:

# _model name_;
# _test template file_;
# _target test program source code file_.

For example, the following command runs the @euclid.rb@ test template for the miniMIPS model generated by the command from the previous example and saves the generated test program to the @test.asm@ file:

sh bin/ minimips arch/minimips/templates/euclid.rb test.asm

To specify whether "Z3": or "CVC4": should be used to solve constraints, a user needs to specify the @-s@ or @--solver@ command-line option as @z3@ or @cvc4@ respectively. By default, Z3 will be used. Here is an example:

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

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