Installation Guide » History » Revision 96
Revision 95 (Andrei Tatarnikov, 09/26/2017 10:23 AM) → Revision 96/115 (Alexander Kamkin, 01/10/2020 01:50 PM)
h1. Installation Guide
{{toc}}
h2. h3. System Requirements
Being developed in Java, MicroTESK is a set of Java-based utilities that are run from the command line. It can be used on Windows, Linux, macOS, *_Windows_*, *_Linux_* and other platforms with the following software installed:
* JDK 11+ (https://openjdk.java.net);
* Apache *_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 1.8+ (https://ant.apache.org).
version 1.8_ or later* is required. To generate test data based on constraints (if required), constraints, MicroTESK needs an SMT solver such as Z3 *_Z3_* or CVC4 (see <<Installing SMT Solvers>>). *_CVC4_* that can work under the corresponding operating system.
h2. Installation
h3. Installation Steps
# Download from http://forge.ispras.ru/projects/microtesk/files and unpack a distribution the MicroTESK installation package (the @.tar.gz@ file, latest @.tar.gz@ file).
release) to your computer. The destination directory folder to which it was unpacked will be further referred to as @<INSTALL_DIR>@.
the installation directory (@<installation dir>@).
# Set Download and install constraint solver tools to the @MICROTESK_HOME@ @<installation dir>/tools@ directory (see the *Installing Constraint Solvers* section).
# Declare the *MICROTESK_HOME* environment variable and set its value to the @<INSTALL_DIR>@ path to the installation directory (see <<Setting the *Setting Environment Variables>>).
Variables* section).
# Add Set the @<INSTALL_DIR>/bin@ @<installation dir>/bin@ as the working directory (add the path to the @PATH@ environment variable.
variable) to be able to run MicroTESK utilities from any path.
# If required, install SMT solver(s) Now you can run the @compile.sh@ (or @.bat@) script to create a microprocessor model and the @<INSTALL_DIR>/tools@ directory (see <<Installing SMT Solvers>>). @generate.sh@ (or @.bat@) script to generate test for this model.
h4. h3. Setting Environment Variables
*Windows* h4. _Windows_
# Start Open the @Control Panel@ dialog. @System Properties@ window.
# Click on Switch to the following items: @Advanced@ tab.
## @System and Security@;
## @System@;
## @Advanced system settings@.
# Click on @Environment Variables@. Environment Variables.
# Click on @New...@ under @System Variables@.
# Specify @Variable name@ In the @New System Variable@ dialog specify variable name as @MICROTESK_HOME@ and @Variable value@ variable value as @<INSTALL_DIR>@. @<installation dir>@.
# Click @OK@ in on all open windows.
# Reopen the command prompt window.
*Linux h4. _Linux and macOS* OS X_
Add the command below to @~/.bash_profile@ the @~.bash_profile@ file (Linux) or the @~/.profile@ (macOS):
<pre> file (OS X):
export MICROTESK_HOME=<INSTALL_DIR>
</pre>
<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 terminal. 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":https://github.com/z3prover and "CVC4":http://cvc4.cs.nyu.edu constraint solvers. Constraint solver 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: http://z3.codeplex.com/releases 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 | 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 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 http://cvc4.cs.nyu.edu/builds/win32-opt/ and save it to the @<installation dir>/tools/cvc4/windows@ directory as @cvc4.exe@.
* Linux users download the latest version of CVC4 binary from http://cvc4.cs.nyu.edu/builds/i386-linux-opt/unstable/ (32-bit version) or http://cvc4.cs.nyu.edu/builds/x86_64-linux-opt/unstable/ (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 http://cvc4.cs.nyu.edu/builds/macos/ 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
@<INSTALL_DIR>@ The MicroTESK installation directory contains the following subdirectories:
table=.
{font-style:italic; font-weight:bold; background:#ddd}. |<. Directory |<. Description |
|<. @arch@ |<. Microprocessor | Examples of microprocessor specifications and test templates for the described designs |
|<. | @bin@ |<. | Scripts for model compilation to run features of MicroTESK (modelling and test generation generation) |
|<. | @doc@ |<. | Documentation on MicroTESK |
|<. | @etc@ |<. Configuration | MicroTESK configuration files |
|<. | @gen@ |<. | Generated code Java models of the specified microprocessor models designs |
|<. | @lib@ |<. | JAR files and Ruby scripts to perform modelling and test generation tasks |
|<. | @src@ |<. | Source code of MicroTESK |
|<. @tools@ |<. SMT solvers |
h3. Running MicroTESK
h4. Installing SMT Solvers
To generate test data based on constraints, MicroTESK uses external SMT solvers.
There are supported https://github.com/z3prover/[Z3] and https://github.com/CVC4/CVC4/[CVC4].
Solver executables should be placed to @<INSTALL_DIR>/tools@.
*Specifying paths*
If solvers are already installed, MicroTESK can find them by using the @Z3_PATH@ and @CVC4_PATH@ environment variables.
*NOTE:* Each @_PATH@ variable specifies the path to the corresponding executable.
*Installing Z3*
* Build Z3 as it is described in https://github.com/Z3Prover/z3.
* Move the executable file to the following path (or create a symbolic link):
- @<INSTALL_DIR>/tools/z3/windows/z3.exe@ (Windows);
- @<INSTALL_DIR>/tools/z3/unix/z3@ (Linux);
- @<INSTALL_DIR>/tools/z3/osx/z3@ (macOS).
*Installing CVC4*
* Build CVC4 as it is described in https://github.com/CVC4/CVC4/.
* Move the executable file to the following path (or create Java model of a symbolic link):
- @<INSTALL_DIR>/tools/cvc4/windows/cvc4.exe@ (Windows);
- @<INSTALL_DIR>/tools/cvc4/unix/cvc4@ (Linux);
- @<INSTALL_DIR>/tools/cvc4/osx/cvc4@ (macOS).
h2. Usage
h3. Model Compilation
To compile a microprocessor model from its nML specification, a user needs to run the following command:
* @sh compile.sh <SPECIFICATION>@ (Linux and macOS);
* @compile.bat <SPECIFICATION>@ @compile.sh@ script (Unix, Linux, OS X) or the @compile.bat@ script (Windows).
For example, the actions below compile the following command generates a model from for the miniMIPS specification:
<pre>
$ cd $MICROTESK_HOME
$ sh bin/compile.sh arch/minimips/model/minimips.nml arch/minimips/model/mmu/minimips.mmu arch/demo/minimips/model/minimips.nml
</pre>
*NOTE:* _NOTE: Models for all demo specifications are already built and included into in the MicroTESK distribution package. There is no need to compile them. So a user can start working with MicroTESK from generating test programs for these models._
h3. Test Program Generation
To generate a test program for program, a given architecture (model) and a given test template, run user needs to use the @generate.sh@ script (Unix, Linux, OS X) or the @generate.bat@ script (Windows). The scripts require the following command:
* @sh generate.sh <ARCH> <TEMPLATE>@ (Linux and macOS); parameters:
# _model name_;
* @generate.bat <ARCH> <TEMPLATE>@ (Windows). # _test template file_.
For example, the actions command below generate a runs the @euclid.rb@ test program template for the miniMIPS model compiled in generated by the command from the previous example and saves the @euclid.rb@ generated test template: program to an assembler file. The file name is based on values of the @--code-file-prefix@ and @--code-file-extension@ options.
<pre>
$ cd $MICROTESK_HOME
$ sh bin/generate.sh minimips arch/minimips/templates/euclid.rb arch/demo/minimips/templates/euclid.rb
</pre>
The output file name depends on the @--code-file-prefix@ and @--code-file-extension@ options (see <<Options>>).
To specify which SMT solver whether "Z3":https://github.com/z3prover or "CVC4":http://cvc4.cs.nyu.edu should be used to solve constraints (if required), constraints, a user needs to specify the @--solver <SOLVER>@ (or @-s <SOLVER>@) option, where @<SOLVER>@ is @-s@ or @--solver@ command-line option as @z3@ or @cvc4@ (by respectively. By default, Z3 will be used. Here is used): an example:
<pre>
$ cd $MICROTESK_HOME
$ sh bin/generate.sh -s cvc4 minimips arch/minimips/templates/constraint.rb arch/demo/minimips/templates/constraint.rb
</pre>
More information on command-line options can be found in <<Command-Line Options>>.
h2. Options
h3. Command-Line Options
MicroTESK works in two main modes:
* model compilation (@--translate@);
* test program generation (@--generate@).
*NOTE:* The @--translate@ and @--generate@ keys are inserted into on the command line by @compile.sh@ (or @compile.bat@) and @generate.sh@ (or @generate.bat@) correspondingly.
Other options should be specified explicitly.
h3. Settings File
Default values of options are stored in the @<INSTALL_DIR>/etc/settings.xml@ configuration file:
<pre>
<?xml version="1.0" encoding="utf-8"?>
<settings>
<setting name="random-seed" value="0"/>
<setting name="branch-exec-limit" value="1000"/>
<setting name="code-file-extension" value="asm"/>
<setting name="code-file-prefix" value="test"/>
<setting name="data-file-extension" value="dat"/>
<setting name="data-file-prefix" value="test"/>
<setting name="exception-file-prefix" value="test_except"/>
<setting name="program-length-limit" value="1000"/>
<setting name="trace-length-limit" value="1000"/>
<setting name="comments-enabled" value=""/>
<setting name="comments-debug" value=""/>
<setting name="default-test-data" value=""/>
<setting
name="arch-dirs"
value="cpu=arch/demo/cpu/settings.xml:minimips=arch/minimips/settings.xml"
/>
</settings>
</pre>
[[Command-Line Options]] page.