Project

General

Profile

Installation Guide » History » Revision 63

Revision 62 (Andrei Tatarnikov, 03/05/2015 03:22 PM) → Revision 63/115 (Andrei Tatarnikov, 03/05/2015 03:22 PM)

h1. Installation Guide 

 {{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.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 http://forge.ispras.ru/projects/microtesk/files and unpack the MicroTESK installation package (the @.tar.gz@ file, latest release) to your computer. 
 # [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 @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_ 

 # 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@ MICROTESK_HOME and variable value as @<installation dir>@. <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 

 _NOTE: Not required for MicroTESK 2.1 beta._ 

 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 | 
 | @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 for the VLIW demo specification: 

 <pre> 
 sh bin/compile.sh arch/demo/vliw/model/vliw.nml 
 </pre> 

 _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 generate.sh 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: 

 <pre> 
 sh bin/generate.sh vliw arch/demo/vliw/templates/euclid.rb test.asm 
 </pre>