Project

General

Profile

Installation Guide » History » Revision 46

Revision 45 (Sergey Smolov, 02/14/2020 03:47 PM) → Revision 46/63 (Sergey Smolov, 02/14/2020 03:48 PM)

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 " *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 @smt.solver.path@ will be used. 
 # Retrascope is able to use "*nuXmv*":https://nuxmv.fbk.eu/ or "*NuSMV*":http://nusmv.fbk.eu/ to perform model checking.  
 Due to license limitations, we recommend to use select NuSMV for commercial projects and nuXmv for non-commercial ones. 
 Choose Select the most one that is more suitable model checker for your tasks, and 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.  
 # Download and unpack the " *Retrascope* ":https://forge.ispras.ru/projects/retrascope/files. 

 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