Project

General

Profile

Installation Guide » History » Version 57

Sergey Smolov, 02/17/2020 05:42 PM

1 1 Sergey Smolov
h1. Installation Guide
2 38 Sergey Smolov
3 37 Sergey Smolov
{{toc}}
4 1 Sergey Smolov
5 53 Sergey Smolov
h2. Before we start: setting environment variables
6 16 Sergey Smolov
7 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):
8 16 Sergey Smolov
9
h3. Windows
10
11
# Open the @System Properties@ window.
12
# Switch to the @Advanced@ tab.
13
# Click on Environment Variables.
14
# Click @New...@ under @System Variables@.
15
# In the @New System Variable@ dialog specify variable name as @NAME@ and variable value as @VALUE@.
16
# Click @OK@ on all open windows.
17
# Reopen the command prompt window.
18 39 Sergey Smolov
19 16 Sergey Smolov
h3. Linux
20
21
Add the command below to the @~/.bash_profile@ or @~/.bashrc@ file (Linux):
22
<pre>export NAME=VALUE</pre> 
23
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.
24
25 17 Sergey Smolov
h2. Retrascope Installation
26 16 Sergey Smolov
27 35 Sergey Smolov
# Download and install JDK 11 (use " *AdoptOpenJDK* ":https://adoptopenjdk.net/ for Windows and *openjdk-11-jdk* for Ubuntu Linux based OS). 
28 43 Sergey Smolov
# Download and install SMT-LIBv2 solver " *Z3 version 4.3 or higher* ":https://github.com/Z3Prover/z3.
29 50 Sergey Smolov
# Set @SMT_SOLVER_PATH@ environment variable to a +full path to SMT-solver executable+ (like "/home/user/z3/bin/z3" or "C:\tools\z3\bin\z3.exe").
30 45 Sergey Smolov
# Retrascope is able to use "*nuXmv*":https://nuxmv.fbk.eu/ or "*NuSMV*":http://nusmv.fbk.eu/ to perform model checking. 
31 46 Sergey Smolov
Due to license limitations, we recommend to use NuSMV for commercial projects and nuXmv for non-commercial ones.
32
Choose the most suitable model checker and do the following:
33 35 Sergey Smolov
## To use *nuXmv*:
34 34 Sergey Smolov
### Download and install "nuXmv":https://es-static.fbk.eu/tools/nuxmv/index.php?n=Download.Download model checker.
35 49 Sergey Smolov
### Set @NUXMV_PATH@ environment variable to a +full path to nuXmv executable+ (like "/home/user/nuxmv/nuXmv" or "C:\tools\nuxmv\nuXmv.exe").
36 35 Sergey Smolov
## To use *NuSMV*:
37 34 Sergey Smolov
### Download and install "NuSMV":http://nusmv.fbk.eu/NuSMV/download/getting-v2.html model checker.
38 49 Sergey Smolov
### Set @NUSMV_PATH@ environment variable to a +full path to NuSMV executable+ (like "/home/user/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").
39 35 Sergey Smolov
# For *VHDL* designs elaboration:
40 1 Sergey Smolov
## Set @ZAMIA_LOCKING@ environment variable to @true@.
41 34 Sergey Smolov
## Download and install " *Python interpreter* ":https://www.python.org. 
42 41 Sergey Smolov
# Download and unpack the " *Retrascope* ":https://forge.ispras.ru/projects/retrascope/files.
43 30 Sergey Smolov
44
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):
45
<pre>
46 55 Sergey Smolov
>bin\retrascope.bat --check
47
Retrascope version: 1.1.3-beta-SNAPSHOT
48
49 56 Sergey Smolov
2020.02.17 17:11:30.258. INFO: SMT solver is installed here: C:\Program Files\z3\bin\z3.exe
50 55 Sergey Smolov
2020.02.17 17:11:30.298. INFO: Z3 version 4.3.2
51 1 Sergey Smolov
52 55 Sergey Smolov
2020.02.17 17:11:30.308. WARNING: 'NUSMV_PATH' env variable is not set.
53 56 Sergey Smolov
2020.02.17 17:11:30.308. INFO: nuXmv is installed here: C:\Program Files\nuxmv\nuXmv.exe
54
2020.02.17 17:11:31.288. INFO: *** This is nuXmv 1.0.1 (compiled on Mon Nov 17 16:54:49 2014)
55 55 Sergey Smolov
56 57 Sergey Smolov
2020.02.17 17:11:31.288. WARNING: Set 'ZAMIA_LOCKING' environment variable to 'true' for VHDL designs processing
57 55 Sergey Smolov
2020.02.17 17:11:31.318. INFO: Python 3.8.1
58
59 30 Sergey Smolov
</pre>
60
For Linux-based OS:
61
<pre>
62 51 Sergey Smolov
$ ./bin/retrascope --check
63
Retrascope version: 1.1.3-beta-SNAPSHOT
64
65
2020.02.14 17:20:23.717. INFO: SMT solver is installed here: /home/tools/z3-4.7.1-x64-ubuntu-16.04/bin/z3
66
2020.02.14 17:20:23.759. INFO: Z3 version 4.7.1 - 64 bit
67
68
2020.02.14 17:20:23.759. WARNING: 'NUSMV_PATH' env variable is not set.
69
2020.02.14 17:20:23.760. INFO: nuXmv is installed here: /home/tools/nuxmv-1.0.1-linux-x86_64/nuXmv
70
2020.02.14 17:20:23.774. INFO: *** This is nuXmv 1.0.1 (compiled on Mon Nov 17 16:49:54 2014)
71
72 57 Sergey Smolov
2020.02.14 17:20:23.774. INFO: 'ZAMIA_LOCKING' environment variable is set to 'true'
73 51 Sergey Smolov
2020.02.14 17:20:23.776. INFO: Python 2.7.17
74 30 Sergey Smolov
</pre>
75
76
h2. What's next?
77
78
# To understand the main concept of the Retrascope architecture see "Overview":http://forge.ispras.ru/projects/retrascope/wiki/Overview
79
# For quick overview of common use cases see "Getting Started":http://forge.ispras.ru/projects/retrascope/wiki/Getting_Started
80 54 Sergey Smolov
# For full guide of the tool options see "Command Line Options":http://forge.ispras.ru/projects/retrascope/wiki/Command_Line_Options
81 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