Installation Guide » History » Version 24
Andrei Tatarnikov, 03/19/2014 05:59 PM
1 | 1 | Andrei Tatarnikov | h1. Installation Guide |
---|---|---|---|
2 | |||
3 | *UNDER CONSTRUCTION* |
||
4 | |||
5 | 22 | Andrei Tatarnikov | _~By Andrei Tatarnikov~_ |
6 | |||
7 | 17 | Andrei Tatarnikov | h3. System Requirements |
8 | 1 | Andrei Tatarnikov | |
9 | 9 | 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.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. |
10 | 1 | Andrei Tatarnikov | |
11 | 17 | Andrei Tatarnikov | h3. Installation Steps |
12 | 1 | Andrei Tatarnikov | |
13 | # Download and unpack the MicroTESK installation package (the .tar.gz file) to your computer. |
||
14 | 22 | Andrei Tatarnikov | # Download and install constraint solver tools to the "<installation folder>/tools" folder (see the "Installing Constraint Solver Tools" section). |
15 | # Open your console terminal and set the "<installation folder>/bin" as the working directory. |
||
16 | 13 | Andrei Tatarnikov | # 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. |
17 | |||
18 | 17 | Andrei Tatarnikov | h3. Installing Constraint Solver Tools |
19 | 15 | Andrei Tatarnikov | |
20 | 23 | Andrei Tatarnikov | 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 folder>/tools" folder. |
21 | 18 | Andrei Tatarnikov | |
22 | 22 | Andrei Tatarnikov | * 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 folder>/tools/z3/windows" folder. |
23 | 1 | Andrei Tatarnikov | |
24 | 24 | Andrei Tatarnikov | * UNIX and Linux users should use one of the links below and place the z3 executable file to the "<installation folder>/tools/z3/unix/z3" folder. |
25 | Debian x64: http://z3.codeplex.com/releases/view/101916 |
||
26 | Ubuntu x86: http://z3.codeplex.com/releases/view/101913 |
||
27 | Ubuntu x64: http://z3.codeplex.com/releases/view/101911 |
||
28 | FreeBSD x64: http://z3.codeplex.com/releases/view/101907 |
||
29 | 21 | Andrei Tatarnikov | |
30 | 23 | Andrei Tatarnikov | * OS X users should download Z3 from http://z3.codeplex.com/releases/view/101918 and place the z3 executable file to the "<installation folder>/z3/osx/z3" folder. |
31 | 15 | Andrei Tatarnikov | |
32 | 17 | Andrei Tatarnikov | h3. Installation Folder Structure |
33 | 13 | Andrei Tatarnikov | |
34 | The MicroTESK installation folder contains the following subfolders: |
||
35 | |||
36 | # _arch_ Examples of microprocessor specifications and test templates for the described designs. |
||
37 | # _bin_ Scripts to run features of MicroTESK (modelling and test generation). |
||
38 | 1 | Andrei Tatarnikov | # _doc_ Documentation on MicroTESK and nML/Sim-nML. |
39 | # _libs_ JAR files and Ruby scripts to perform modelling and test generation tasks. |
||
40 | 13 | Andrei Tatarnikov | # _output_ Generated Java models of the specified microprocessor designs. |
41 | 14 | Andrei Tatarnikov | |
42 | h3. Running MicroTESK |