Project

General

Profile

Edit History

Wiki ยป

Installation Guide » History » Version 31

Mikhail Lebedev, 02/13/2020 03:33 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
    29
    Sergey Smolov
    
# Download and unpack the "Retrascope":https://forge.ispras.ru/projects/retrascope/files itself.





    28
    23
    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") in order to run solver-dependent tasks. If the both are set, a value of @fortress.solver.path@ will be used.





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





    30
    31
    Mikhail Lebedev
    
# 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") in order to run checker-dependent tasks.





    31
    
    
    
# To use the "NuSMV":http://nusmv.fbk.eu/NuSMV/download/getting-v2.html model checker download and install it.





    32
    
    
    
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") in order to run checker-dependent tasks.





    33
    10
    Mikhail Lebedev
    
# For VHDL designs elaboration:





    34
    16
    Sergey Smolov
    
  a) Set @ZAMIA_LOCKING@ environment variable to @true@.





    35
    26
    Sergey Smolov
    
  b) Download and install "Python interpreter":https://www.python.org. 





    36
    30
    Sergey Smolov
    





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





    38
    
    
    
<pre>





    39
    
    
    
> bin\retrascope.bat --help





    40
    
    
    
usage: files [options]





    41
    
    
    
    --engine <arg>            Set a subset of engines





    42
    
    
    
    --help                    Show this message





    43
    
    
    
    --log <arg>               Set a log file





    44
    
    
    
    --log-level <arg>         Set a log level





    45
    
    
    
    --solver-debug            Set debug mode for SMT solver





    46
    
    
    
    --target <arg>            Set a target entity





    47
    
    
    
    --tool-debug-file <arg>   Set debug mode and save info to debug log file





    48
    
    
    
</pre>





    49
    
    
    
For Linux-based OS:





    50
    
    
    
<pre>





    51
    
    
    
$ ./bin/retrascope --help





    52
    
    
    
usage: files [options]





    53
    
    
    
    --engine <arg>            Set a subset of engines





    54
    
    
    
    --help                    Show this message





    55
    
    
    
    --log <arg>               Set a log file





    56
    
    
    
    --log-level <arg>         Set a log level





    57
    
    
    
    --solver-debug            Set debug mode for SMT solver





    58
    
    
    
    --target <arg>            Set a target entity





    59
    
    
    
    --tool-debug-file <arg>   Set debug mode and save info to debug log file





    60
    
    
    
</pre>





    61
    
    
    





    62
    
    
    
h2. What's next?





    63
    
    
    





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





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





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





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