Installation Guide¶

Prerequisites¶

For VHDL code elaboration we use ZamiaCAD toolkit.

For constraint solving we use Z3 SMT solver.

For model checking we use nuXmv tool (see distribution below).

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¶

1. Open the System Properties window.
2. Switch to the Advanced tab.
3. Click on Environment Variables.
4. Click New... under System Variables.
5. In the New System Variable dialog specify variable name as NAME and variable value as VALUE.
6. Click OK on all open windows.
7. 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¶

1. Download and install JDK 1.11
2. Download and install SMT-LIBv2 solver. We recommend to use Z3 4.3.
3. 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.
4. Download and install nuXmv model checker.
5. 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.
6. For VHDL designs elaboration:
   a) Set ZAMIA_LOCKING environment variable to true.
   b) Download and install Python interpreter.
7. Download, unpack and use the tool through it's Command Line Options.