Installation Guide » History » Version 49
Sergey Smolov, 02/14/2020 04:04 PM
1 | 1 | Sergey Smolov | h1. Installation Guide |
---|---|---|---|
2 | 38 | Sergey Smolov | |
3 | 37 | Sergey Smolov | {{toc}} |
4 | 1 | Sergey Smolov | |
5 | 16 | Sergey Smolov | h2. Setting Environment Variables |
6 | |||
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 | 49 | Sergey Smolov | # Set @SMT_SOLVER_PATH@ environment variable to a +full path to SMT-solver executable+ (like "/home/user/z3/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 | > bin\retrascope.bat --help |
||
47 | usage: files [options] |
||
48 | --engine <arg> Set a subset of engines |
||
49 | --help Show this message |
||
50 | --log <arg> Set a log file |
||
51 | --log-level <arg> Set a log level |
||
52 | --solver-debug Set debug mode for SMT solver |
||
53 | --target <arg> Set a target entity |
||
54 | --tool-debug-file <arg> Set debug mode and save info to debug log file |
||
55 | </pre> |
||
56 | For Linux-based OS: |
||
57 | <pre> |
||
58 | $ ./bin/retrascope --help |
||
59 | usage: files [options] |
||
60 | --engine <arg> Set a subset of engines |
||
61 | --help Show this message |
||
62 | --log <arg> Set a log file |
||
63 | --log-level <arg> Set a log level |
||
64 | --solver-debug Set debug mode for SMT solver |
||
65 | --target <arg> Set a target entity |
||
66 | --tool-debug-file <arg> Set debug mode and save info to debug log file |
||
67 | </pre> |
||
68 | |||
69 | h2. What's next? |
||
70 | |||
71 | # To understand the main concept of the Retrascope architecture see "Overview":http://forge.ispras.ru/projects/retrascope/wiki/Overview |
||
72 | # For quick overview of common use cases see "Getting Started":http://forge.ispras.ru/projects/retrascope/wiki/Getting_Started |
||
73 | # For full guide of the tool options, read "Command Line Options":http://forge.ispras.ru/projects/retrascope/wiki/Command_Line_Options |
||
74 | 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 |