Project

General

Profile

Installation Guide » History » Version 113

Alexander Protsenko, 07/31/2023 11:09 AM

1 1 Andrei Tatarnikov
h1. Installation Guide
2
3 36 Alexander Kamkin
{{toc}}
4
5 96 Alexander Kamkin
h2. System Requirements
6 1 Andrei Tatarnikov
7 96 Alexander Kamkin
Being developed in Java, MicroTESK can be used on Windows, Linux, macOS, and other platforms with the following software installed:
8 1 Andrei Tatarnikov
9 110 Alexander Protsenko
# JDK 11+ (https://openjdk.java.net).
10
# Apache Ant 1.8+ (https://ant.apache.org).
11 96 Alexander Kamkin
12 98 Alexander Kamkin
To generate test data based on constraints (if required), MicroTESK needs an SMT solver such as Z3 or CVC4 (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).
13 96 Alexander Kamkin
14
h2. Installation
15
16 1 Andrei Tatarnikov
h3. Installation Steps
17
18 109 Sergey Smolov
# "Download":http://forge.ispras.ru/projects/microtesk/files and unpack a distribution package (the latest @.tar.gz@ file).
19 98 Alexander Kamkin
  The destination directory will be further referred to as @<INSTALL_DIR>@.
20 96 Alexander Kamkin
# Set the @MICROTESK_HOME@ environment variable to the @<INSTALL_DIR>@ path (see [[Installation Guide#Setting-Environment-Variables|Setting Environment Variables]]).
21 1 Andrei Tatarnikov
# Add the @<INSTALL_DIR>/bin@ path to the @PATH@ environment variable.
22 98 Alexander Kamkin
# If required, install SMT solver(s) to the @<INSTALL_DIR>/tools@ directory (see [[Installation Guide#Installing-SMT-Solvers|Installing SMT Solvers]]).
23 96 Alexander Kamkin
24 101 Alexander Kamkin
h3. Setting Environment Variables
25 96 Alexander Kamkin
26
*Windows*
27
28
# Start the @Control Panel@ dialog.
29
# Click on the following items:
30 105 Alexander Kamkin
  - @System and Security@;
31
  - @System@;
32
  - @Advanced system settings@.
33 96 Alexander Kamkin
# Click on @Environment Variables@.
34
# Click on @New...@ under @System Variables@.
35
# Specify @Variable name@ as @MICROTESK_HOME@ and @Variable value@ as @<INSTALL_DIR>@.
36
# Click @OK@ in all open windows.
37 1 Andrei Tatarnikov
# Reopen the command prompt window.
38
39 96 Alexander Kamkin
*Linux and macOS*
40 1 Andrei Tatarnikov
41 96 Alexander Kamkin
Add the command below to @~/.bash_profile@ (Linux) or @~/.profile@ (macOS):
42 1 Andrei Tatarnikov
43 96 Alexander Kamkin
<pre>
44
export MICROTESK_HOME=<INSTALL_DIR>
45
</pre>
46 1 Andrei Tatarnikov
47 96 Alexander Kamkin
Changes will be applied after restarting the terminal.
48 1 Andrei Tatarnikov
49 96 Alexander Kamkin
h3. Installation Directory Structure
50 1 Andrei Tatarnikov
51 96 Alexander Kamkin
@<INSTALL_DIR>@ contains the following subdirectories:
52 1 Andrei Tatarnikov
53 96 Alexander Kamkin
table=.
54
{font-style:italic; font-weight:bold; background:#ddd}. |<. Directory |<. Description |
55 102 Alexander Kamkin
                      |<. @arch@    |<. Microprocessor specifications and test templates |
56
{background:#f6fcff}. |<. @bin@     |<. Scripts for model compilation and test generation |
57
                      |<. @doc@     |<. Documentation |
58
{background:#f6fcff}. |<. @etc@     |<. Configuration files |
59
                      |<. @gen@     |<. Generated code of microprocessor models |
60
{background:#f6fcff}. |<. @lib@     |<. JAR files and Ruby scripts |
61
                      |<. @src@     |<. Source code |
62
{background:#f6fcff}. |<. @tools@   |<. SMT solvers |
63 1 Andrei Tatarnikov
64 101 Alexander Kamkin
h3. Installing SMT Solvers
65 96 Alexander Kamkin
66 104 Alexander Kamkin
To generate test data based on constraints, MicroTESK uses external SMT solvers. There are supported "Z3":https://github.com/z3prover/ and "CVC4":https://github.com/CVC4/CVC4/. Solver executables should be placed to @<INSTALL_DIR>/tools@.
67 1 Andrei Tatarnikov
68 96 Alexander Kamkin
*Specifying paths*
69 40 Alexander Kamkin
70 106 Alexander Kamkin
If solvers are already installed, MicroTESK can find them by using the @Z3_PATH@ and @CVC4_PATH@ environment variables. Each @_PATH@ variable specifies the path to the corresponding executable.
71 1 Andrei Tatarnikov
72 96 Alexander Kamkin
*Installing Z3*
73 1 Andrei Tatarnikov
74 109 Sergey Smolov
# Build Z3 as it is described in https://github.com/Z3Prover/z3.
75
# Move the executable file to the following path (or create a symbolic link):
76 96 Alexander Kamkin
  - @<INSTALL_DIR>/tools/z3/windows/z3.exe@ (Windows);
77
  - @<INSTALL_DIR>/tools/z3/unix/z3@ (Linux);
78
  - @<INSTALL_DIR>/tools/z3/osx/z3@ (macOS).
79 1 Andrei Tatarnikov
80 96 Alexander Kamkin
*Installing CVC4*
81 1 Andrei Tatarnikov
82 111 Alexander Protsenko
# Build CVC4 as it is described in "https://github.com/CVC4/CVC4/":https://github.com/CVC4/CVC4-archived.
83 112 Alexander Protsenko
  Or download CVC4 stable version from https://cvc4.github.io/downloads.html.
84 109 Sergey Smolov
# Move the executable file to the following path (or create a symbolic link):
85 96 Alexander Kamkin
  - @<INSTALL_DIR>/tools/cvc4/windows/cvc4.exe@ (Windows);
86
  - @<INSTALL_DIR>/tools/cvc4/unix/cvc4@ (Linux);
87
  - @<INSTALL_DIR>/tools/cvc4/osx/cvc4@ (macOS).
88 1 Andrei Tatarnikov
89 96 Alexander Kamkin
h2. Usage
90 1 Andrei Tatarnikov
91 96 Alexander Kamkin
h3. Model Compilation
92
93
To compile a microprocessor model from its specification, run the following command:
94
95
* @sh compile.sh <SPECIFICATION>@ (Linux and macOS);
96
* @compile.bat <SPECIFICATION>@ (Windows).
97
98
For example, the actions below compile the model from the miniMIPS specification:
99
100 1 Andrei Tatarnikov
<pre>
101 96 Alexander Kamkin
$ cd $MICROTESK_HOME
102 113 Alexander Protsenko
$ sh bin/compile.sh arch/demo/minimips/model/minimips.nml arch/demo/minimips/model/mmu/minimips.mmu
103 1 Andrei Tatarnikov
</pre>
104
105 96 Alexander Kamkin
*NOTE:* Models for all demo specifications are included into the MicroTESK distribution package. There is no need to compile them.
106 1 Andrei Tatarnikov
107 96 Alexander Kamkin
h3. Test Program Generation
108 1 Andrei Tatarnikov
109 96 Alexander Kamkin
To generate a test program for a given architecture (model) and a given test template, run the following command:
110 1 Andrei Tatarnikov
111 96 Alexander Kamkin
* @sh generate.sh <ARCH> <TEMPLATE>@ (Linux and macOS);
112
* @generate.bat <ARCH> <TEMPLATE>@ (Windows).
113 1 Andrei Tatarnikov
114 96 Alexander Kamkin
For example, the actions below generate a test program for the miniMIPS model compiled in the previous example and the @euclid.rb@ test template:
115
116 33 Alexander Kamkin
<pre>
117 96 Alexander Kamkin
$ cd $MICROTESK_HOME
118 113 Alexander Protsenko
$ sh bin/generate.sh minimips arch/demo/minimips/templates/euclid.rb
119 43 Andrei Tatarnikov
</pre>
120
121 99 Alexander Kamkin
The output file name depends on the @--code-file-prefix@ and @--code-file-extension@ options (see [[Command-Line Options]]).
122 14 Andrei Tatarnikov
123 96 Alexander Kamkin
To specify which SMT solver should be used to solve constraints (if required), specify the @--solver <SOLVER>@ (or @-s <SOLVER>@) option, where @<SOLVER>@ is @z3@ or @cvc4@ (by default, Z3 is used):
124
125 89 Alexander Kamkin
<pre>
126 96 Alexander Kamkin
$ cd $MICROTESK_HOME
127 113 Alexander Protsenko
$ sh bin/generate.sh -s cvc4 minimips arch/demo/minimips/templates/constraint.rb
128 95 Andrei Tatarnikov
</pre>
129 27 Andrei Tatarnikov
130 1 Andrei Tatarnikov
h2. Options
131 100 Alexander Kamkin
132
h3. Command-Line Options
133
134
See [[Command-Line Options]].
135 96 Alexander Kamkin
136
h3. Settings File
137
138
Default values of options are stored in the @<INSTALL_DIR>/etc/settings.xml@ configuration file:
139
140
<pre>
141
<?xml version="1.0" encoding="utf-8"?>
142
<settings>
143
  <setting name="random-seed" value="0"/>
144
  <setting name="branch-exec-limit" value="1000"/>
145
  <setting name="code-file-extension" value="asm"/>
146
  <setting name="code-file-prefix" value="test"/>
147
  <setting name="data-file-extension" value="dat"/>
148
  <setting name="data-file-prefix" value="test"/>
149
  <setting name="exception-file-prefix" value="test_except"/>
150
  <setting name="program-length-limit" value="1000"/>
151
  <setting name="trace-length-limit" value="1000"/>
152
  <setting name="comments-enabled" value=""/>
153
  <setting name="comments-debug" value=""/>
154
  <setting name="default-test-data" value=""/>
155
  <setting
156
    name="arch-dirs"
157 113 Alexander Protsenko
    value="cpu=arch/demo/cpu/settings.xml:minimips=arch/demo/minimips/settings.xml"
158 96 Alexander Kamkin
  />
159
</settings>
160
</pre>