Installation Guide » History » Revision 49
Revision 48 (Andrei Tatarnikov, 03/23/2014 03:21 PM) → Revision 49/115 (Andrei Tatarnikov, 03/23/2014 03:57 PM)
h1. Installation Guide
_~By Andrei Tatarnikov~_
{{toc}}
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.6 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 http://forge.ispras.ru/projects/microtesk/files and unpack the MicroTESK installation package (the @.tar.gz@ file, latest release) to your computer.
# 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).
# Now you can run the @compile.sh@ (or @.bat@) script to create a microprocessor model and the @generate.sh@ (or @.bat@) script to generate test for this model.
h3. Setting Environment Variables
h4. _Windows_
TODO
h4. _Linux and OS X_ _Linux_
Add the command below to the @~.bash_profile@ @.bash_profile@ file (Linux) or (type @vi ~/.bash_profile@ to start editing the @~/.profile@ file (OS X): file):
<pre>export MICROTESK_HOME=<installation dir></pre> To start editing the file, type @vi ~/.bash_profile@ (or @vi ~/.profile@). Changes dir></pre>Changes will be applied after reboot. You can also execute the command in your command-line terminal to make temporary changes.
h4. _OS X_
TODO
h3. Installing Constraint Solvers
To generate test data based on constraints, MicroTESK requires external constraint solver engines. The current version uses the Z3 constraint solver by Microsoft Research (http://z3.codeplex.com/). The Z3 executable should be downloaded and placed to the @<installation dir>/tools@ directory.
* Windows users should download Z3 (32 or 64-bit version) from the following page: http://z3.codeplex.com/releases, unpack the archive and place the @z3.exe@ file to the @<installation dir>/tools/z3/windows@ directory.
* UNIX and Linux users should use one of the links below and place the @z3@ executable file to the @<installation dir>/tools/z3/unix/z3@ directory.
| Debian x64 | http://z3.codeplex.com/releases/view/101916 |
| Ubuntu x86 | http://z3.codeplex.com/releases/view/101913 |
| Ubuntu x64 | http://z3.codeplex.com/releases/view/101911 |
| FreeBSD x64 | http://z3.codeplex.com/releases/view/101907 |
* OS X users should download Z3 from http://z3.codeplex.com/releases/view/101918 and place the @z3@ executable file to the @<installation dir>/z3/osx/z3@ directory.
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 and nML/Sim-nML |
| @gen@ | Generated Java models of the specified microprocessor designs |
| @lib@ | JAR files and Ruby scripts to perform modelling and test generation tasks |
h3. Running MicroTESK
To generate a Java model of a microprocessor from its nML specification, a user needs to run the compile.sh script (Unix, Linux, OS X) or the compile.bat script (Windows). For example, the following command generates a model from a MIPS ISA specification:
<pre>
sh compile.sh ../arch/mips/model/mips.nml
</pre>
To generate a test program, a user needs to use the generate.sh script (Unix, Linux, OS X) or the generate.bat script (Windows). The scripts require the following parameters: (1) _model name_ , (2) _test template file_ and (3) _target test program source code file_. For example, the following command runs the @mips_demo.rb@ test template for the MIPS model generated by the command from the previous example and saves the generated test program to the @test.asm@ file:
<pre>
sh generate.sh mips ../arch/mips/templates/mips_demo.rb test.asm
</pre>