Actions
Installation Guide » History » Revision 48
« Previous |
Revision 48/63
(diff)
| Next »
Sergey Smolov, 02/14/2020 04:01 PM
Installation Guide¶
- Table of contents
- Installation Guide
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):
Windows¶
- Open the
System Properties
window. - Switch to the
Advanced
tab. - Click on Environment Variables.
- Click
New...
underSystem Variables
. - In the
New System Variable
dialog specify variable name asNAME
and variable value asVALUE
. - Click
OK
on all open windows. - Reopen the command prompt window.
Linux¶
Add the command below to the ~/.bash_profile
or ~/.bashrc
file (Linux):
export NAME=VALUE
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.
Retrascope Installation¶
- Download and install JDK 11 (use AdoptOpenJDK for Windows and openjdk-11-jdk for Ubuntu Linux based OS).
- Download and install SMT-LIBv2 solver Z3 version 4.3 or higher.
- Set the
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"). - Retrascope is able to use *nuXmv* or *NuSMV* to perform model checking.
Due to license limitations, we recommend to use NuSMV for commercial projects and nuXmv for non-commercial ones.
Choose the most suitable model checker and do the following:- To use nuXmv:
- Download and install nuXmv model checker.
- Set the
NUXMV_PATH
environment variable 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 model checker.
- Set the
NUSMV_PATH
environment variable to a full path to NuSMV executable (like "/home/user/nusmv/bin/NuSMV" or "C:\tools\nusmv\bin\NuSMV.exe").
- To use nuXmv:
- For VHDL designs elaboration:
- Set
ZAMIA_LOCKING
environment variable totrue
. - Download and install Python interpreter.
- Set
- Download and unpack the Retrascope.
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):
> 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
For Linux-based OS:
$ ./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
What's next?¶
- To understand the main concept of the Retrascope architecture see Overview
- For quick overview of common use cases see Getting Started
- For full guide of the tool options, read Command Line Options
- To understand the scientific foundations of the tool see Retrascope-Related Publications
Updated by Sergey Smolov over 4 years ago · 48 revisions