Project

General

Profile

Installation Guide » History » Revision 41

Revision 40 (Sergey Smolov, 02/13/2020 04:52 PM) → Revision 41/63 (Sergey Smolov, 02/13/2020 04:58 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. We recommend to use " *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 @fortress.solver.path@ will be used. 
 # Download and unpack the " *Retrascope* ":https://forge.ispras.ru/projects/retrascope/files itself. 
 # Retrascope is able to use uses "*nuXmv*":https://nuxmv.fbk.eu/ or and/or "*NuSMV*":http://nusmv.fbk.eu/ tools to perform model checking. Select the one that is more suitable for your tasks (due to license limitations, we'd recommend to select NuSMV for commercial projects and nuXmv for non-commercial ones), and To use them via Retrascope, 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