Project

General

Profile

Installation Guide » History » Version 96

Alexander Kamkin, 01/10/2020 01:50 PM

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