Installation Guide » History » Revision 109
Revision 108 (Alexander Protsenko, 02/17/2021 03:13 PM) → Revision 109/115 (Sergey Smolov, 02/17/2021 03:57 PM)
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+ 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":http://forge.ispras.ru/projects/microtesk/files 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>