Installation Guide¶

Setting Environment Variables¶

Several steps below require environment variable to be set in your OS. When you encounter such step in the guide, do the following (substitute NAME and VALUE by the name and value of your environment variable respectively):

Windows¶

1. Open the System Properties window.
2. Switch to the Advanced tab.
3. Click on Environment Variables.
4. Click New... under System Variables.
5. In the New System Variable dialog specify variable name as NAME and variable value as VALUE.
6. Click OK on all open windows.
7. Reopen the command prompt window. **
   h3. Linux

Add the command below to the ~/.bash_profile or ~/.bashrc file (Linux):

export NAME=VALUE

Changes will be applied after restarting the command-line terminal or reboot. You can also execute the command in your command-line terminal to make temporary changes.

Retrascope Installation¶

1. Download and install JDK 11 (use AdoptOpenJDK for Windows and openjdk-11-jdk for Ubuntu Linux based OS).
2. Download and install SMT-LIBv2 solver. We recommend to use Z3 version 4.3 or higher.
3. Set either the system property smt.solver.path or the environment variable SMT_SOLVER_PATH to a full path to a SMT-solver executable file (for example, "/home/user/tools/z3/z3" or "C:\tools\z3\bin\z3.exe"). If the both are set, a value of fortress.solver.path will be used.
4. Download and unpack the Retrascope itself.
5. Retrascope uses *nuXmv* and/or *NuSMV* tools to perform model checking. To use them via Retrascope, do the following:
   1. To use nuXmv:
      1. Download and install nuXmv model checker.
      2. Set either the system property nuxmv.path or the environment variable NUXMV_PATH to a full path to a nuXmv executable file (for example, "/opt/tools/nuxmv/nuXmv" or "C:\tools\nuxmv\nuXmv.exe").
   2. To use NuSMV:
      1. Download and install NuSMV model checker.
      2. Set either the system property nusmv.path or the environment variable NUSMV_PATH to a full path to a NuSMV executable file (for example, "/opt/tools/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").
6. For VHDL designs elaboration:
   1. Set ZAMIA_LOCKING environment variable to true.
   2. Download and install Python interpreter.

To make sure the tool is successfully installed, enter the retrascope installation directory and run the following command for Windows OS (the correct output is also shown):

> bin\retrascope.bat --help
usage: files [options]
    --engine <arg>            Set a subset of engines
    --help                    Show this message
    --log <arg>               Set a log file
    --log-level <arg>         Set a log level
    --solver-debug            Set debug mode for SMT solver
    --target <arg>            Set a target entity
    --tool-debug-file <arg>   Set debug mode and save info to debug log file

For Linux-based OS:

$ ./bin/retrascope --help
usage: files [options]
    --engine <arg>            Set a subset of engines
    --help                    Show this message
    --log <arg>               Set a log file
    --log-level <arg>         Set a log level
    --solver-debug            Set debug mode for SMT solver
    --target <arg>            Set a target entity
    --tool-debug-file <arg>   Set debug mode and save info to debug log file

What's next?¶

1. To understand the main concept of the Retrascope architecture see Overview
2. For quick overview of common use cases see Getting Started
3. For full guide of the tool options, read Command Line Options
4. To understand the scientific foundations of the tool see Retrascope-Related Publications