Retrascope

h1. Installation Guide

{{toc}}

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

h3. Windows

# Open the @System Properties@ window.

# Switch to the @Advanced@ tab.

# Click on Environment Variables.

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

# In the @New System Variable@ dialog specify variable name as @NAME@ and variable value as @VALUE@.

# Click @OK@ on all open windows.

# Reopen the command prompt window.

h3. Linux

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

<pre>export NAME=VALUE</pre> 

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.

h2. Retrascope Installation

# Download and install JDK 11 (use " *AdoptOpenJDK* ":https://adoptopenjdk.net/ for Windows and *openjdk-11-jdk* for Ubuntu Linux based OS). 

# Download and install SMT-LIBv2 solver. We recommend to use " *Z3 version 4.3 or higher* ":https://github.com/Z3Prover/z3.

# Set either the system property @smt.solver.path@ or the environment variable @SMT_SOLVER_PATH@ to a +full path to SMT-solver executable+ (like "/home/user/z3/z3" or "C:\tools\z3\bin\z3.exe"). If the both are set, a value of @fortress.solver.path@ will be used.

# Download and unpack the " *Retrascope* ":https://forge.ispras.ru/projects/retrascope/files itself.

# Retrascope uses "*nuXmv*":https://nuxmv.fbk.eu/ and/or "*NuSMV*":http://nusmv.fbk.eu/ tools to perform model checking. To use them via Retrascope, do the following:

## To use *nuXmv*:

### Download and install "nuXmv":https://es-static.fbk.eu/tools/nuxmv/index.php?n=Download.Download model checker.

### Set either the system property @nuxmv.path@ or the environment variable @NUXMV_PATH@ to a +full path to nuXmv executable+ (like "/home/user/nuxmv/nuXmv" or "C:\tools\nuxmv\nuXmv.exe").

## To use *NuSMV*:

### Download and install "NuSMV":http://nusmv.fbk.eu/NuSMV/download/getting-v2.html model checker.

### Set either the system property @nusmv.path@ or the environment variable @NUSMV_PATH@ to a +full path to NuSMV executable+ (like "/home/user/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").

# For *VHDL* designs elaboration:

## Set @ZAMIA_LOCKING@ environment variable to @true@.

## Download and install " *Python interpreter* ":https://www.python.org. 

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

<pre>

> 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

</pre>

For Linux-based OS:

<pre>

$ ./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

</pre>

h2. What's next?

# To understand the main concept of the Retrascope architecture see "Overview":http://forge.ispras.ru/projects/retrascope/wiki/Overview

# For quick overview of common use cases see "Getting Started":http://forge.ispras.ru/projects/retrascope/wiki/Getting_Started

# For full guide of the tool options, read "Command Line Options":http://forge.ispras.ru/projects/retrascope/wiki/Command_Line_Options

# To understand the scientific foundations of the tool see "Retrascope-Related Publications":https://forge.ispras.ru/projects/retrascope/wiki/Retrascope-Related_Publications