Project

General

Profile

Installation Guide » History » Version 34

Sergey Smolov, 02/13/2020 04:43 PM

1 1 Sergey Smolov
h1. Installation Guide
2
3 16 Sergey Smolov
h2. Setting Environment Variables
4
5 20 Sergey Smolov
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):
6 16 Sergey Smolov
7
h3. Windows
8
9
# Open the @System Properties@ window.
10
# Switch to the @Advanced@ tab.
11
# Click on Environment Variables.
12
# Click @New...@ under @System Variables@.
13
# In the @New System Variable@ dialog specify variable name as @NAME@ and variable value as @VALUE@.
14
# Click @OK@ on all open windows.
15
# Reopen the command prompt window.
16
17
h3. Linux
18
19
Add the command below to the @~/.bash_profile@ or @~/.bashrc@ file (Linux):
20
<pre>export NAME=VALUE</pre> 
21
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.
22
23 17 Sergey Smolov
h2. Retrascope Installation
24 16 Sergey Smolov
25 25 Sergey Smolov
# Download and install JDK 11 (use "AdoptOpenJDK":https://adoptopenjdk.net/ for Windows and *openjdk-11-jdk* for Ubuntu Linux based OS). 
26 28 Sergey Smolov
# Download and install SMT-LIBv2 solver. We recommend to use "Z3 version 4.3 or higher":https://github.com/Z3Prover/z3.
27 34 Sergey Smolov
# 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.
28 23 Sergey Smolov
# Download and unpack the "Retrascope":https://forge.ispras.ru/projects/retrascope/files itself.
29 1 Sergey Smolov
# Retrascope uses *nuXmv* and/or *NuSMV* tools to perform model checking. To use them via Retrascope, do the following:
30 34 Sergey Smolov
## To use nuXmv:
31
### Download and install "nuXmv":https://es-static.fbk.eu/tools/nuxmv/index.php?n=Download.Download model checker.
32
### Set either the system property @nuxmv.path@ or the environment variable @NUXMV_PATH@ to a *full path to a nuXmv executable file* (for example, "/home/user/tools/nuxmv/nuXmv" or "C:\tools\nuxmv\nuXmv.exe").
33
## To use NuSMV:
34
### Download and install "NuSMV":http://nusmv.fbk.eu/NuSMV/download/getting-v2.html model checker.
35
### Set either the system property @nusmv.path@ or the environment variable @NUSMV_PATH@ to a *full path to a NuSMV executable file* (for example, "/home/user/tools/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").
36 16 Sergey Smolov
# For VHDL designs elaboration:
37 34 Sergey Smolov
## Set @ZAMIA_LOCKING@ environment variable to @true@.
38
## Download and install "Python interpreter":https://www.python.org. 
39 30 Sergey Smolov
40
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):
41
<pre>
42
> bin\retrascope.bat --help
43
usage: files [options]
44
    --engine <arg>            Set a subset of engines
45
    --help                    Show this message
46
    --log <arg>               Set a log file
47
    --log-level <arg>         Set a log level
48
    --solver-debug            Set debug mode for SMT solver
49
    --target <arg>            Set a target entity
50
    --tool-debug-file <arg>   Set debug mode and save info to debug log file
51
</pre>
52
For Linux-based OS:
53
<pre>
54
$ ./bin/retrascope --help
55
usage: files [options]
56
    --engine <arg>            Set a subset of engines
57
    --help                    Show this message
58
    --log <arg>               Set a log file
59
    --log-level <arg>         Set a log level
60
    --solver-debug            Set debug mode for SMT solver
61
    --target <arg>            Set a target entity
62
    --tool-debug-file <arg>   Set debug mode and save info to debug log file
63
</pre>
64
65
h2. What's next?
66
67
# To understand the main concept of the Retrascope architecture see "Overview":http://forge.ispras.ru/projects/retrascope/wiki/Overview
68
# For quick overview of common use cases see "Getting Started":http://forge.ispras.ru/projects/retrascope/wiki/Getting_Started
69
# For full guide of the tool options, read "Command Line Options":http://forge.ispras.ru/projects/retrascope/wiki/Command_Line_Options
70 1 Sergey Smolov
# To understand the scientific foundations of the tool see "Retrascope-Related Publications":https://forge.ispras.ru/projects/retrascope/wiki/Retrascope-Related_Publications