Project

General

Profile

Installation Guide » History » Revision 107

Revision 106 (Alexander Kamkin, 01/10/2020 02:21 PM) → Revision 107/115 (Alexander Protsenko, 02/17/2021 02:43 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+ (https://openjdk.java.net ); (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>