Installation Guide¶

• Table of contents
• Installation Guide
  • System Requirements
  • Installation
    • Installation Steps
    • Setting Environment Variables
    • Installation Directory Structure
    • Installing SMT Solvers
  • Usage
    • Model Compilation
    • Test Program Generation
  • Options
    • Command-Line Options
    • Settings File

System Requirements¶

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

1. JDK 11 (https://openjdk.java.net).
2. 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 Installing SMT Solvers).

Installation¶

Installation Steps¶

1. Download and unpack a distribution package (the latest .tar.gz file).
   The destination directory will be further referred to as <INSTALL_DIR>.
2. Set the MICROTESK_HOME environment variable to the <INSTALL_DIR> path (see Setting Environment Variables).
3. Add the <INSTALL_DIR>/bin path to the PATH environment variable.
4. If required, install SMT solver(s) to the <INSTALL_DIR>/tools directory (see Installing SMT Solvers).

Setting Environment Variables¶

Windows

1. Start the Control Panel dialog.
2. Click on the following items:
   - System and Security;
   - System;
   - Advanced system settings.
3. Click on Environment Variables.
4. Click on New... under System Variables.
5. Specify Variable name as MICROTESK_HOME and Variable value as <INSTALL_DIR>.
6. Click OK in all open windows.
7. Reopen the command prompt window.

Linux and macOS

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

export MICROTESK_HOME=<INSTALL_DIR>

Changes will be applied after restarting the terminal.

Installation Directory Structure¶

<INSTALL_DIR> contains the following subdirectories:

Installing SMT Solvers¶

To generate test data based on constraints, MicroTESK uses external SMT solvers. There are supported Z3 and 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

1. Build Z3 as it is described in https://github.com/Z3Prover/z3.
2. 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

1. Build CVC4 as it is described in https://github.com/CVC4/CVC4/.
   Or download CVC4 stable version from https://cvc4.github.io/downloads.html.
2. 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).

Usage¶

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:

$ cd $MICROTESK_HOME
$ sh bin/compile.sh arch/demo/minimips/model/minimips.nml arch/demo/minimips/model/mmu/minimips.mmu --extension-dir arch/demo/minimips/extensions

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

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:

$ cd $MICROTESK_HOME
$ sh bin/generate.sh minimips arch/demo/minimips/templates/euclid.rb

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):

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

Options¶

Command-Line Options¶

See Command-Line Options.

Settings File¶

Default values of options are stored in the <INSTALL_DIR>/etc/settings.xml configuration file:

<?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/demo/minimips/settings.xml" 
  />
</settings>