MicroTESK

h1. Installation Guide

{{toc}}

h2. System Requirements

Being developed in Java, MicroTESK can be used on Windows, Linux, macOS, and other platforms with the following software installed:

* JDK 11+ (https://openjdk.java.net );

* Apache Ant 1.8+ (https://ant.apache.org).

To generate test data based on constraints (if required), MicroTESK needs an SMT solver such as Z3 or CVC4 (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).

h2. Installation

h3. Installation Steps

# Download from http://forge.ispras.ru/projects/microtesk/files and unpack a distribution package (the latest @.tar.gz@ file).

  The destination directory will be further referred to as @<INSTALL_DIR>@.

# Set the @MICROTESK_HOME@ environment variable to the @<INSTALL_DIR>@ path (see [[Installation Guide#Setting-Environment-Variables|Setting Environment Variables]]).

# Add the @<INSTALL_DIR>/bin@ path to the @PATH@ environment variable.

# If required, install SMT solver(s) to the @<INSTALL_DIR>/tools@ directory (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).

h3. Setting Environment Variables

*Windows*

# Start the @Control Panel@ dialog.

# Click on the following items:

  - @System and Security@;

  - @System@;

  - @Advanced system settings@.

# Click on @Environment Variables@.

# Click on @New...@ under @System Variables@.

# Specify @Variable name@ as @MICROTESK_HOME@ and @Variable value@ as @<INSTALL_DIR>@.

# Click @OK@ in all open windows.

# Reopen the command prompt window.

*Linux and macOS*

Add the command below to @~/.bash_profile@ (Linux) or @~/.profile@ (macOS):

<pre>

export MICROTESK_HOME=<INSTALL_DIR>

</pre>

Changes will be applied after restarting the terminal.

h3. Installation Directory Structure

@<INSTALL_DIR>@ contains the following subdirectories:

table=.

{font-style:italic; font-weight:bold; background:#ddd}. |<. Directory |<. Description |

                      |<. @arch@    |<. Microprocessor specifications and test templates |

{background:#f6fcff}. |<. @bin@     |<. Scripts for model compilation and test generation |

                      |<. @doc@     |<. Documentation |

{background:#f6fcff}. |<. @etc@     |<. Configuration files |

                      |<. @gen@     |<. Generated code of microprocessor models |

{background:#f6fcff}. |<. @lib@     |<. JAR files and Ruby scripts |

                      |<. @src@     |<. Source code |

{background:#f6fcff}. |<. @tools@   |<. SMT solvers |

h3. Installing SMT Solvers

To generate test data based on constraints, MicroTESK uses external SMT solvers. There are supported "Z3":https://github.com/z3prover/ and "CVC4":https://github.com/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. 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 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 specification, run the following command:

* @sh compile.sh <SPECIFICATION>@ (Linux and macOS);

* @compile.bat <SPECIFICATION>@ (Windows).

For example, the actions below compile the model from the miniMIPS specification:

<pre>

$ cd $MICROTESK_HOME

$ sh bin/compile.sh arch/minimips/model/minimips.nml arch/minimips/model/mmu/minimips.mmu

</pre>

*NOTE:* Models for all demo specifications are included into the MicroTESK distribution package. There is no need to compile them.

h3. Test Program Generation

To generate a test program for a given architecture (model) and a given test template, run the following command:

* @sh generate.sh <ARCH> <TEMPLATE>@ (Linux and macOS);

* @generate.bat <ARCH> <TEMPLATE>@ (Windows).

For example, the actions below generate a test program for the miniMIPS model compiled in the previous example and the @euclid.rb@ test template:

<pre>

$ cd $MICROTESK_HOME

$ sh bin/generate.sh minimips arch/minimips/templates/euclid.rb

</pre>

The output file name depends on the @--code-file-prefix@ and @--code-file-extension@ options (see [[Command-Line Options]]).

To specify which SMT solver should be used to solve constraints (if required), specify the @--solver <SOLVER>@ (or @-s <SOLVER>@) option, where @<SOLVER>@ is @z3@ or @cvc4@ (by default, Z3 is used):

<pre>

$ cd $MICROTESK_HOME

$ sh bin/generate.sh -s cvc4 minimips arch/minimips/templates/constraint.rb

</pre>

h2. Options

h3. Command-Line Options

See [[Command-Line Options]].

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>