Installation Guide » History » Version 65

Andrei Tatarnikov, 03/24/2015 02:05 PM

1 1 Andrei Tatarnikov
h1. Installation Guide
3 36 Alexander Kamkin
5 17 Andrei Tatarnikov
h3. System Requirements
6 1 Andrei Tatarnikov
7 52 Andrei Tatarnikov
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.
8 1 Andrei Tatarnikov
9 17 Andrei Tatarnikov
h3. Installation Steps
10 1 Andrei Tatarnikov
11 64 Andrei Tatarnikov
# 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>@).
12 53 Andrei Tatarnikov
# [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).
13 46 Andrei Tatarnikov
# Declare the *MICROTESK_HOME* environment variable and set its value to the path to the installation directory (see the *Setting Environment Variables* section).
14 60 Andrei Tatarnikov
# 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.
15 33 Alexander Kamkin
# Now you can run the (or @.bat@) script to create a microprocessor model and the (or @.bat@) script to generate test for this model.
16 13 Andrei Tatarnikov
17 47 Andrei Tatarnikov
h3. Setting Environment Variables
19 48 Andrei Tatarnikov
h4. _Windows_
20 47 Andrei Tatarnikov
21 50 Andrei Tatarnikov
# Open the "System Properties" window.
# Switch to the "Advanced" tab.
# Click on Environment Variables.
# Click "New.." under "System Variables".
25 63 Andrei Tatarnikov
# In the "New System Variable" dialog specify variable name as @MICROTESK_HOME@ and variable value as @<installation dir>@.
26 50 Andrei Tatarnikov
# Click "OK" on all open windows.
# Reopen the command prompt window.
29 49 Andrei Tatarnikov
h4. _Linux and OS X_
30 48 Andrei Tatarnikov
31 1 Andrei Tatarnikov
Add the command below to the @~.bash_profile@ file (Linux) or the @~/.profile@ file (OS X):
32 61 Andrei Tatarnikov
<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.
33 47 Andrei Tatarnikov
34 55 Andrei Tatarnikov
h3. Installing Constraint Solvers
_NOTE: Not required for MicroTESK 2.1 beta._
37 15 Andrei Tatarnikov
38 40 Alexander Kamkin
To generate test data based on constraints, MicroTESK requires external constraint solver engines. The current version uses the Z3 constraint solver by Microsoft Research ( The Z3 executable should be downloaded and placed to the @<installation dir>/tools@ directory.
39 18 Andrei Tatarnikov
40 40 Alexander Kamkin
* Windows users should download Z3 (32 or 64-bit version) from the following page:, unpack the archive and place the @z3.exe@ file to the @<installation dir>/tools/z3/windows@ directory.
41 1 Andrei Tatarnikov
42 65 Andrei Tatarnikov
* UNIX and Linux users should use one of the links below and place the @z3@ executable file to the @<installation dir>/tools/z3/unix@ directory.
43 34 Alexander Kamkin
| Debian  x64 | |
| Ubuntu  x86 | |
| Ubuntu  x64 | |
| FreeBSD x64 | |
47 21 Andrei Tatarnikov
48 65 Andrei Tatarnikov
* OS X users should download Z3 from and place the @z3@ executable file to the @<installation dir>/tools/z3/osx@ directory.
49 15 Andrei Tatarnikov
50 40 Alexander Kamkin
h3. Installation Directory Structure
51 13 Andrei Tatarnikov
52 40 Alexander Kamkin
The MicroTESK installation directory contains the following subdirectories:
53 13 Andrei Tatarnikov
54 33 Alexander Kamkin
| @arch@   | Examples of microprocessor specifications and test templates for the described designs |
| @bin@    | Scripts to run features of MicroTESK (modelling and test generation) |
56 56 Andrei Tatarnikov
| @doc@    | Documentation on MicroTESK |
57 43 Andrei Tatarnikov
| @gen@    | Generated Java models of the specified microprocessor designs |
| @lib@    | JAR files and Ruby scripts to perform modelling and test generation tasks |
59 14 Andrei Tatarnikov
h3. Running MicroTESK
61 26 Andrei Tatarnikov
62 58 Andrei Tatarnikov
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 VLIW demo specification:
63 1 Andrei Tatarnikov
64 26 Andrei Tatarnikov
65 57 Andrei Tatarnikov
sh bin/ arch/demo/vliw/model/vliw.nml
66 27 Andrei Tatarnikov
67 1 Andrei Tatarnikov
68 57 Andrei Tatarnikov
_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._
69 1 Andrei Tatarnikov
70 57 Andrei Tatarnikov
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 VLIW demo model generated by the command from the previous example and saves the generated test program to the @test.asm@ file:
78 27 Andrei Tatarnikov
79 57 Andrei Tatarnikov
sh bin/ vliw arch/demo/vliw/templates/euclid.rb test.asm
80 26 Andrei Tatarnikov